path: root/doc/proofs.dep.ps

%!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