Mercurial > hg > Members > kono > Proof > ZF-in-agda

annotate fig/address-of-HOD.svg @ 361:4cbcf71b09c4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Jul 2020 16:33:30 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 <svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="253.785 161.5 248.185 537.116" width="248.185" height="537.116">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 <defs>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -3 6 6" markerWidth="6" markerHeight="6" color="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 <g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 <path d="M 3.7333333 0 L 0 -1.4 L 0 1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 </marker>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 <font-face font-family="Helvetica Neue" font-size="22" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 <font-face-src>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 <font-face-name name="HelveticaNeue"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 </font-face-src>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 </font-face>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-5 -3 6 6" markerWidth="6" markerHeight="6" color="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 <g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 <path d="M -3.7333333 0 L 0 1.4 L 0 -1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 </marker>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 <font-face font-family="Helvetica Neue" font-size="14" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 <font-face-src>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 <font-face-name name="HelveticaNeue"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 </font-face-src>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 </font-face>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 </defs>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 <metadata> Produced by OmniGraffle 7.12.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 <dc:date>2020-07-16 09:18:05 +0000</dc:date>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 </metadata>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 <title>Canvas 1</title>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 <rect fill="white" x="253.785" y="161.5" width="248.185" height="537.116"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 <g id="Canvas_1: Layer 1">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 <title>Layer 1</title>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 <g id="Graphic_17">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" fill="white"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 <g id="Line_22">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 <path d="M 411.04 513.5 C 399.34904 489.1891 344.94662 458.1271 312.2266 439.7944" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 <g id="Graphic_19">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" fill="white"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 <g id="Graphic_18">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" fill="white"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 <g id="Graphic_16">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" fill="white"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 <g id="Graphic_15">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 <g id="Graphic_13">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 <circle cx="294.04" cy="215.5" r="6.50001038636234" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 <circle cx="294.04" cy="215.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 <g id="Graphic_11">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 <circle cx="294.04" cy="338.5" r="6.50001038636235" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 <circle cx="294.04" cy="338.5" r="6.50001038636235" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 <g id="Graphic_10">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 <circle cx="294.04" cy="429.5" r="6.50001038636236" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 <circle cx="294.04" cy="429.5" r="6.50001038636236" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 <g id="Graphic_9">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 <circle cx="294.04" cy="458.5" r="6.50001038636234" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 <circle cx="294.04" cy="458.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 <g id="Graphic_8">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 <circle cx="289.75835" cy="559.5" r="6.50001038636231" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 <circle cx="289.75835" cy="559.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 <g id="Graphic_7">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 <text transform="translate(258.785 667)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 </text>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 <g id="Graphic_6">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 <text transform="translate(367 608)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="37.07" y="21">HOD</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="47.616">such as (x,y)</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 </text>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 <g id="Graphic_4">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 <circle cx="289.75835" cy="183.5" r="6.50001038636233" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 <circle cx="289.75835" cy="183.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 <g id="Line_21">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 <path d="M 394.8927 484.52356 C 373.0247 446.2235 335.43026 385.45883 310.8905 355.36405" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 <g id="Line_23">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 <path d="M 432.15203 479.32975 C 465.39396 437.59087 508.5818 403.685 494 365 C 475.7518 316.58818 367.02 260.6628 300.54 222" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="12.0,12.0" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 <g id="Line_24">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 <path d="M 432.5173 470.00093 C 444.1753 446.3428 445.478 433.10376 433 400 C 415.3925 353.28783 364.2836 345.6657 300.99565 310.45614" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 <g id="Graphic_12">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 <circle cx="294.04" cy="306.5" r="6.50001038636234" fill="black"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 <circle cx="294.04" cy="306.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 <g id="Graphic_25">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 <text transform="translate(373 207.608)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.309" y="13">The address of</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="5755396e-19" y="29.392">HOD has a freedom</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 </text>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 </svg>