2 %%Creator: dot version 2.2.1 (Tue Apr 12 00:03:35 UTC 2005)
3 %%For: (sacerdot) Claudio Sacerdoti Coen,,,
6 %%BoundingBox: 35 35 461 649
15 /EncodingVector 256 array def
18 ISOLatin1Encoding 0 255 getinterval putinterval
71 % Set up ISO Latin 1 character encoding
73 dup dup findfont dup length dict begin
74 { 1 index /FID ne { def }{ pop pop } ifelse
76 /Encoding EncodingVector def
77 currentdict end definefont
79 /Times-Roman starnetISO def
80 /Times-Italic starnetISO def
81 /Times-Bold starnetISO def
82 /Times-BoldItalic starnetISO def
83 /Helvetica starnetISO def
84 /Helvetica-Oblique starnetISO def
85 /Helvetica-Bold starnetISO def
86 /Helvetica-BoldOblique starnetISO def
87 /Courier starnetISO def
88 /Courier-Oblique starnetISO def
89 /Courier-Bold starnetISO def
90 /Courier-BoldOblique starnetISO def
94 %%BeginResource: procset graphviz 0 0
95 /coord-font-family /Times-Roman def
96 /default-font-family /Times-Roman def
97 /coordfont coord-font-family findfont 8 scalefont def
99 /InvScaleFactor 1.0 def
101 dup 1 exch div /InvScaleFactor exch def
106 /solid { [] 0 setdash } bind def
107 /dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
108 /dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
109 /invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
110 /bold { 2 setlinewidth } bind def
112 /unfilled { } bind def
113 /rounded { } bind def
114 /diagonals { } bind def
116 % hooks for setting color
117 /nodecolor { sethsbcolor } bind def
118 /edgecolor { sethsbcolor } bind def
119 /graphcolor { sethsbcolor } bind def
120 /nopcolor {pop pop pop} bind def
122 /beginpage { % i j npages
131 (\() show i str cvs show (,) show j str cvs show (\)) show
141 % draw aligned label in bounding box aligned to current point
142 /alignedtext { % width adj text
148 text stringwidth pop adj mul 0 rmoveto
155 /boxprim { % xcorner ycorner xsize ysize
178 /endpage { showpage } bind def
182 [ % layer color sequence - darkest to lightest
191 /layerlen layercolorseq length def
193 /setlayer {/maxlayer exch def /curlayer exch def
194 layercolorseq curlayer 1 sub layerlen mod get
195 aload pop sethsbcolor
196 /nodecolor {nopcolor} def
197 /edgecolor {nopcolor} def
198 /graphcolor {nopcolor} def
201 /onlayer { curlayer ne {invis} if } def
217 14 default-font-family set_font
219 % /arrowlength 10 def
222 % make sure pdfmark is harmless for PS-interpreters other than Distiller
223 /pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
224 % make '<<' and '>>' safe on PS Level 1 devices
225 /languagelevel where {pop languagelevel}{1} ifelse
227 userdict (<<) cvn ([) cvn load put
228 userdict (>>) cvn ([) cvn load put
233 %%PageBoundingBox: 36 36 461 649
234 %%PageOrientation: Portrait
236 35 35 426 614 boxprim clip newpath
239 0 0 translate 0 rotate
240 0.000 0.000 0.000 graphcolor
241 14.00 /Times-Roman set_font
245 164 594 57 18 ellipse_path
250 [6.96 6.24 4.56 6.24 10.8 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96]
257 164 522 68 18 ellipse_path
262 [6.24 3.84 6.24 6.96 6.96 3.84 5.52 6.24 10.8 6.96 3.84 6.96 6.96 6.24 3.84 3.84 6.96 6.96]
267 % paramodulation -> cic_disambiguation
268 newpath 164 576 moveto
269 164 568 164 559 164 550 curveto
274 0.000 0.000 0.000 edgecolor
275 newpath 168 550 moveto
280 0.000 0.000 0.000 edgecolor
281 newpath 168 550 moveto
290 48 378 48 18 ellipse_path
295 [6.24 3.84 6.24 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96]
300 % cic_disambiguation -> cic_notation
301 newpath 128 507 moveto
302 111 498 91 485 77 468 curveto
303 64 450 56 425 52 406 curveto
308 0.000 0.000 0.000 edgecolor
309 newpath 55 405 moveto
314 0.000 0.000 0.000 edgecolor
315 newpath 55 405 moveto
324 275 450 31 18 ellipse_path
329 [3.84 6.24 6.24 3.84 3.84 6.24 5.52]
334 % cic_disambiguation -> tactics
335 newpath 190 505 moveto
336 207 494 228 480 246 469 curveto
341 0.000 0.000 0.000 edgecolor
342 newpath 248 472 moveto
347 0.000 0.000 0.000 edgecolor
348 newpath 248 472 moveto
357 242 306 68 18 ellipse_path
362 [6.24 3.84 6.24 6.96 6.96 4.56 6.96 6.96 4.56 6.96 6.24 6.96 6.24 6.24 6.96 3.84 6.96 6.96]
367 % cic_notation -> cic_proof_checking
368 newpath 82 365 moveto
369 113 354 158 337 192 325 curveto
374 0.000 0.000 0.000 edgecolor
375 newpath 194 328 moveto
380 0.000 0.000 0.000 edgecolor
381 newpath 194 328 moveto
390 48 306 48 18 ellipse_path
395 [6.96 3.84 4.56 6.96 6.96 10.8 6.24 6.24 4.56 6.96 5.52]
400 % cic_notation -> utf8_macros
401 newpath 48 360 moveto
402 48 352 48 343 48 334 curveto
407 0.000 0.000 0.000 edgecolor
408 newpath 52 334 moveto
413 0.000 0.000 0.000 edgecolor
414 newpath 52 334 moveto
423 386 378 38 18 ellipse_path
428 [10.8 6.24 3.84 6.24 6.96 6.24 3.84 6.24]
433 % tactics -> metadata
434 newpath 296 436 moveto
435 312 426 336 411 355 399 curveto
440 0.000 0.000 0.000 edgecolor
441 newpath 357 402 moveto
446 0.000 0.000 0.000 edgecolor
447 newpath 357 402 moveto
456 275 378 55 18 ellipse_path
461 [6.24 3.84 6.24 6.96 6.96 6.96 3.84 4.56 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
466 % tactics -> cic_unification
467 newpath 275 432 moveto
468 275 424 275 415 275 406 curveto
473 0.000 0.000 0.000 edgecolor
474 newpath 279 406 moveto
479 0.000 0.000 0.000 edgecolor
480 newpath 279 406 moveto
487 % cic_transformations
489 154 450 68 18 ellipse_path
493 (cic_transformations)
494 [6.24 3.84 6.24 6.96 3.84 4.56 6.24 6.96 5.52 4.56 6.96 4.56 10.8 6.24 3.84 3.84 6.96 6.96 5.52]
499 % cic_transformations -> cic_notation
500 newpath 129 433 moveto
501 115 423 95 410 79 399 curveto
506 0.000 0.000 0.000 edgecolor
507 newpath 81 396 moveto
512 0.000 0.000 0.000 edgecolor
513 newpath 81 396 moveto
522 158 378 44 18 ellipse_path
527 [6.24 3.84 6.24 6.96 6.96 10.8 6.96 6.96 6.24]
532 % cic_transformations -> cic_omdoc
533 newpath 155 432 moveto
534 156 424 156 415 156 406 curveto
539 0.000 0.000 0.000 edgecolor
540 newpath 159 406 moveto
545 0.000 0.000 0.000 edgecolor
546 newpath 159 406 moveto
553 % cic_omdoc -> cic_proof_checking
554 newpath 177 362 moveto
555 188 352 202 340 214 330 curveto
560 0.000 0.000 0.000 edgecolor
561 newpath 217 332 moveto
566 0.000 0.000 0.000 edgecolor
567 newpath 217 332 moveto
576 292 234 29 18 ellipse_path
581 [6.96 6.24 3.84 3.84 6.24 4.56]
586 % cic_proof_checking -> getter
587 newpath 254 288 moveto
588 260 280 267 269 274 259 curveto
593 0.000 0.000 0.000 edgecolor
594 newpath 277 261 moveto
599 0.000 0.000 0.000 edgecolor
600 newpath 277 261 moveto
609 208 234 27 18 ellipse_path
619 % cic_proof_checking -> cic
620 newpath 233 288 moveto
621 229 280 225 270 220 261 curveto
626 0.000 0.000 0.000 edgecolor
627 newpath 223 260 moveto
632 0.000 0.000 0.000 edgecolor
633 newpath 223 260 moveto
640 % metadata -> cic_proof_checking
641 newpath 360 365 moveto
642 339 354 308 339 283 327 curveto
647 0.000 0.000 0.000 edgecolor
648 newpath 284 324 moveto
653 0.000 0.000 0.000 edgecolor
654 newpath 284 324 moveto
663 386 234 34 18 ellipse_path
668 [6.96 10.8 6.96 5.52 6.96 3.84]
674 newpath 386 360 moveto
675 386 335 386 291 386 262 curveto
680 0.000 0.000 0.000 edgecolor
681 newpath 390 262 moveto
686 0.000 0.000 0.000 edgecolor
687 newpath 390 262 moveto
694 % cic_unification -> cic_proof_checking
695 newpath 267 360 moveto
696 263 352 259 342 254 333 curveto
701 0.000 0.000 0.000 edgecolor
702 newpath 257 332 moveto
707 0.000 0.000 0.000 edgecolor
708 newpath 257 332 moveto
717 386 162 35 18 ellipse_path
722 [4.56 6.24 6.96 3.84 5.52 3.84 4.56 6.96]
728 newpath 386 216 moveto
729 386 208 386 199 386 190 curveto
734 0.000 0.000 0.000 edgecolor
735 newpath 390 190 moveto
740 0.000 0.000 0.000 edgecolor
741 newpath 390 190 moveto
750 208 162 45 18 ellipse_path
755 [6.96 4.56 3.84 10.8 6.24 6.96 6.24 6.96 6.24 4.56]
760 % getter -> urimanager
761 newpath 275 219 moveto
762 263 209 248 196 235 185 curveto
767 0.000 0.000 0.000 edgecolor
768 newpath 237 182 moveto
773 0.000 0.000 0.000 edgecolor
774 newpath 237 182 moveto
782 newpath 311 220 moveto
783 325 210 343 195 359 183 curveto
788 0.000 0.000 0.000 edgecolor
789 newpath 361 186 moveto
794 0.000 0.000 0.000 edgecolor
795 newpath 361 186 moveto
804 302 162 31 18 ellipse_path
809 [3.84 6.96 6.96 6.96 6.24 4.56]
815 newpath 295 216 moveto
816 296 208 297 199 298 190 curveto
821 0.000 0.000 0.000 edgecolor
822 newpath 301 190 moveto
827 0.000 0.000 0.000 edgecolor
828 newpath 301 190 moveto
837 260 90 27 18 ellipse_path
848 newpath 189 221 moveto
849 176 212 161 197 154 180 curveto
850 147 165 145 157 154 144 curveto
851 169 119 199 105 224 98 curveto
856 0.000 0.000 0.000 edgecolor
857 newpath 225 101 moveto
862 0.000 0.000 0.000 edgecolor
863 newpath 225 101 moveto
871 newpath 208 216 moveto
872 208 208 208 199 208 190 curveto
877 0.000 0.000 0.000 edgecolor
878 newpath 212 190 moveto
883 0.000 0.000 0.000 edgecolor
884 newpath 212 190 moveto
893 260 18 29 18 ellipse_path
898 [6.24 6.96 3.84 3.84 3.84 6.96]
904 newpath 260 72 moveto
905 260 64 260 55 260 46 curveto
910 0.000 0.000 0.000 edgecolor
911 newpath 264 46 moveto
916 0.000 0.000 0.000 edgecolor
917 newpath 264 46 moveto
925 newpath 362 148 moveto
926 342 137 312 120 290 107 curveto
931 0.000 0.000 0.000 edgecolor
932 newpath 291 104 moveto
937 0.000 0.000 0.000 edgecolor
938 newpath 291 104 moveto