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

annotate fig/ODandOrdinals.svg @ 947:a028409f5ca2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid memory exhaust
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 31 Oct 2022 15:36:58 +0900
parents 4cbcf71b09c4
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
9ccf8514c323 add documents
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">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
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="68 87 586 582" width="586" height="582">
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 <defs>
9ccf8514c323 add documents
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="-5 -3 6 6" markerWidth="6" markerHeight="6" color="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 <g>
9ccf8514c323 add documents
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"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 </marker>
9ccf8514c323 add documents
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">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 <font-face-src>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 <font-face-name name="HelveticaNeue"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 </font-face-src>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 </font-face>
9ccf8514c323 add documents
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="-1 -3 6 6" markerWidth="6" markerHeight="6" color="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 <g>
9ccf8514c323 add documents
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"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 </marker>
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
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: 273
diff changeset
21 <font-face-src>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
22 <font-face-name name="HelveticaNeue"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
23 </font-face-src>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
24 </font-face>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 </defs>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 <metadata> Produced by OmniGraffle 7.12.1
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
27 <dc:date>2020-07-16 05:25:36 +0000</dc:date>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 </metadata>
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
29 <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 <title>Canvas 1</title>
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
31 <rect fill="white" x="68" y="87" width="586" height="582"/>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 <g id="Canvas_1: Layer 1">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 <title>Layer 1</title>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 <g id="Graphic_6">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 <path d="M 123 129 L 150.21835 251 L 177.4367 129 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 <path d="M 123 129 L 150.21835 251 L 177.4367 129 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 <g id="Graphic_7">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 <path d="M 123 251 L 150.21835 373 L 177.4367 251 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 <path d="M 123 251 L 150.21835 373 L 177.4367 251 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 <g id="Graphic_8">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 <path d="M 123 373 L 150.21835 495 L 177.4367 373 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 <path d="M 123 373 L 150.21835 495 L 177.4367 373 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 <g id="Graphic_9">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 <path d="M 123 495 L 150.21835 617 L 177.4367 495 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 <path d="M 123 495 L 150.21835 617 L 177.4367 495 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 <g id="Graphic_10">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 <ellipse cx="270.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 <ellipse cx="270.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 <g id="Graphic_13">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 <circle cx="154.5" cy="181.5" r="6.50001038636232" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 <circle cx="154.5" cy="181.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 <g id="Graphic_14">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 <circle cx="154.5" cy="272.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 <circle cx="154.5" cy="272.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 <g id="Graphic_15">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 <circle cx="154.5" cy="304.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 <circle cx="154.5" cy="304.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 <g id="Graphic_16">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 <circle cx="154.5" cy="395.5" r="6.50001038636233" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 <circle cx="154.5" cy="395.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 <g id="Graphic_18">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 <circle cx="154.5" cy="424.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 <circle cx="154.5" cy="424.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 <g id="Line_19">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 <line x1="173.9379" y1="409.40815" x2="254.63666" y2="467.1495" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 <g id="Line_20">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 <line x1="176.16929" y1="434.5874" x2="254.55825" y2="471.07884" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 <g id="Line_21">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
81 <line x1="175.39975" y1="181.39705" x2="256" y2="181" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 <g id="Line_22">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
84 <line x1="172.14058" y1="261.28998" x2="256" y2="208" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 <g id="Line_23">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
87 <line x1="170.95411" y1="291.6123" x2="256" y2="225" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 <g id="Graphic_24">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 <circle cx="150.21835" cy="525.5" r="6.50001038636231" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 <circle cx="150.21835" cy="525.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 <g id="Line_25">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
94 <line x1="157.63988" y1="505.96074" x2="256" y2="247" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 <g id="Graphic_26">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 <text transform="translate(119.245 633)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 <g id="Graphic_47">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 <path d="M 426 129 L 453.21835 251 L 480.4367 129 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 <path d="M 426 129 L 453.21835 251 L 480.4367 129 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 <g id="Graphic_46">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 <path d="M 426 251 L 453.21835 373 L 480.4367 251 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 <path d="M 426 251 L 453.21835 373 L 480.4367 251 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 <g id="Graphic_45">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 <path d="M 426 373 L 453.21835 495 L 480.4367 373 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 <path d="M 426 373 L 453.21835 495 L 480.4367 373 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 <g id="Graphic_44">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 <path d="M 426 495 L 453.21835 617 L 480.4367 495 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 <path d="M 426 495 L 453.21835 617 L 480.4367 495 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 <g id="Graphic_43">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 <ellipse cx="573.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 <ellipse cx="573.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 <g id="Graphic_42">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 <ellipse cx="596.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 <ellipse cx="596.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 <g id="Graphic_41">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 <circle cx="457.5" cy="181.5" r="6.50001038636232" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 <circle cx="457.5" cy="181.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 <g id="Graphic_40">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 <circle cx="457.5" cy="272.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 <circle cx="457.5" cy="272.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 <g id="Graphic_39">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 <circle cx="457.5" cy="304.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 <circle cx="457.5" cy="304.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 <g id="Graphic_38">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 <circle cx="457.5" cy="395.5" r="6.50001038636232" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 <circle cx="457.5" cy="395.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 <g id="Graphic_37">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 <circle cx="457.5" cy="424.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 <circle cx="457.5" cy="424.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 <g id="Graphic_31">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 <circle cx="453.21835" cy="525.5" r="6.50001038636233" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 <circle cx="453.21835" cy="525.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 <g id="Graphic_29">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 <text transform="translate(422.245 633)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 <g id="Graphic_28">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
155 <text transform="translate(549.454 584)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
156 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="27711167e-20" y="21">HOD</tspan>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 <g id="Line_48">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 <path d="M 604.7609 469.93216 C 612.0671 467.7524 618.9377 465.6045 624.34375 463.84375 C 637.5514 459.5421 639.2045 425.7619 633.77734 414.5703 C 628.35015 403.3787 602 397 574 385 C 546 373 545 374 507 358 C 469 342 416.78393 326.70416 398 311 C 379.21607 295.29584 381.79114 286.83255 383 279 C 384.20886 271.16745 393.904 266.09114 404 266 C 410.17797 265.94423 421.8459 265.70735 434.2442 267.17386" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 <g id="Graphic_49">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 <circle cx="453.21835" cy="149.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 <circle cx="453.21835" cy="149.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 <g id="Line_50">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 <path d="M 623.554 268.5201 C 625.4985 267.62867 627.6082 266.779 630 266 C 643.2077 261.69835 643.4272 246.1916 638 235 C 632.5728 223.8084 607 201 559 210 C 511 219 518.4367 243 480.4367 227 C 442.4367 211 413.62724 203.75242 394.8433 188.04826 C 376.0594 172.3441 378.63445 163.88081 379.8433 156.04826 C 381.05217 148.21571 390.7473 143.1394 400.8433 143.04826 C 408.3246 142.98073 423.85655 142.6476 438.987 145.39538" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 <g id="Graphic_52">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 <text transform="translate(73.912 92.608)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="18474111e-20" y="21">OD contains Ordinals</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 <g id="Graphic_53">
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
175 <text transform="translate(369.262 92.608)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
176 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">HOD has a name in Ordinals</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
177 </text>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
178 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
179 <g id="Line_56">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
180 <path d="M 256 133 L 256 272.21094 L 277.79297 272.21094 L 278 133" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
181 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
182 <g id="Graphic_57">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
183 <text transform="translate(255.47435 287.884)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
184 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
185 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187 </g>
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
188 <g id="Graphic_58">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
189 <text transform="translate(221 584)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
190 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Hereditarily</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
191 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="20.35" y="47.616">Ordinal</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
192 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="9.361" y="74.231995">Definable</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
193 </text>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
194 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
195 <g id="Graphic_59">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
196 <text transform="translate(297.46 219)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
197 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="7247536e-19" y="13">not bounded</tspan>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
198 </text>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
199 </g>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
200 <g id="Graphic_60">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
201 <text transform="translate(297.46 409.608)" fill="black">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
202 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">bounded</tspan>
273
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 </svg>