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

annotate fig/ord-od-mapping.svg @ 325:1a54dbe1ea4c

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 Sat, 04 Jul 2020 22:48:49 +0900
parents 9ccf8514c323
children 4cbcf71b09c4
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">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 <svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="37 -5 449 664" width="449" height="664">
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 <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
6 <font-face-src>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 <font-face-name name="HelveticaNeue"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 </font-face-src>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 </font-face>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 <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">
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" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" 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 8 0 L 0 -3 L 0 3 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>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 </defs>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 <metadata> Produced by OmniGraffle 7.12.1
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 <dc:date>2019-11-28 05:45:48 +0000</dc:date>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 </metadata>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 <title>Canvas 1</title>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 <rect fill="white" x="37" y="-5" width="449" height="664"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 <g id="Canvas_1: Layer 1">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 <title>Layer 1</title>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 <g id="Graphic_18">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 <path d="M 159 49 L 186.21835 171 L 213.4367 49 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
32 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 <g id="Graphic_17">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 <path d="M 159 171 L 186.21835 293 L 213.4367 171 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
36 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 <g id="Graphic_16">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 <path d="M 159 293 L 186.21835 415 L 213.4367 293 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
40 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 <g id="Graphic_15">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" fill="white"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 <path d="M 159 415 L 186.21835 537 L 213.4367 415 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
44 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 <g id="Graphic_12">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 <circle cx="186.21835" cy="16.5" r="6.50001038636233" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 <circle cx="186.21835" cy="16.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
48 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 <g id="Graphic_6">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 <text transform="translate(155.245 553)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 <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
52 </text>
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_5">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 <text transform="translate(337 536)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 <g id="Graphic_20">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 <text transform="translate(406.77 98.76035)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">max</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x=".343" y="29.392">= all</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 </text>
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_21">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 <text transform="translate(440.722 509.608)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 <g id="Graphic_22">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 <text transform="translate(42 .10800171)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="23.261" y="13">Ordinal</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="29.392">max != Ordinal</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 </text>
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_23">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 <line x1="255.471" y1="430.5664" x2="255.471" y2="534.5664" 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_24">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 <line x1="236" y1="180" x2="236" y2="535" 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
82 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 <g id="Graphic_25">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 <text transform="translate(99 509.608)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 <g id="Line_27">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 <line x1="127" y1="535" x2="484.894" y2="535" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 <g id="Line_28">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 <line x1="389" y1="140" x2="255.471" y2="430.5664" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 <g id="Line_31">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 <line x1="389" y1="140" x2="236" y2="180.9972" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 <g id="Graphic_32">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 <circle cx="242.5" cy="146.5" r="6.50001038636233" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 <circle cx="242.5" cy="146.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
100 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 <g id="Graphic_33">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 <circle cx="255.971" cy="397.5" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 <circle cx="255.971" cy="397.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
104 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 <g id="Graphic_34">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 <circle cx="383.5" cy="115.15234" r="6.50001038636234" fill="black"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 <circle cx="383.5" cy="115.15234" 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
108 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 <g id="Line_35">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 <line x1="250.3103" y1="144.76358" x2="375.6897" y2="116.88876" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 <g id="Line_36">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 <line x1="380.20605" y1="122.44512" x2="259.26495" y2="390.20723" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 <g id="Line_40">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 <line x1="372.3718" y1="630.664" x2="246.9" y2="630.664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 <g id="Line_39">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 <line x1="188" y1="622.218" x2="365.575" y2="622.218" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
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_38">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 <text transform="translate(253.792 599.232)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">non-order preserving</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 <g id="Graphic_37">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 <text transform="translate(260.471 636.664)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">order preserving</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 <g id="Line_41">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 <line x1="107" y1="356" x2="107" y2="274.47422" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 <g id="Graphic_44">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 <text transform="translate(45.888 318.13017)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="4973799e-19" y="13">larger</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 <g id="Line_46">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 <line x1="399" y1="370" x2="414.93724" y2="273.84283" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 <g id="Graphic_45">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 <text transform="translate(433.218 318.13017)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">defined</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.687" y="29.392">by</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 <g id="Line_47">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 <line x1="399" y1="450" x2="399" y2="375.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 <g id="Line_48">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 <line x1="416.556" y1="474.9336" x2="416.556" y2="400.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
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="Line_49">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 <line x1="407.778" y1="507.9336" x2="407.778" y2="433.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 <g id="Line_50">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 <line x1="391.54" y1="209.0664" x2="400.23237" y2="153.77986" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 <g id="Line_51">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 <line x1="412" y1="243.9336" x2="412" y2="169.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 <g id="Line_52">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 <line x1="391.54" y1="307" x2="391.54" y2="218.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
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_53">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 <line x1="416.556" y1="264.07607" x2="431.52065" y2="216.44483" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
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="Line_54">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 <line x1="399" y1="366.0664" x2="392.7805" y2="316.82197" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 <g id="Graphic_55">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 <text transform="translate(107 610.272)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">Total order</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 <g id="Graphic_56">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 <text transform="translate(395 614.522)" fill="black">
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="17053026e-20" y="13">Partial order</tspan>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 </text>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 </g>
9ccf8514c323 add documents
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 </svg>