%!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 159 %%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 159 %%PageOrientation: Portrait gsave 35 35 542 124 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0.3634 set_scale 0 0 translate 0 rotate [ /CropBox [36 36 577 159] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Typing gsave 10 dict begin 523 241 36 18 ellipse_path stroke gsave 10 dict begin 523 236 moveto 50 -0.5 (Typing) alignedtext end grestore end grestore % Pretype_errors gsave 10 dict begin 898 264 62 18 ellipse_path stroke gsave 10 dict begin 898 259 moveto 102 -0.5 (Pretype_errors) alignedtext end grestore end grestore % Typing -> Pretype_errors newpath 559 243 moveto 621 247 750 255 830 260 curveto stroke 0.000 0.000 0.000 edgecolor newpath 827 258 moveto 837 260 lineto 827 263 lineto closepath fill 0.000 0.000 0.000 edgecolor % Rawterm gsave 10 dict begin 1051 114 43 18 ellipse_path stroke gsave 10 dict begin 1051 109 moveto 65 -0.5 (Rawterm) alignedtext end grestore end grestore % Pretype_errors -> Rawterm newpath 939 250 moveto 946 247 954 242 960 237 curveto 983 218 979 206 996 183 curveto 1008 168 1021 151 1032 138 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1029 138 moveto 1037 131 lineto 1033 141 lineto closepath fill 0.000 0.000 0.000 edgecolor % Inductiveops gsave 10 dict begin 1051 210 54 18 ellipse_path stroke gsave 10 dict begin 1051 205 moveto 87 -0.5 (Inductiveops) alignedtext end grestore end grestore % Pretype_errors -> Inductiveops newpath 937 250 moveto 958 243 984 234 1005 226 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1004 224 moveto 1014 223 lineto 1005 229 lineto closepath fill 0.000 0.000 0.000 edgecolor % Tacred gsave 10 dict begin 761 120 34 18 ellipse_path stroke gsave 10 dict begin 761 115 moveto 47 -0.5 (Tacred) alignedtext end grestore end grestore % Cbv gsave 10 dict begin 1200 18 27 18 ellipse_path stroke gsave 10 dict begin 1200 13 moveto 29 -0.5 (Cbv) alignedtext end grestore end grestore % Tacred -> Cbv newpath 775 103 moveto 794 80 828 41 836 37 curveto 852 30 1077 22 1165 19 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1163 17 moveto 1173 19 lineto 1163 22 lineto closepath fill 0.000 0.000 0.000 edgecolor % Tacred -> Rawterm newpath 796 119 moveto 847 118 941 116 999 115 curveto stroke 0.000 0.000 0.000 edgecolor newpath 997 113 moveto 1007 115 lineto 997 118 lineto closepath fill 0.000 0.000 0.000 edgecolor % Retyping gsave 10 dict begin 898 210 43 18 ellipse_path stroke gsave 10 dict begin 898 205 moveto 64 -0.5 (Retyping) alignedtext end grestore end grestore % Tacred -> Retyping newpath 779 135 moveto 801 154 835 182 836 183 curveto 837 183 847 188 859 193 curveto stroke 0.000 0.000 0.000 edgecolor newpath 860 191 moveto 868 197 lineto 858 195 lineto closepath fill 0.000 0.000 0.000 edgecolor % Instantiate gsave 10 dict begin 1341 18 46 18 ellipse_path stroke gsave 10 dict begin 1341 13 moveto 71 -0.5 (Instantiate) alignedtext end grestore end grestore % Cbv -> Instantiate newpath 1227 18 moveto 1243 18 1264 18 1284 18 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1284 16 moveto 1294 18 lineto 1284 21 lineto closepath fill 0.000 0.000 0.000 edgecolor % Retyping -> Inductiveops newpath 941 210 moveto 955 210 971 210 986 210 curveto stroke 0.000 0.000 0.000 edgecolor newpath 986 208 moveto 996 210 lineto 986 213 lineto closepath fill 0.000 0.000 0.000 edgecolor % Reductionops gsave 10 dict begin 1200 72 58 18 ellipse_path stroke gsave 10 dict begin 1200 67 moveto 94 -0.5 (Reductionops) alignedtext end grestore end grestore % Inductiveops -> Reductionops newpath 1070 193 moveto 1097 169 1146 123 1175 95 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1172 94 moveto 1181 89 lineto 1176 98 lineto closepath fill 0.000 0.000 0.000 edgecolor % Reductionops -> Instantiate newpath 1237 58 moveto 1256 51 1279 42 1299 34 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1298 32 moveto 1308 31 lineto 1299 37 lineto closepath fill 0.000 0.000 0.000 edgecolor % Termops gsave 10 dict begin 1341 72 41 18 ellipse_path stroke gsave 10 dict begin 1341 67 moveto 60 -0.5 (Termops) alignedtext end grestore end grestore % Reductionops -> Termops newpath 1258 72 moveto 1269 72 1280 72 1290 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1290 70 moveto 1300 72 lineto 1290 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evd gsave 10 dict begin 1451 18 27 18 ellipse_path stroke gsave 10 dict begin 1451 13 moveto 28 -0.5 (Evd) alignedtext end grestore end grestore % Instantiate -> Evd newpath 1388 18 moveto 1397 18 1406 18 1414 18 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1414 16 moveto 1424 18 lineto 1414 21 lineto closepath fill 0.000 0.000 0.000 edgecolor % Recordops gsave 10 dict begin 523 149 47 18 ellipse_path stroke gsave 10 dict begin 523 144 moveto 72 -0.5 (Recordops) alignedtext end grestore end grestore % Classops gsave 10 dict begin 646 139 39 18 ellipse_path stroke gsave 10 dict begin 646 134 moveto 57 -0.5 (Classops) alignedtext end grestore end grestore % Recordops -> Classops newpath 569 145 moveto 578 144 588 144 597 143 curveto stroke 0.000 0.000 0.000 edgecolor newpath 597 141 moveto 607 142 lineto 597 145 lineto closepath fill 0.000 0.000 0.000 edgecolor % Classops -> Tacred newpath 683 133 moveto 694 131 707 129 718 127 curveto stroke 0.000 0.000 0.000 edgecolor newpath 718 125 moveto 728 125 lineto 719 129 lineto closepath fill 0.000 0.000 0.000 edgecolor % Pretyping gsave 10 dict begin 53 241 44 18 ellipse_path stroke gsave 10 dict begin 53 236 moveto 67 -0.5 (Pretyping) alignedtext end grestore end grestore % Cases gsave 10 dict begin 164 241 29 18 ellipse_path stroke gsave 10 dict begin 164 236 moveto 37 -0.5 (Cases) alignedtext end grestore end grestore % Pretyping -> Cases newpath 98 241 moveto 107 241 116 241 124 241 curveto stroke 0.000 0.000 0.000 edgecolor newpath 124 239 moveto 134 241 lineto 124 244 lineto closepath fill 0.000 0.000 0.000 edgecolor % Coercion gsave 10 dict begin 272 241 41 18 ellipse_path stroke gsave 10 dict begin 272 236 moveto 61 -0.5 (Coercion) alignedtext end grestore end grestore % Cases -> Coercion newpath 194 241 moveto 202 241 211 241 220 241 curveto stroke 0.000 0.000 0.000 edgecolor newpath 220 239 moveto 230 241 lineto 220 244 lineto closepath fill 0.000 0.000 0.000 edgecolor % Pattern gsave 10 dict begin 898 64 35 18 ellipse_path stroke gsave 10 dict begin 898 59 moveto 49 -0.5 (Pattern) alignedtext end grestore end grestore % Pattern -> Rawterm newpath 928 74 moveto 950 81 982 91 1008 100 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1008 97 moveto 1017 103 lineto 1007 102 lineto closepath fill 0.000 0.000 0.000 edgecolor % Pattern -> Reductionops newpath 934 65 moveto 983 66 1072 69 1134 70 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1132 68 moveto 1142 70 lineto 1132 73 lineto closepath fill 0.000 0.000 0.000 edgecolor % Indrec gsave 10 dict begin 898 318 32 18 ellipse_path stroke gsave 10 dict begin 898 313 moveto 43 -0.5 (Indrec) alignedtext end grestore end grestore % Indrec -> Inductiveops newpath 926 308 moveto 937 304 949 298 960 291 curveto 973 282 1004 255 1026 234 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1024 232 moveto 1033 227 lineto 1028 236 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evarutil gsave 10 dict begin 761 287 39 18 ellipse_path stroke gsave 10 dict begin 761 282 moveto 56 -0.5 (Evarutil) alignedtext end grestore end grestore % Evarutil -> Pretype_errors newpath 798 281 moveto 809 279 822 277 834 275 curveto stroke 0.000 0.000 0.000 edgecolor newpath 834 273 moveto 844 273 lineto 835 277 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evarutil -> Indrec newpath 796 295 moveto 815 299 839 304 859 309 curveto stroke 0.000 0.000 0.000 edgecolor newpath 859 306 moveto 868 311 lineto 858 311 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evarconv gsave 10 dict begin 395 241 44 18 ellipse_path stroke gsave 10 dict begin 395 236 moveto 67 -0.5 (Evarconv) alignedtext end grestore end grestore % Evarconv -> Typing newpath 440 241 moveto 452 241 465 241 477 241 curveto stroke 0.000 0.000 0.000 edgecolor newpath 477 239 moveto 487 241 lineto 477 244 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evarconv -> Recordops newpath 417 225 moveto 439 210 471 187 494 170 curveto stroke 0.000 0.000 0.000 edgecolor newpath 491 169 moveto 501 165 lineto 494 173 lineto closepath fill 0.000 0.000 0.000 edgecolor % Evarconv -> Evarutil newpath 427 254 moveto 442 259 460 264 476 268 curveto 482 269 636 278 715 284 curveto stroke 0.000 0.000 0.000 edgecolor newpath 712 282 moveto 722 284 lineto 712 287 lineto closepath fill 0.000 0.000 0.000 edgecolor % Detyping gsave 10 dict begin 898 156 43 18 ellipse_path stroke gsave 10 dict begin 898 151 moveto 64 -0.5 (Detyping) alignedtext end grestore end grestore % Detyping -> Rawterm newpath 934 146 moveto 956 141 983 133 1006 127 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1005 125 moveto 1015 124 lineto 1006 130 lineto closepath fill 0.000 0.000 0.000 edgecolor % Detyping -> Inductiveops newpath 931 168 moveto 952 176 981 185 1004 194 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1004 191 moveto 1013 197 lineto 1003 196 lineto closepath fill 0.000 0.000 0.000 edgecolor % Coercion -> Evarconv newpath 314 241 moveto 323 241 331 241 340 241 curveto stroke 0.000 0.000 0.000 edgecolor newpath 340 239 moveto 350 241 lineto 340 244 lineto closepath fill 0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer %%EndPage: 1 %%Trailer %%Pages: 1 end restore %%EOF