@@ -14,7 +14,7 @@
1414 viewBox="0 0 744.09448819 1052.3622047"
1515 id="svg2"
1616 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
1818 sodipodi:docname="tree.svg">
1919 <defs
2020 id="defs4">
@@ -32,21 +32,6 @@
3232 d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
3333 id="path5206" />
3434 </marker>
35− <marker
36− inkscape:stockid="Arrow1Mend"
37− orient="auto"
38− refY="0.0"
39− refX="0.0"
40− id="Arrow1Mend"
41− style="overflow:visible;"
42− inkscape:isstock="true"
43− inkscape:collect="always">
44− <path
45− id="path4179"
46− d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
47− style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
48− transform="scale(0.4) rotate(180) translate(10,0)" />
49− </marker>
5035 </defs>
5136 <sodipodi:namedview
5237 id="base"
@@ -57,13 +42,13 @@
5742 inkscape:pageshadow="2"
5843 inkscape:zoom="1"
5944 inkscape:cx="383.03443"
60− inkscape:cy="520"
45+ inkscape:cy="690.88799"
6146 inkscape:document-units="px"
6247 inkscape:current-layer="layer1"
6348 showgrid="false"
64− inkscape:window-width="1406"
65− inkscape:window-height="1011"
66− inkscape:window-x="-4"
49+ inkscape:window-width="1129"
50+ inkscape:window-height="730"
51+ inkscape:window-x="671"
6752 inkscape:window-y="0"
6853 inkscape:window-maximized="0" />
6954 <metadata
@@ -74,7 +59,7 @@
7459 <dc:format>image/svg+xml</dc:format>
7560 <dc:type
7661 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
77− <dc:title></dc:title>
62+ <dc:title />
7863 </cc:Work>
7964 </rdf:RDF>
8065 </metadata>
@@ -84,97 +69,144 @@
8469 id="layer1">
8570 <text
8671 xml:space="preserve"
87− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
88− x="221"
89− y="433.36221"
72+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
73+ x="348.5"
74+ y="334.92474"
9075 id="text4136"
91− sodipodi:linespacing="125%"
9276 inkscape:export-xdpi="61.120499"
9377 inkscape:export-ydpi="61.120499"><tspan
9478 sodipodi:role="line"
9579 id="tspan4138"
96− x="221"
97− y="433.36221"
98− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1">λ n:t1 . h:t2</tspan></text>
80+ x="348.5"
81+ y="334.92474"
82+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;fill-opacity:1">{hole2} :Nat->Nat</tspan></text>
9983 <text
100− xml:space="preserve"
101− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
102− x="260"
103− y="366.36221"
104− id="text4144"
105− sodipodi:linespacing="125%"
106− inkscape:export-xdpi="61.120499"
107− inkscape:export-ydpi="61.120499"><tspan
108− sodipodi:role="line"
109− id="tspan4146"
110− x="260"
111− y="366.36221"
112− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1">x</tspan></text>
113− <path
114− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
115− d="m 268,373.3622 13,43"
116− id="path4150"
117− inkscape:connector-curvature="0"
118− sodipodi:nodetypes="cc"
119− inkscape:export-xdpi="61.120499"
120− inkscape:export-ydpi="61.120499" />
121− <text
122− sodipodi:linespacing="125%"
12384 id="text4152"
124− y="466.36221"
125− x="161"
126− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
85+ y="364.17471"
86+ x="380.375"
87+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
12788 xml:space="preserve"
12889 inkscape:export-xdpi="61.120499"
12990 inkscape:export-ydpi="61.120499"><tspan
130− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"
131− y="466.36221"
132− x="161"
91+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"
92+ y="364.17471"
93+ x="380.375"
13394 id="tspan4154"
13495 sodipodi:role="line">intro `{{x}}</tspan></text>
13596 <text
13697 xml:space="preserve"
137− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
138− x="322"
139− y="468.36221"
98+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
99+ x="381.0625"
100+ y="470.23721"
140101 id="text4156"
141− sodipodi:linespacing="125%"
142102 inkscape:export-xdpi="61.120499"
143103 inkscape:export-ydpi="61.120499"><tspan
144104 sodipodi:role="line"
145105 id="tspan4158"
146− x="322"
147− y="468.36221"
148− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1">solve</tspan></text>
106+ x="381.0625"
107+ y="470.23721"
108+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1">solve</tspan></text>
149109 <text
150− sodipodi:linespacing="125%"
151110 id="text4160"
152− y="325.36221"
153− x="224"
154− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
111+ y="414.42471"
112+ x="380.5625"
113+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
155114 xml:space="preserve"
156115 inkscape:export-xdpi="61.120499"
157116 inkscape:export-ydpi="61.120499"><tspan
158− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"
159− y="325.36221"
160− x="224"
117+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"
118+ y="414.42471"
119+ x="380.5625"
161120 id="tspan4162"
162121 sodipodi:role="line">fill (Var `{{x}})</tspan></text>
163122 <path
164− sodipodi:nodetypes="cc"
123+ style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)"
124+ d="m 371.4375,343.4872 0.875,29.125"
125+ id="path5202"
165126 inkscape:connector-curvature="0"
166− id="path4164"
167− d="m 179,448.3622 76,-117"
168− style="fill:none;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
127+ sodipodi:nodetypes="cc"
169128 inkscape:export-xdpi="61.120499"
170129 inkscape:export-ydpi="61.120499" />
130+ <path
131+ inkscape:export-ydpi="61.120499"
132+ inkscape:export-xdpi="61.120499"
133+ sodipodi:nodetypes="cc"
134+ inkscape:connector-curvature="0"
135+ id="path89"
136+ d="m 371.4375,395.9872 0.875,29.125"
137+ style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)" />
171138 <path
172139 style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)"
173− d="m 273,330.3622 59,121"
174− id="path5202"
140+ d="m 371.4375,450.3622 0.875,29.125"
141+ id="path91"
175142 inkscape:connector-curvature="0"
176143 sodipodi:nodetypes="cc"
177144 inkscape:export-xdpi="61.120499"
178145 inkscape:export-ydpi="61.120499" />
146+ <text
147+ inkscape:export-ydpi="61.120499"
148+ inkscape:export-xdpi="61.120499"
149+ id="text95"
150+ y="332.11224"
151+ x="295.0625"
152+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
153+ xml:space="preserve"><tspan
154+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
155+ y="332.11224"
156+ x="295.0625"
157+ id="tspan93"
158+ sodipodi:role="line">state</tspan></text>
159+ <text
160+ xml:space="preserve"
161+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
162+ x="295.0625"
163+ y="386.48724"
164+ id="text99"
165+ inkscape:export-xdpi="61.120499"
166+ inkscape:export-ydpi="61.120499"><tspan
167+ sodipodi:role="line"
168+ id="tspan97"
169+ x="295.0625"
170+ y="386.48724"
171+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1">state</tspan></text>
172+ <text
173+ inkscape:export-ydpi="61.120499"
174+ inkscape:export-xdpi="61.120499"
175+ id="text103"
176+ y="444.61224"
177+ x="295.0625"
178+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
179+ xml:space="preserve"><tspan
180+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
181+ y="444.61224"
182+ x="295.0625"
183+ id="tspan101"
184+ sodipodi:role="line">state</tspan></text>
185+ <text
186+ inkscape:export-ydpi="61.120499"
187+ inkscape:export-xdpi="61.120499"
188+ id="text3796"
189+ y="389.29974"
190+ x="345.6875"
191+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
192+ xml:space="preserve"><tspan
193+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;fill-opacity:1"
194+ y="389.29974"
195+ x="345.6875"
196+ id="tspan3794"
197+ sodipodi:role="line">λ x:Nat . ? {hole 2}</tspan></text>
198+ <text
199+ xml:space="preserve"
200+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
201+ x="344.75"
202+ y="442.73724"
203+ id="text3800"
204+ inkscape:export-xdpi="61.120499"
205+ inkscape:export-ydpi="61.120499"><tspan
206+ sodipodi:role="line"
207+ id="tspan3798"
208+ x="344.75"
209+ y="442.73724"
210+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;fill-opacity:1">λ x:Nat . x</tspan></text>
179211 </g>
180212</svg>