%!PS-Adobe-2.0 %%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) %%For: (notin) Jean-Marc Notin,,, %%Title: G %%Pages: (atend) %%BoundingBox: (atend) %%EndComments save %%BeginProlog /DotDict 200 dict def DotDict begin /setupLatin1 { mark /EncodingVector 256 array def EncodingVector 0 ISOLatin1Encoding 0 255 getinterval putinterval EncodingVector 45 /hyphen put % 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 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 setupLatin1 %%Page: 1 1 %%PageBoundingBox: 36 36 576 753 %%PageOrientation: Landscape gsave 36 36 576 753 boxprim clip newpath 0 0 1 beginpage 0.870968 0.870968 set_scale 90 rotate 45.3333 -657.333 translate 0.000 0.000 1.000 graphcolor newpath -4 -4 moveto -4 616 lineto 819 616 lineto 819 -4 lineto closepath fill 0.870968 setlinewidth 0.000 0.000 1.000 graphcolor newpath -4 -4 moveto -4 616 lineto 819 616 lineto 819 -4 lineto closepath stroke % Clenvtac gsave 0.502 1.000 0.820 nodecolor 451 522 37.1753 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 451 522 37.1753 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 451 517 moveto 49 -0.5 (Clenvtac) alignedtext grestore % Evar_refiner gsave 0.502 1.000 0.820 nodecolor 439 450 49.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 450 49.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 445 moveto 72 -0.5 (Evar_refiner) alignedtext grestore % Clenvtac->Evar_refiner gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 448 504 moveto 447 496 445 487 444 478 curveto stroke 0.000 0.000 0.000 edgecolor newpath 447.393 477.119 moveto 442 468 lineto 440.529 478.492 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 447.393 477.119 moveto 442 468 lineto 440.529 478.492 lineto closepath stroke grestore % Tacmach gsave 0.502 1.000 0.820 nodecolor 711 450 38.1754 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 711 450 38.1754 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 711 445 moveto 51 -0.5 (Tacmach) alignedtext grestore % Clenvtac->Tacmach gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 483 513 moveto 530 500 616 476 668 462 curveto stroke 0.000 0.000 0.000 edgecolor newpath 669.427 465.226 moveto 678 459 lineto 667.416 458.521 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 669.427 465.226 moveto 678 459 lineto 667.416 458.521 lineto closepath stroke grestore % Refiner gsave 0.502 1.000 0.820 nodecolor 439 378 34.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 378 34.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 373 moveto 42 -0.5 (Refiner) alignedtext grestore % Evar_refiner->Refiner gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 439 432 moveto 439 424 439 415 439 406 curveto stroke 0.000 0.000 0.000 edgecolor newpath 442.5 406 moveto 439 396 lineto 435.5 406 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 442.5 406 moveto 439 396 lineto 435.5 406 lineto closepath stroke grestore % Tacmach->Refiner gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 678 441 moveto 628 428 533 403 480 389 curveto stroke 0.000 0.000 0.000 edgecolor newpath 480.584 385.521 moveto 470 386 lineto 478.573 392.226 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 480.584 385.521 moveto 470 386 lineto 478.573 392.226 lineto closepath stroke grestore % Redexpr gsave 0.502 1.000 0.820 nodecolor 711 378 36.1752 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 711 378 36.1752 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 711 373 moveto 47 -0.5 (Redexpr) alignedtext grestore % Tacmach->Redexpr gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 711 432 moveto 711 424 711 415 711 406 curveto stroke 0.000 0.000 0.000 edgecolor newpath 714.5 406 moveto 711 396 lineto 707.5 406 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 714.5 406 moveto 711 396 lineto 707.5 406 lineto closepath stroke grestore % Decl_mode gsave 0.502 1.000 0.820 nodecolor 698 594 45.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 698 594 45.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 698 589 moveto 64 -0.5 (Decl_mode) alignedtext grestore % Pfedit gsave 0.502 1.000 0.820 nodecolor 698 522 30.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 698 522 30.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 698 517 moveto 34 -0.5 (Pfedit) alignedtext grestore % Decl_mode->Pfedit gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 698 576 moveto 698 568 698 559 698 550 curveto stroke 0.000 0.000 0.000 edgecolor newpath 701.5 550 moveto 698 540 lineto 694.5 550 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 701.5 550 moveto 698 540 lineto 694.5 550 lineto closepath stroke grestore % Pfedit->Evar_refiner gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 671 514 moveto 628 503 543 479 488 464 curveto stroke 0.000 0.000 0.000 edgecolor newpath 488.584 460.521 moveto 478 461 lineto 486.573 467.226 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 488.584 460.521 moveto 478 461 lineto 486.573 467.226 lineto closepath stroke grestore % Pfedit->Tacmach gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 701 504 moveto 702 496 704 487 706 478 curveto stroke 0.000 0.000 0.000 edgecolor newpath 709.471 478.492 moveto 708 468 lineto 702.607 477.119 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 709.471 478.492 moveto 708 468 lineto 702.607 477.119 lineto closepath stroke grestore % Logic gsave 0.502 1.000 0.820 nodecolor 439 306 29.1747 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 306 29.1747 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 301 moveto 33 -0.5 (Logic) alignedtext grestore % Refiner->Logic gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 439 360 moveto 439 352 439 343 439 334 curveto stroke 0.000 0.000 0.000 edgecolor newpath 442.5 334 moveto 439 324 lineto 435.5 334 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 442.5 334 moveto 439 324 lineto 435.5 334 lineto closepath stroke grestore % Proof_trees gsave 0.502 1.000 0.820 nodecolor 439 234 45.1757 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 234 45.1757 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 229 moveto 65 -0.5 (Proof_trees) alignedtext grestore % Logic->Proof_trees gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 439 288 moveto 439 280 439 271 439 262 curveto stroke 0.000 0.000 0.000 edgecolor newpath 442.5 262 moveto 439 252 lineto 435.5 262 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 442.5 262 moveto 439 252 lineto 435.5 262 lineto closepath stroke grestore % Proof_type gsave 0.502 1.000 0.820 nodecolor 439 162 44.1757 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 162 44.1757 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 157 moveto 63 -0.5 (Proof_type) alignedtext grestore % Proof_trees->Proof_type gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 439 216 moveto 439 208 439 199 439 190 curveto stroke 0.000 0.000 0.000 edgecolor newpath 442.5 190 moveto 439 180 lineto 435.5 190 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 442.5 190 moveto 439 180 lineto 435.5 190 lineto closepath stroke grestore % Decl_expr gsave 0.502 1.000 0.820 nodecolor 439 90 42.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 90 42.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 85 moveto 58 -0.5 (Decl_expr) alignedtext grestore % Proof_type->Decl_expr gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 439 144 moveto 439 136 439 127 439 118 curveto stroke 0.000 0.000 0.000 edgecolor newpath 442.5 118 moveto 439 108 lineto 435.5 118 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 442.5 118 moveto 439 108 lineto 435.5 118 lineto closepath stroke grestore % Tacexpr gsave 0.502 1.000 0.820 nodecolor 439 18 36.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 439 18 36.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 439 13 moveto 46 -0.5 (Tacexpr) alignedtext grestore % Decl_expr->Tacexpr gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 439 72 moveto 439 64 439 55 439 46 curveto stroke 0.000 0.000 0.000 edgecolor newpath 442.5 46 moveto 439 36 lineto 435.5 46 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 442.5 46 moveto 439 36 lineto 435.5 46 lineto closepath stroke grestore % Tactic_debug gsave 0.502 1.000 0.820 nodecolor 133 450 51.1777 18 ellipse_path fill 0.870968 setlinewidth filled 0.502 1.000 0.820 nodecolor 133 450 51.1777 18 ellipse_path stroke 0.000 0.000 0.000 nodecolor 14.00 /Times-Roman set_font 133 445 moveto 76 -0.5 (Tactic_debug) alignedtext grestore % Tactic_debug->Refiner gsave 0.870968 setlinewidth 0.000 0.000 0.000 edgecolor newpath 176 440 moveto 234 426 339 401 398 387 curveto stroke 0.000 0.000 0.000 edgecolor newpath 398.881 390.393 moveto 408 385 lineto 397.508 383.529 lineto closepath fill 0.870968 setlinewidth solid 0.000 0.000 0.000 edgecolor newpath 398.881 390.393 moveto 408 385 lineto 397.508 383.529 lineto closepath stroke grestore endpage showpage grestore %%PageTrailer %%EndPage: 1 %%Trailer %%Pages: 1 %%BoundingBox: 36 36 576 753 end restore %%EOF