diff options
Diffstat (limited to 'dev/doc/proofs.dep.ps')
| -rw-r--r-- | dev/doc/proofs.dep.ps | 638 |
1 files changed, 0 insertions, 638 deletions
diff --git a/dev/doc/proofs.dep.ps b/dev/doc/proofs.dep.ps deleted file mode 100644 index 0e78f422..00000000 --- a/dev/doc/proofs.dep.ps +++ /dev/null @@ -1,638 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 577 136 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 577 136 -%%PageOrientation: Portrait -gsave -35 35 542 101 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0.6923 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font - -% Tactic_debug -gsave 10 dict begin -163 72 51 18 ellipse_path -stroke -gsave 10 dict begin -125 67 moveto -(Tactic_debug) -[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96] -xshow -end grestore -end grestore - -% Refiner -gsave 10 dict begin -287 72 34 18 ellipse_path -stroke -gsave 10 dict begin -266 67 moveto -(Refiner) -[9.12 6.24 4.8 3.84 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Tactic_debug -> Refiner -newpath 214 72 moveto -223 72 233 72 243 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 243 76 moveto -253 72 lineto -243 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 243 76 moveto -253 72 lineto -243 69 lineto -closepath -stroke -end grestore - -% Logic -gsave 10 dict begin -390 72 30 18 ellipse_path -stroke -gsave 10 dict begin -373 67 moveto -(Logic) -[8.4 6.96 6.96 3.84 6.24] -xshow -end grestore -end grestore - -% Refiner -> Logic -newpath 321 72 moveto -330 72 340 72 350 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 350 76 moveto -360 72 lineto -350 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 350 76 moveto -360 72 lineto -350 69 lineto -closepath -stroke -end grestore - -% Tacmach -gsave 10 dict begin -163 126 38 18 ellipse_path -stroke -gsave 10 dict begin -137 121 moveto -(Tacmach) -[7.44 6.24 6.24 10.8 6.24 6 6.96] -xshow -end grestore -end grestore - -% Tacmach -> Refiner -newpath 191 114 moveto -209 106 232 96 251 88 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 253 91 moveto -261 84 lineto -250 84 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 253 91 moveto -261 84 lineto -250 84 lineto -closepath -stroke -end grestore - -% Redexpr -gsave 10 dict begin -287 126 36 18 ellipse_path -stroke -gsave 10 dict begin -263 121 moveto -(Redexpr) -[9.12 6.24 6.96 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Tacmach -> Redexpr -newpath 202 126 moveto -214 126 227 126 240 126 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 240 130 moveto -250 126 lineto -240 123 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 240 130 moveto -250 126 lineto -240 123 lineto -closepath -stroke -end grestore - -% Proof_trees -gsave 10 dict begin -502 72 45 18 ellipse_path -stroke -gsave 10 dict begin -469 67 moveto -(Proof_trees) -[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52] -xshow -end grestore -end grestore - -% Logic -> Proof_trees -newpath 420 72 moveto -428 72 437 72 446 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 446 76 moveto -456 72 lineto -446 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 446 76 moveto -456 72 lineto -446 69 lineto -closepath -stroke -end grestore - -% Proof_type -gsave 10 dict begin -628 72 44 18 ellipse_path -stroke -gsave 10 dict begin -597 67 moveto -(Proof_type) -[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24] -xshow -end grestore -end grestore - -% Tacexpr -gsave 10 dict begin -744 72 35 18 ellipse_path -stroke -gsave 10 dict begin -721 67 moveto -(Tacexpr) -[7.44 6.24 6.24 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Proof_type -> Tacexpr -newpath 672 72 moveto -680 72 689 72 698 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 698 76 moveto -708 72 lineto -698 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 698 76 moveto -708 72 lineto -698 69 lineto -closepath -stroke -end grestore - -% Proof_trees -> Proof_type -newpath 548 72 moveto -557 72 565 72 574 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 574 76 moveto -584 72 lineto -574 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 574 76 moveto -584 72 lineto -574 69 lineto -closepath -stroke -end grestore - -% Pfedit -gsave 10 dict begin -38 112 29 18 ellipse_path -stroke -gsave 10 dict begin -21 107 moveto -(Pfedit) -[7.68 4.08 6.24 6.96 3.84 3.84] -xshow -end grestore -end grestore - -% Pfedit -> Tacmach -newpath 67 115 moveto -81 117 99 118 115 120 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 115 123 moveto -125 122 lineto -116 117 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 115 123 moveto -125 122 lineto -116 117 lineto -closepath -stroke -end grestore - -% Evar_refiner -gsave 10 dict begin -163 18 49 18 ellipse_path -stroke -gsave 10 dict begin -127 13 moveto -(Evar_refiner) -[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Pfedit -> Evar_refiner -newpath 53 96 moveto -67 82 90 60 112 45 curveto -116 42 120 40 124 37 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 126 40 moveto -133 32 lineto -123 34 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 126 40 moveto -133 32 lineto -123 34 lineto -closepath -stroke -end grestore - -% Evar_refiner -> Refiner -newpath 195 32 moveto -212 40 233 49 251 57 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 249 60 moveto -260 61 lineto -252 54 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 249 60 moveto -260 61 lineto -252 54 lineto -closepath -stroke -end grestore - -% Clenvtac -gsave 10 dict begin -38 45 38 18 ellipse_path -stroke -gsave 10 dict begin -13 40 moveto -(Clenvtac) -[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24] -xshow -end grestore -end grestore - -% Clenvtac -> Tacmach -newpath 58 61 moveto -73 72 93 87 112 99 curveto -117 102 123 105 128 108 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 127 111 moveto -137 113 lineto -130 105 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 127 111 moveto -137 113 lineto -130 105 lineto -closepath -stroke -end grestore - -% Clenvtac -> Evar_refiner -newpath 73 37 moveto -85 35 98 32 110 29 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 111 32 moveto -120 27 lineto -110 26 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 111 32 moveto -120 27 lineto -110 26 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF |