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

comparison 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
comparison
equal deleted inserted replaced
360:2a8a51375e49 361:4cbcf71b09c4
1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
2 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
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">
4 <defs>
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">
6 <g>
7 <path d="M 3.7333333 0 L 0 -1.4 L 0 1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
8 </g>
9 </marker>
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">
11 <font-face-src>
12 <font-face-name name="HelveticaNeue"/>
13 </font-face-src>
14 </font-face>
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">
16 <g>
17 <path d="M -3.7333333 0 L 0 1.4 L 0 -1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
18 </g>
19 </marker>
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">
21 <font-face-src>
22 <font-face-name name="HelveticaNeue"/>
23 </font-face-src>
24 </font-face>
25 </defs>
26 <metadata> Produced by OmniGraffle 7.12.1
27 <dc:date>2020-07-16 09:18:05 +0000</dc:date>
28 </metadata>
29 <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
30 <title>Canvas 1</title>
31 <rect fill="white" x="253.785" y="161.5" width="248.185" height="537.116"/>
32 <g id="Canvas_1: Layer 1">
33 <title>Layer 1</title>
34 <g id="Graphic_17">
35 <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" fill="white"/>
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"/>
37 </g>
38 <g id="Line_22">
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"/>
40 </g>
41 <g id="Graphic_19">
42 <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" fill="white"/>
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"/>
44 </g>
45 <g id="Graphic_18">
46 <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" fill="white"/>
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"/>
48 </g>
49 <g id="Graphic_16">
50 <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" fill="white"/>
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"/>
52 </g>
53 <g id="Graphic_15">
54 <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/>
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"/>
56 </g>
57 <g id="Graphic_13">
58 <circle cx="294.04" cy="215.5" r="6.50001038636234" fill="black"/>
59 <circle cx="294.04" cy="215.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
60 </g>
61 <g id="Graphic_11">
62 <circle cx="294.04" cy="338.5" r="6.50001038636235" fill="black"/>
63 <circle cx="294.04" cy="338.5" r="6.50001038636235" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
64 </g>
65 <g id="Graphic_10">
66 <circle cx="294.04" cy="429.5" r="6.50001038636236" fill="black"/>
67 <circle cx="294.04" cy="429.5" r="6.50001038636236" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
68 </g>
69 <g id="Graphic_9">
70 <circle cx="294.04" cy="458.5" r="6.50001038636234" fill="black"/>
71 <circle cx="294.04" cy="458.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
72 </g>
73 <g id="Graphic_8">
74 <circle cx="289.75835" cy="559.5" r="6.50001038636231" fill="black"/>
75 <circle cx="289.75835" cy="559.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
76 </g>
77 <g id="Graphic_7">
78 <text transform="translate(258.785 667)" fill="black">
79 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan>
80 </text>
81 </g>
82 <g id="Graphic_6">
83 <text transform="translate(367 608)" fill="black">
84 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="37.07" y="21">HOD</tspan>
85 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="47.616">such as (x,y)</tspan>
86 </text>
87 </g>
88 <g id="Graphic_4">
89 <circle cx="289.75835" cy="183.5" r="6.50001038636233" fill="black"/>
90 <circle cx="289.75835" cy="183.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
91 </g>
92 <g id="Line_21">
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"/>
94 </g>
95 <g id="Line_23">
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"/>
97 </g>
98 <g id="Line_24">
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"/>
100 </g>
101 <g id="Graphic_12">
102 <circle cx="294.04" cy="306.5" r="6.50001038636234" fill="black"/>
103 <circle cx="294.04" cy="306.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
104 </g>
105 <g id="Graphic_25">
106 <text transform="translate(373 207.608)" fill="black">
107 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.309" y="13">The address of</tspan>
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>
109 </text>
110 </g>
111 </g>
112 </g>
113 </svg>