path: root/doc/proofs.dep.ps

%!PS-Adobe-2.0
%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
%%For: (clrenard) Clement Renard
%%Title: G
%%Pages: (atend)
%%BoundingBox: 36 36 577 136
%%EndComments
%%BeginProlog
save
/DotDict 200 dict def
DotDict begin

%%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
% alignfactor tells what fraction to place on the left.
% -.5 is centered.
/alignedtext {			% text labelwidth fontsz alignfactor
	/alignfactor exch def
	/fontsz exch def
	/width exch def
	/text exch def
	gsave
		% even if node or edge is dashed, don't paint text with dashes
		[] 0 setdash
		currentpoint newpath moveto
		text stringwidth pop
		alignfactor mul fontsz -.3 mul rmoveto
		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

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

%%EndResource
%%EndSetup
%%Page: 1 1
%%PageBoundingBox: 36 36 577 136
%%PageOrientation: Portrait
gsave
35 35 542 101 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.6905 set_scale
0 0 translate 0 rotate
[ /CropBox [36 36 577 136] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font

%	Tactic_debug
gsave 10 dict begin
167 18 48 18 ellipse_path
stroke
gsave 10 dict begin
167 19 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
end grestore
end grestore

%	Tacmach
gsave 10 dict begin
298 72 36 18 ellipse_path
stroke
gsave 10 dict begin
298 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
end grestore
end grestore

%	Tactic_debug -> Tacmach
newpath 200 31 moveto
219 39 243 49 262 57 curveto
stroke
newpath 262 54 moveto
270 60 lineto
260 59 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Refiner
gsave 10 dict begin
411 99 31 18 ellipse_path
stroke
gsave 10 dict begin
411 100 moveto (Refiner) 41 14.00 -0.50 alignedtext
end grestore
end grestore

%	Tacmach -> Refiner
newpath 331 80 moveto
344 83 360 87 373 90 curveto
stroke
newpath 373 87 moveto
382 92 lineto
372 92 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Logic
gsave 10 dict begin
505 99 27 18 ellipse_path
stroke
gsave 10 dict begin
505 100 moveto (Logic) 32 14.00 -0.50 alignedtext
end grestore
end grestore

%	Refiner -> Logic
newpath 442 99 moveto
450 99 459 99 468 99 curveto
stroke
newpath 468 97 moveto
478 99 lineto
468 102 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Tacinterp
gsave 10 dict begin
45 72 37 18 ellipse_path
stroke
gsave 10 dict begin
45 73 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
end grestore
end grestore

%	Tacinterp -> Tactic_debug
newpath 72 60 moveto
88 53 109 44 127 36 curveto
stroke
newpath 126 34 moveto
136 32 lineto
128 38 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Pfedit
gsave 10 dict begin
167 126 27 18 ellipse_path
stroke
gsave 10 dict begin
167 127 moveto (Pfedit) 33 14.00 -0.50 alignedtext
end grestore
end grestore

%	Tacinterp -> Pfedit
newpath 72 84 moveto
91 93 117 104 136 112 curveto
stroke
newpath 136 109 moveto
144 116 lineto
134 114 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Pfedit -> Tacmach
newpath 190 116 moveto
210 108 239 96 261 87 curveto
stroke
newpath 260 85 moveto
270 83 lineto
262 89 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Evar_refiner
gsave 10 dict begin
298 126 45 18 ellipse_path
stroke
gsave 10 dict begin
298 127 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
end grestore
end grestore

%	Pfedit -> Evar_refiner
newpath 194 126 moveto
208 126 226 126 242 126 curveto
stroke
newpath 242 124 moveto
252 126 lineto
242 129 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Proof_trees
gsave 10 dict begin
611 99 42 18 ellipse_path
stroke
gsave 10 dict begin
611 100 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
end grestore
end grestore

%	Logic -> Proof_trees
newpath 532 99 moveto
540 99 549 99 558 99 curveto
stroke
newpath 558 97 moveto
568 99 lineto
558 102 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Proof_type
gsave 10 dict begin
732 99 41 18 ellipse_path
stroke
gsave 10 dict begin
732 100 moveto (Proof_type) 62 14.00 -0.50 alignedtext
end grestore
end grestore

%	Proof_trees -> Proof_type
newpath 654 99 moveto
663 99 672 99 680 99 curveto
stroke
newpath 680 97 moveto
690 99 lineto
680 102 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Evar_refiner -> Refiner
newpath 337 117 moveto
349 114 362 111 373 108 curveto
stroke
newpath 372 106 moveto
382 106 lineto
373 111 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Clenv
gsave 10 dict begin
167 72 27 18 ellipse_path
stroke
gsave 10 dict begin
167 73 moveto (Clenv) 33 14.00 -0.50 alignedtext
end grestore
end grestore

%	Clenv -> Tacmach
newpath 194 72 moveto
211 72 232 72 252 72 curveto
stroke
newpath 252 70 moveto
262 72 lineto
252 75 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Clenv -> Evar_refiner
newpath 190 82 moveto
208 89 235 100 257 109 curveto
stroke
newpath 258 107 moveto
266 113 lineto
256 111 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
end
restore
%%EOF