%!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 123 %%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 123 %%PageOrientation: Portrait gsave 35 35 542 88 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0.4348 set_scale 0 0 translate 0 rotate [ /CropBox [36 36 577 123] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Termdn gsave 10 dict begin 1091 180 39 18 ellipse_path stroke gsave 10 dict begin 1091 175 moveto 56 -0.5 (Termdn) alignedtext end grestore end grestore % Dn gsave 10 dict begin 1207 180 27 18 ellipse_path stroke gsave 10 dict begin 1207 175 moveto 21 -0.5 (Dn) alignedtext end grestore end grestore % Termdn -> Dn newpath 1130 180 moveto 1143 180 1158 180 1171 180 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1170 178 moveto 1180 180 lineto 1170 183 lineto closepath fill 0.000 0.000 0.000 edgecolor % Tactics gsave 10 dict begin 830 86 34 18 ellipse_path stroke gsave 10 dict begin 830 81 moveto 46 -0.5 (Tactics) alignedtext end grestore end grestore % Hipattern gsave 10 dict begin 958 113 44 18 ellipse_path stroke gsave 10 dict begin 958 108 moveto 66 -0.5 (Hipattern) alignedtext end grestore end grestore % Tactics -> Hipattern newpath 862 93 moveto 876 96 894 100 909 103 curveto stroke 0.000 0.000 0.000 edgecolor newpath 910 101 moveto 919 105 lineto 909 105 lineto closepath fill 0.000 0.000 0.000 edgecolor % Tacticals gsave 10 dict begin 958 59 40 18 ellipse_path stroke gsave 10 dict begin 958 54 moveto 58 -0.5 (Tacticals) alignedtext end grestore end grestore % Tactics -> Tacticals newpath 862 79 moveto 877 76 896 72 912 69 curveto stroke 0.000 0.000 0.000 edgecolor newpath 912 67 moveto 922 67 lineto 913 71 lineto closepath fill 0.000 0.000 0.000 edgecolor % Wcclausenv gsave 10 dict begin 1091 59 52 18 ellipse_path stroke gsave 10 dict begin 1091 54 moveto 83 -0.5 (Wcclausenv) alignedtext end grestore end grestore % Tacticals -> Wcclausenv newpath 998 59 moveto 1008 59 1018 59 1028 59 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1028 57 moveto 1038 59 lineto 1028 62 lineto closepath fill 0.000 0.000 0.000 edgecolor % Tacinterp gsave 10 dict begin 439 18 43 18 ellipse_path stroke gsave 10 dict begin 439 13 moveto 65 -0.5 (Tacinterp) alignedtext end grestore end grestore % Auto gsave 10 dict begin 565 72 28 18 ellipse_path stroke gsave 10 dict begin 565 67 moveto 35 -0.5 (Auto) alignedtext end grestore end grestore % Tacinterp -> Auto newpath 470 31 moveto 489 39 514 50 533 58 curveto stroke 0.000 0.000 0.000 edgecolor newpath 533 55 moveto 541 62 lineto 531 60 lineto closepath fill 0.000 0.000 0.000 edgecolor % Elim gsave 10 dict begin 565 18 27 18 ellipse_path stroke gsave 10 dict begin 565 13 moveto 33 -0.5 (Elim) alignedtext end grestore end grestore % Tacinterp -> Elim newpath 483 18 moveto 498 18 514 18 528 18 curveto stroke 0.000 0.000 0.000 edgecolor newpath 527 16 moveto 537 18 lineto 527 21 lineto closepath fill 0.000 0.000 0.000 edgecolor % Hiddentac gsave 10 dict begin 688 18 46 18 ellipse_path stroke gsave 10 dict begin 688 13 moveto 70 -0.5 (Hiddentac) alignedtext end grestore end grestore % Auto -> Hiddentac newpath 588 62 moveto 605 54 629 44 648 36 curveto stroke 0.000 0.000 0.000 edgecolor newpath 647 34 moveto 657 32 lineto 649 38 lineto closepath fill 0.000 0.000 0.000 edgecolor % Dhyp gsave 10 dict begin 688 180 30 18 ellipse_path stroke gsave 10 dict begin 688 175 moveto 39 -0.5 (Dhyp) alignedtext end grestore end grestore % Auto -> Dhyp newpath 578 88 moveto 597 112 630 152 630 153 curveto 637 158 646 163 653 167 curveto stroke 0.000 0.000 0.000 edgecolor newpath 654 165 moveto 662 171 lineto 652 169 lineto closepath fill 0.000 0.000 0.000 edgecolor % Elim -> Hiddentac newpath 593 18 moveto 604 18 618 18 632 18 curveto stroke 0.000 0.000 0.000 edgecolor newpath 632 16 moveto 642 18 lineto 632 21 lineto closepath fill 0.000 0.000 0.000 edgecolor % Setoid_replace gsave 10 dict begin 439 72 60 18 ellipse_path stroke gsave 10 dict begin 439 67 moveto 99 -0.5 (Setoid_replace) alignedtext end grestore end grestore % Setoid_replace -> Auto newpath 500 72 moveto 509 72 518 72 527 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 526 70 moveto 536 72 lineto 526 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Refine gsave 10 dict begin 688 126 34 18 ellipse_path stroke gsave 10 dict begin 688 121 moveto 47 -0.5 (Refine) alignedtext end grestore end grestore % Refine -> Tactics newpath 718 117 moveto 739 112 768 103 791 97 curveto stroke 0.000 0.000 0.000 edgecolor newpath 790 95 moveto 800 95 lineto 791 100 lineto closepath fill 0.000 0.000 0.000 edgecolor % Nbtermdn gsave 10 dict begin 830 180 47 18 ellipse_path stroke gsave 10 dict begin 830 175 moveto 73 -0.5 (Nbtermdn) alignedtext end grestore end grestore % Btermdn gsave 10 dict begin 958 180 42 18 ellipse_path stroke gsave 10 dict begin 958 175 moveto 62 -0.5 (Btermdn) alignedtext end grestore end grestore % Nbtermdn -> Btermdn newpath 878 180 moveto 887 180 897 180 906 180 curveto stroke 0.000 0.000 0.000 edgecolor newpath 906 178 moveto 916 180 lineto 906 183 lineto closepath fill 0.000 0.000 0.000 edgecolor % Btermdn -> Termdn newpath 1000 180 moveto 1014 180 1029 180 1042 180 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1042 178 moveto 1052 180 lineto 1042 183 lineto closepath fill 0.000 0.000 0.000 edgecolor % Leminv gsave 10 dict begin 46 72 38 18 ellipse_path stroke gsave 10 dict begin 46 67 moveto 54 -0.5 (Leminv) alignedtext end grestore end grestore % Inv gsave 10 dict begin 173 72 27 18 ellipse_path stroke gsave 10 dict begin 173 67 moveto 23 -0.5 (Inv) alignedtext end grestore end grestore % Leminv -> Inv newpath 84 72 moveto 101 72 120 72 137 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 136 70 moveto 146 72 lineto 136 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Equality gsave 10 dict begin 302 45 40 18 ellipse_path stroke gsave 10 dict begin 302 40 moveto 58 -0.5 (Equality) alignedtext end grestore end grestore % Inv -> Equality newpath 199 67 moveto 215 64 236 59 255 55 curveto stroke 0.000 0.000 0.000 edgecolor newpath 255 53 moveto 265 53 lineto 256 57 lineto closepath fill 0.000 0.000 0.000 edgecolor % Equality -> Tacinterp newpath 339 38 moveto 355 35 374 31 391 28 curveto stroke 0.000 0.000 0.000 edgecolor newpath 390 26 moveto 400 26 lineto 391 31 lineto closepath fill 0.000 0.000 0.000 edgecolor % Equality -> Setoid_replace newpath 339 52 moveto 352 55 367 58 382 61 curveto stroke 0.000 0.000 0.000 edgecolor newpath 379 58 moveto 389 62 lineto 379 63 lineto closepath fill 0.000 0.000 0.000 edgecolor % Hiddentac -> Tactics newpath 718 32 moveto 732 39 746 45 746 45 curveto 751 48 776 60 798 71 curveto stroke 0.000 0.000 0.000 edgecolor newpath 797 68 moveto 805 74 lineto 795 72 lineto closepath fill 0.000 0.000 0.000 edgecolor % Dhyp -> Tactics newpath 713 170 moveto 724 165 736 159 746 153 curveto 768 139 790 121 807 107 curveto stroke 0.000 0.000 0.000 edgecolor newpath 804 106 moveto 813 102 lineto 807 110 lineto closepath fill 0.000 0.000 0.000 edgecolor % Dhyp -> Nbtermdn newpath 719 180 moveto 735 180 755 180 772 180 curveto stroke 0.000 0.000 0.000 edgecolor newpath 772 178 moveto 782 180 lineto 772 183 lineto closepath fill 0.000 0.000 0.000 edgecolor % Contradiction gsave 10 dict begin 688 72 57 18 ellipse_path stroke gsave 10 dict begin 688 67 moveto 93 -0.5 (Contradiction) alignedtext end grestore end grestore % Contradiction -> Tactics newpath 743 77 moveto 758 79 773 80 787 81 curveto stroke 0.000 0.000 0.000 edgecolor newpath 786 78 moveto 796 82 lineto 786 83 lineto closepath fill 0.000 0.000 0.000 edgecolor % Autorewrite gsave 10 dict begin 173 18 53 18 ellipse_path stroke gsave 10 dict begin 173 13 moveto 84 -0.5 (Autorewrite) alignedtext end grestore end grestore % Autorewrite -> Equality newpath 218 28 moveto 231 30 244 33 256 35 curveto stroke 0.000 0.000 0.000 edgecolor newpath 256 32 moveto 265 37 lineto 255 37 lineto closepath fill 0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer %%EndPage: 1 %%Trailer %%Pages: 1 end restore %%EOF