%!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 88 %%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 88 %%PageOrientation: Portrait gsave 35 35 542 53 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0.2736 set_scale 0 0 translate 0 rotate [ /CropBox [36 36 577 88] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Univ gsave 10 dict begin 1826 172 28 18 ellipse_path stroke gsave 10 dict begin 1826 167 moveto 35 -0.5 (Univ) alignedtext end grestore end grestore % Names gsave 10 dict begin 1931 172 35 18 ellipse_path stroke gsave 10 dict begin 1931 167 moveto 48 -0.5 (Names) alignedtext end grestore end grestore % Univ -> Names newpath 1855 172 moveto 1865 172 1875 172 1886 172 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1886 170 moveto 1896 172 lineto 1886 175 lineto closepath fill 0.000 0.000 0.000 edgecolor % Typeops gsave 10 dict begin 613 149 40 18 ellipse_path stroke gsave 10 dict begin 613 144 moveto 58 -0.5 (Typeops) alignedtext end grestore end grestore % Entries gsave 10 dict begin 872 168 35 18 ellipse_path stroke gsave 10 dict begin 872 163 moveto 48 -0.5 (Entries) alignedtext end grestore end grestore % Typeops -> Entries newpath 653 152 moveto 701 155 781 161 830 165 curveto stroke 0.000 0.000 0.000 edgecolor newpath 827 163 moveto 837 165 lineto 827 168 lineto closepath fill 0.000 0.000 0.000 edgecolor % Inductive gsave 10 dict begin 739 72 43 18 ellipse_path stroke gsave 10 dict begin 739 67 moveto 64 -0.5 (Inductive) alignedtext end grestore end grestore % Typeops -> Inductive newpath 637 134 moveto 657 122 685 105 706 92 curveto stroke 0.000 0.000 0.000 edgecolor newpath 704 90 moveto 714 87 lineto 707 94 lineto closepath fill 0.000 0.000 0.000 edgecolor % Sign gsave 10 dict begin 1633 145 27 18 ellipse_path stroke gsave 10 dict begin 1633 140 moveto 30 -0.5 (Sign) alignedtext end grestore end grestore % Entries -> Sign newpath 907 168 moveto 976 168 1124 167 1147 168 curveto 1147 168 1147 168 1387 168 curveto 1462 167 1549 157 1597 150 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1597 148 moveto 1607 149 lineto 1597 152 lineto closepath fill 0.000 0.000 0.000 edgecolor % Type_errors gsave 10 dict begin 872 72 53 18 ellipse_path stroke gsave 10 dict begin 872 67 moveto 85 -0.5 (Type_errors) alignedtext end grestore end grestore % Inductive -> Type_errors newpath 782 72 moveto 791 72 799 72 808 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 808 70 moveto 818 72 lineto 808 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Reduction gsave 10 dict begin 1009 72 46 18 ellipse_path stroke gsave 10 dict begin 1009 67 moveto 71 -0.5 (Reduction) alignedtext end grestore end grestore % Type_errors -> Reduction newpath 926 72 moveto 935 72 943 72 952 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 952 70 moveto 962 72 lineto 952 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Conv_oracle gsave 10 dict begin 1147 74 55 18 ellipse_path stroke gsave 10 dict begin 1147 69 moveto 88 -0.5 (Conv_oracle) alignedtext end grestore end grestore % Reduction -> Conv_oracle newpath 1056 73 moveto 1065 73 1073 73 1082 73 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1082 71 moveto 1092 73 lineto 1082 76 lineto closepath fill 0.000 0.000 0.000 edgecolor % Term_typing gsave 10 dict begin 355 95 57 18 ellipse_path stroke gsave 10 dict begin 355 90 moveto 92 -0.5 (Term_typing) alignedtext end grestore end grestore % Cooking gsave 10 dict begin 489 95 40 18 ellipse_path stroke gsave 10 dict begin 489 90 moveto 58 -0.5 (Cooking) alignedtext end grestore end grestore % Term_typing -> Cooking newpath 412 95 moveto 421 95 430 95 439 95 curveto stroke 0.000 0.000 0.000 edgecolor newpath 439 93 moveto 449 95 lineto 439 98 lineto closepath fill 0.000 0.000 0.000 edgecolor % Indtypes gsave 10 dict begin 489 149 40 18 ellipse_path stroke gsave 10 dict begin 489 144 moveto 59 -0.5 (Indtypes) alignedtext end grestore end grestore % Term_typing -> Indtypes newpath 390 109 moveto 409 117 432 126 451 134 curveto stroke 0.000 0.000 0.000 edgecolor newpath 451 131 moveto 459 137 lineto 449 136 lineto closepath fill 0.000 0.000 0.000 edgecolor % Cooking -> Reduction newpath 511 80 moveto 532 66 560 47 566 45 curveto 720 0 768 20 926 45 curveto 935 47 951 52 968 58 curveto stroke 0.000 0.000 0.000 edgecolor newpath 966 55 moveto 975 60 lineto 965 60 lineto closepath fill 0.000 0.000 0.000 edgecolor % Indtypes -> Typeops newpath 530 149 moveto 541 149 552 149 563 149 curveto stroke 0.000 0.000 0.000 edgecolor newpath 563 147 moveto 573 149 lineto 563 152 lineto closepath fill 0.000 0.000 0.000 edgecolor % Term gsave 10 dict begin 1726 145 30 18 ellipse_path stroke gsave 10 dict begin 1726 140 moveto 38 -0.5 (Term) alignedtext end grestore end grestore % Term -> Univ newpath 1754 152 moveto 1765 155 1779 159 1791 162 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1791 159 moveto 1800 165 lineto 1790 164 lineto closepath fill 0.000 0.000 0.000 edgecolor % Esubst gsave 10 dict begin 1826 118 33 18 ellipse_path stroke gsave 10 dict begin 1826 113 moveto 45 -0.5 (Esubst) alignedtext end grestore end grestore % Term -> Esubst newpath 1754 138 moveto 1764 135 1776 132 1787 129 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1786 127 moveto 1796 126 lineto 1787 132 lineto closepath fill 0.000 0.000 0.000 edgecolor % Subtyping gsave 10 dict begin 613 72 46 18 ellipse_path stroke gsave 10 dict begin 613 67 moveto 71 -0.5 (Subtyping) alignedtext end grestore end grestore % Subtyping -> Inductive newpath 660 72 moveto 669 72 677 72 686 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 686 70 moveto 696 72 lineto 686 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Modops gsave 10 dict begin 739 126 38 18 ellipse_path stroke gsave 10 dict begin 739 121 moveto 55 -0.5 (Modops) alignedtext end grestore end grestore % Subtyping -> Modops newpath 644 85 moveto 662 93 684 102 702 110 curveto stroke 0.000 0.000 0.000 edgecolor newpath 703 108 moveto 711 114 lineto 701 112 lineto closepath fill 0.000 0.000 0.000 edgecolor % Modops -> Entries newpath 771 136 moveto 790 142 814 150 833 156 curveto stroke 0.000 0.000 0.000 edgecolor newpath 833 153 moveto 842 159 lineto 832 158 lineto closepath fill 0.000 0.000 0.000 edgecolor % Environ gsave 10 dict begin 1387 122 39 18 ellipse_path stroke gsave 10 dict begin 1387 117 moveto 56 -0.5 (Environ) alignedtext end grestore end grestore % Modops -> Environ newpath 777 125 moveto 830 124 926 122 1009 122 curveto 1009 122 1009 122 1147 122 curveto 1152 122 1270 122 1339 122 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1338 120 moveto 1348 122 lineto 1338 125 lineto closepath fill 0.000 0.000 0.000 edgecolor % Sign -> Term newpath 1660 145 moveto 1668 145 1677 145 1686 145 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1686 143 moveto 1696 145 lineto 1686 148 lineto closepath fill 0.000 0.000 0.000 edgecolor % Safe_typing gsave 10 dict begin 62 72 53 18 ellipse_path stroke gsave 10 dict begin 62 67 moveto 85 -0.5 (Safe_typing) alignedtext end grestore end grestore % Mod_typing gsave 10 dict begin 207 72 54 18 ellipse_path stroke gsave 10 dict begin 207 67 moveto 87 -0.5 (Mod_typing) alignedtext end grestore end grestore % Safe_typing -> Mod_typing newpath 116 72 moveto 125 72 133 72 142 72 curveto stroke 0.000 0.000 0.000 edgecolor newpath 142 70 moveto 152 72 lineto 142 75 lineto closepath fill 0.000 0.000 0.000 edgecolor % Mod_typing -> Term_typing newpath 257 80 moveto 269 82 282 84 294 86 curveto stroke 0.000 0.000 0.000 edgecolor newpath 294 84 moveto 304 87 lineto 294 88 lineto closepath fill 0.000 0.000 0.000 edgecolor % Mod_typing -> Subtyping newpath 261 69 moveto 273 69 286 68 298 68 curveto 402 66 427 66 530 68 curveto 536 68 547 69 559 69 curveto stroke 0.000 0.000 0.000 edgecolor newpath 557 66 moveto 567 70 lineto 557 71 lineto closepath fill 0.000 0.000 0.000 edgecolor % Closure gsave 10 dict begin 1275 75 37 18 ellipse_path stroke gsave 10 dict begin 1275 70 moveto 52 -0.5 (Closure) alignedtext end grestore end grestore % Conv_oracle -> Closure newpath 1202 74 moveto 1211 74 1220 75 1228 75 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1228 73 moveto 1238 75 lineto 1228 78 lineto closepath fill 0.000 0.000 0.000 edgecolor % Declarations gsave 10 dict begin 1516 122 53 18 ellipse_path stroke gsave 10 dict begin 1516 117 moveto 85 -0.5 (Declarations) alignedtext end grestore end grestore % Environ -> Declarations newpath 1426 122 moveto 1434 122 1443 122 1452 122 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1452 120 moveto 1462 122 lineto 1452 125 lineto closepath fill 0.000 0.000 0.000 edgecolor % Declarations -> Sign newpath 1562 131 moveto 1574 133 1587 136 1598 138 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1598 135 moveto 1607 140 lineto 1597 140 lineto closepath fill 0.000 0.000 0.000 edgecolor % Closure -> Environ newpath 1303 87 moveto 1317 93 1334 100 1349 106 curveto stroke 0.000 0.000 0.000 edgecolor newpath 1350 104 moveto 1358 110 lineto 1348 108 lineto closepath fill 0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer %%EndPage: 1 %%Trailer %%Pages: 1 end restore %%EOF