%!PS-Adobe-2.0 %%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) %%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) %%BoundingBox: 35 35 577 125 %%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 /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 { } 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 /layercolorseq [ % layer color sequence - darkest to lightest [0 0 0] [.2 .8 .8] [.4 .8 .8] [.6 .8 .8] [.8 .8 .8] ] def /setlayer {/maxlayer exch def /curlayer exch def layercolorseq curlayer 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 125 %%PageOrientation: Portrait gsave 35 35 542 90 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0.6136 set_scale 0 0 translate 0 rotate [ /CropBox [36 36 577 125] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Tactic_debug gsave 10 dict begin 66 126 57 18 ellipse_path stroke gsave 10 dict begin 66 121 moveto 93 -0.5 (Tactic_debug) alignedtext end grestore end grestore % Tacmach gsave 10 dict begin 217 72 42 18 ellipse_path stroke gsave 10 dict begin 217 67 moveto 63 -0.5 (Tacmach) alignedtext end grestore end grestore % Tactic_debug -> Tacmach newpath 104 112 moveto 126 104 154 95 176 87 curveto stroke 0.000 0.000 0.000 edgecolor newpath 174 85 moveto 184 84 lineto 176 90 lineto closepath fill 0.000 0.000 0.000 edgecolor % Refiner gsave 10 dict begin 348 45 37 18 ellipse_path stroke gsave 10 dict begin 348 40 moveto 53 -0.5 (Refiner) alignedtext end grestore end grestore % Tacmach -> Refiner newpath 255 64 moveto 270 61 288 57 304 54 curveto stroke 0.000 0.000 0.000 edgecolor newpath 303 52 moveto 313 52 lineto 304 57 lineto closepath fill 0.000 0.000 0.000 edgecolor % Logic gsave 10 dict begin 452 45 30 18 ellipse_path stroke gsave 10 dict begin 452 40 moveto 38 -0.5 (Logic) alignedtext end grestore end grestore % Refiner -> Logic newpath 386 45 moveto 395 45 404 45 412 45 curveto stroke 0.000 0.000 0.000 edgecolor newpath 412 43 moveto 422 45 lineto 412 48 lineto closepath fill 0.000 0.000 0.000 edgecolor % Proof_trees gsave 10 dict begin 569 45 51 18 ellipse_path stroke gsave 10 dict begin 569 40 moveto 80 -0.5 (Proof_trees) alignedtext end grestore end grestore % Logic -> Proof_trees newpath 482 45 moveto 490 45 499 45 508 45 curveto stroke 0.000 0.000 0.000 edgecolor newpath 508 43 moveto 518 45 lineto 508 48 lineto closepath fill 0.000 0.000 0.000 edgecolor % Proof_type gsave 10 dict begin 707 45 50 18 ellipse_path stroke gsave 10 dict begin 707 40 moveto 79 -0.5 (Proof_type) alignedtext end grestore end grestore % Tacexpr gsave 10 dict begin 833 45 39 18 ellipse_path stroke gsave 10 dict begin 833 40 moveto 56 -0.5 (Tacexpr) alignedtext end grestore end grestore % Proof_type -> Tacexpr newpath 758 45 moveto 767 45 775 45 784 45 curveto stroke 0.000 0.000 0.000 edgecolor newpath 784 43 moveto 794 45 lineto 784 48 lineto closepath fill 0.000 0.000 0.000 edgecolor % Proof_trees -> Proof_type newpath 620 45 moveto 629 45 637 45 646 45 curveto stroke 0.000 0.000 0.000 edgecolor newpath 646 43 moveto 656 45 lineto 646 48 lineto closepath fill 0.000 0.000 0.000 edgecolor % Pfedit gsave 10 dict begin 66 18 31 18 ellipse_path stroke gsave 10 dict begin 66 13 moveto 41 -0.5 (Pfedit) alignedtext end grestore end grestore % Pfedit -> Tacmach newpath 93 28 moveto 115 36 149 48 175 57 curveto stroke 0.000 0.000 0.000 edgecolor newpath 175 54 moveto 184 60 lineto 174 59 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evar_refiner gsave 10 dict begin 217 18 56 18 ellipse_path stroke gsave 10 dict begin 217 13 moveto 91 -0.5 (Evar_refiner) alignedtext end grestore end grestore % Pfedit -> Evar_refiner newpath 98 18 moveto 113 18 132 18 150 18 curveto stroke 0.000 0.000 0.000 edgecolor newpath 150 16 moveto 160 18 lineto 150 21 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evar_refiner -> Refiner newpath 265 28 moveto 278 30 291 33 304 36 curveto stroke 0.000 0.000 0.000 edgecolor newpath 304 33 moveto 313 38 lineto 303 38 lineto closepath fill 0.000 0.000 0.000 edgecolor % Clenv gsave 10 dict begin 66 72 31 18 ellipse_path stroke gsave 10 dict begin 66 67 moveto 40 -0.5 (Clenv) alignedtext end grestore end grestore % Clenv -> Tacmach newpath 97 72 moveto 117 72 142 72 164 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 164 70 moveto 174 72 lineto 164 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Clenv -> Evar_refiner newpath 93 62 moveto 114 55 144 44 170 34 curveto stroke 0.000 0.000 0.000 edgecolor newpath 169 32 moveto 179 31 lineto 170 37 lineto closepath fill 0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer %%EndPage: 1 %%Trailer %%Pages: 1 end restore %%EOF