aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/proofs.dep.ps
blob: d5d247a2c771b44f8b44200dc54d6de188ecd77f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
%!PS-Adobe-2.0
%%Creator: dot version uwin98 (01-26-98)
%%For: Gros nain
%%Title: G
%%Pages: (atend)
%%BoundingBox: 36 36 577 125
%%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

%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
% /arrowlength 10 def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
%%PageBoundingBox: 36 36 577 125
gsave
35 35 542 90 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.6178 set_scale
0 0 translate 0 rotate
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font

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

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

%	Tactic_debug -> Tacmach
newpath 190 112 moveto
207 104 227 95 244 88 curveto
stroke
newpath 243 86 moveto
253 84 lineto
245 90 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Evar_refiner
gsave 10 dict begin
398 72 45 18 ellipse_path
stroke
gsave 10 dict begin
398 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
end grestore
end grestore

%	Tacmach -> Evar_refiner
newpath 316 72 moveto
324 72 333 72 342 72 curveto
stroke
newpath 342 70 moveto
352 72 lineto
342 75 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Refiner
gsave 10 dict begin
511 72 31 18 ellipse_path
stroke
gsave 10 dict begin
511 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
end grestore
end grestore

%	Evar_refiner -> Refiner
newpath 444 72 moveto
453 72 462 72 470 72 curveto
stroke
newpath 470 70 moveto
480 72 lineto
470 75 lineto
closepath
gsave 0 setgray stroke grestore fill

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

%	Tacinterp -> Tactic_debug
newpath 71 107 moveto
82 109 95 112 107 115 curveto
stroke
newpath 108 113 moveto
117 117 lineto
107 117 lineto
closepath
gsave 0 setgray stroke grestore fill

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

%	Tacinterp -> Pfedit
newpath 71 91 moveto
88 88 108 83 124 80 curveto
stroke
newpath 123 78 moveto
133 78 lineto
124 83 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Pfedit -> Tacmach
newpath 186 72 moveto
200 72 218 72 234 72 curveto
stroke
newpath 234 70 moveto
244 72 lineto
234 75 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Logic
gsave 10 dict begin
605 72 27 18 ellipse_path
stroke
gsave 10 dict begin
605 73 moveto (Logic) 32 14.00 -0.50 alignedtext
end grestore
end grestore

%	Refiner -> Logic
newpath 542 72 moveto
550 72 559 72 568 72 curveto
stroke
newpath 568 70 moveto
578 72 lineto
568 75 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Proof_trees
gsave 10 dict begin
711 72 42 18 ellipse_path
stroke
gsave 10 dict begin
711 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
end grestore
end grestore

%	Logic -> Proof_trees
newpath 632 72 moveto
640 72 649 72 658 72 curveto
stroke
newpath 658 70 moveto
668 72 lineto
658 75 lineto
closepath
gsave 0 setgray stroke grestore fill

%	Proof_type
gsave 10 dict begin
832 72 41 18 ellipse_path
stroke
gsave 10 dict begin
832 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
end grestore
end grestore

%	Proof_trees -> Proof_type
newpath 754 72 moveto
763 72 772 72 780 72 curveto
stroke
newpath 780 70 moveto
790 72 lineto
780 75 lineto
closepath
gsave 0 setgray stroke grestore fill

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

%	Clenv -> Tacmach
newpath 181 28 moveto
198 36 224 48 244 56 curveto
stroke
newpath 245 54 moveto
253 60 lineto
243 58 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
end
restore
%%EOF