on master help sign in
add svg diagram
6255c0dMartin Baker
docs/image/compareToProofAssist.svg+41−32
@@ -18,6 +18,20 @@
18 sodipodi:docname="compareToProofAssist.svg">
18 sodipodi:docname="compareToProofAssist.svg">
19 <defs
19 <defs
20 id="defs4">
20 id="defs4">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker4251"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow1Mend">
29+ <path
30+ transform="scale(0.4) rotate(180) translate(10,0)"
31+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
32+ 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 "
33+ id="path4253" />
34+ </marker>
21 <marker
35 <marker
22 inkscape:stockid="Arrow1Mend"
36 inkscape:stockid="Arrow1Mend"
23 orient="auto"
37 orient="auto"
@@ -89,7 +103,7 @@
89 <dc:format>image/svg+xml</dc:format>
103 <dc:format>image/svg+xml</dc:format>
90 <dc:type
104 <dc:type
91 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
105 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
92− <dc:title></dc:title>
106+ <dc:title />
93 </cc:Work>
107 </cc:Work>
94 </rdf:RDF>
108 </rdf:RDF>
95 </metadata>
109 </metadata>
@@ -167,56 +181,37 @@
167 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;marker-end:url(#marker4436)"
181 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;marker-end:url(#marker4436)"
168 inkscape:export-xdpi="61.120499"
182 inkscape:export-xdpi="61.120499"
169 inkscape:export-ydpi="61.120499" />
183 inkscape:export-ydpi="61.120499" />
170− <text
171− sodipodi:linespacing="125%"
172− id="text4998"
173− y="307.36221"
174− x="306"
175− style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
176− xml:space="preserve"
177− inkscape:export-xdpi="61.120499"
178− inkscape:export-ydpi="61.120499"><tspan
179− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
180− y="307.36221"
181− x="306"
182− id="tspan5000"
183− sodipodi:role="line">High level program</tspan><tspan
184− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
185− y="326.11221"
186− x="306"
187− sodipodi:role="line"
188− id="tspan5058">(unification algorithm)</tspan></text>
189 <text
184 <text
190 xml:space="preserve"
185 xml:space="preserve"
191 style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
186 style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
192− x="316"
187+ x="314"
193− y="369.36221"
188+ y="326.36221"
194 id="text5002"
189 id="text5002"
195 sodipodi:linespacing="125%"
190 sodipodi:linespacing="125%"
196 inkscape:export-xdpi="61.120499"
191 inkscape:export-xdpi="61.120499"
197 inkscape:export-ydpi="61.120499"><tspan
192 inkscape:export-ydpi="61.120499"><tspan
198 sodipodi:role="line"
193 sodipodi:role="line"
199 id="tspan5004"
194 id="tspan5004"
200− x="316"
195+ x="314"
201− y="369.36221"
196+ y="326.36221"
202− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Tactics</tspan></text>
197+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Idris source</tspan></text>
203 <text
198 <text
204 sodipodi:linespacing="125%"
199 sodipodi:linespacing="125%"
205 id="text5006"
200 id="text5006"
206− y="416.36221"
201+ y="413.36221"
207− x="315"
202+ x="281"
208 style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
203 style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
209 xml:space="preserve"
204 xml:space="preserve"
210 inkscape:export-xdpi="61.120499"
205 inkscape:export-xdpi="61.120499"
211 inkscape:export-ydpi="61.120499"><tspan
206 inkscape:export-ydpi="61.120499"><tspan
212 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
207 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
213− y="416.36221"
208+ y="413.36221"
214− x="315"
209+ x="281"
215 id="tspan5008"
210 id="tspan5008"
216 sodipodi:role="line">fill holes</tspan><tspan
211 sodipodi:role="line">fill holes</tspan><tspan
217 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
212 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
218− y="435.11221"
213+ y="432.11221"
219− x="315"
214+ x="281"
220 sodipodi:role="line"
215 sodipodi:role="line"
221 id="tspan5060">(implicit variables, etc)</tspan></text>
216 id="tspan5060">(implicit variables, etc)</tspan></text>
222 <text
217 <text
@@ -237,7 +232,7 @@
237 inkscape:connector-curvature="0"
232 inkscape:connector-curvature="0"
238 id="path5014"
233 id="path5014"
239 d="m 342,330.3622 0,22"
234 d="m 342,330.3622 0,22"
240− 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;marker-end:url(#Arrow1Mend)"
235+ 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;marker-end:url(#marker4251)"
241 inkscape:export-xdpi="61.120499"
236 inkscape:export-xdpi="61.120499"
242 inkscape:export-ydpi="61.120499" />
237 inkscape:export-ydpi="61.120499" />
243 <path
238 <path
@@ -247,5 +242,19 @@
247 inkscape:connector-curvature="0"
242 inkscape:connector-curvature="0"
248 inkscape:export-xdpi="61.120499"
243 inkscape:export-xdpi="61.120499"
249 inkscape:export-ydpi="61.120499" />
244 inkscape:export-ydpi="61.120499" />
245+ <text
246+ inkscape:export-ydpi="61.120499"
247+ inkscape:export-xdpi="61.120499"
248+ sodipodi:linespacing="125%"
249+ id="text4247"
250+ y="369.36221"
251+ x="317"
252+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
253+ xml:space="preserve"><tspan
254+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
255+ y="369.36221"
256+ x="317"
257+ id="tspan4249"
258+ sodipodi:role="line">Tactics</tspan></text>
250 </g>
259 </g>
251</svg>
260</svg>