summaryrefslogtreecommitdiff
path: root/dev/ocamlweb-doc/proofs.dep.ps
blob: 0e78f4226ef2a97b1c78951854d51cc0aa9ce6f6 (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
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
%!PS-Adobe-2.0
%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
%%BoundingBox: 35 35 577 136
%%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 graphviz 0 0
/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 { [] 0 setdash } 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
/showpage { } def

/layercolorseq
	[	% layer color sequence - darkest to lightest
		[0 0 0]
		[.2 .8 .8]
		[.4 .8 .8]
		[.6 .8 .8]
		[.8 .8 .8]
	]
def

/layerlen layercolorseq length def

/setlayer {/maxlayer exch def /curlayer exch def
	layercolorseq curlayer 1 sub layerlen mod 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 136
%%PageOrientation: Portrait
gsave
35 35 542 101 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.6923 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
163 72 51 18 ellipse_path
stroke
gsave 10 dict begin
125 67 moveto
(Tactic_debug)
[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96]
xshow
end grestore
end grestore

%	Refiner
gsave 10 dict begin
287 72 34 18 ellipse_path
stroke
gsave 10 dict begin
266 67 moveto
(Refiner)
[9.12 6.24 4.8 3.84 6.96 6.24 4.56]
xshow
end grestore
end grestore

%	Tactic_debug -> Refiner
newpath 214 72 moveto
223 72 233 72 243 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 243 76 moveto
253 72 lineto
243 69 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 243 76 moveto
253 72 lineto
243 69 lineto
closepath
stroke
end grestore

%	Logic
gsave 10 dict begin
390 72 30 18 ellipse_path
stroke
gsave 10 dict begin
373 67 moveto
(Logic)
[8.4 6.96 6.96 3.84 6.24]
xshow
end grestore
end grestore

%	Refiner -> Logic
newpath 321 72 moveto
330 72 340 72 350 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 350 76 moveto
360 72 lineto
350 69 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 350 76 moveto
360 72 lineto
350 69 lineto
closepath
stroke
end grestore

%	Tacmach
gsave 10 dict begin
163 126 38 18 ellipse_path
stroke
gsave 10 dict begin
137 121 moveto
(Tacmach)
[7.44 6.24 6.24 10.8 6.24 6 6.96]
xshow
end grestore
end grestore

%	Tacmach -> Refiner
newpath 191 114 moveto
209 106 232 96 251 88 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 253 91 moveto
261 84 lineto
250 84 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 253 91 moveto
261 84 lineto
250 84 lineto
closepath
stroke
end grestore

%	Redexpr
gsave 10 dict begin
287 126 36 18 ellipse_path
stroke
gsave 10 dict begin
263 121 moveto
(Redexpr)
[9.12 6.24 6.96 5.76 6.96 6.96 4.56]
xshow
end grestore
end grestore

%	Tacmach -> Redexpr
newpath 202 126 moveto
214 126 227 126 240 126 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 240 130 moveto
250 126 lineto
240 123 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 240 130 moveto
250 126 lineto
240 123 lineto
closepath
stroke
end grestore

%	Proof_trees
gsave 10 dict begin
502 72 45 18 ellipse_path
stroke
gsave 10 dict begin
469 67 moveto
(Proof_trees)
[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52]
xshow
end grestore
end grestore

%	Logic -> Proof_trees
newpath 420 72 moveto
428 72 437 72 446 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 446 76 moveto
456 72 lineto
446 69 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 446 76 moveto
456 72 lineto
446 69 lineto
closepath
stroke
end grestore

%	Proof_type
gsave 10 dict begin
628 72 44 18 ellipse_path
stroke
gsave 10 dict begin
597 67 moveto
(Proof_type)
[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24]
xshow
end grestore
end grestore

%	Tacexpr
gsave 10 dict begin
744 72 35 18 ellipse_path
stroke
gsave 10 dict begin
721 67 moveto
(Tacexpr)
[7.44 6.24 6.24 5.76 6.96 6.96 4.56]
xshow
end grestore
end grestore

%	Proof_type -> Tacexpr
newpath 672 72 moveto
680 72 689 72 698 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 698 76 moveto
708 72 lineto
698 69 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 698 76 moveto
708 72 lineto
698 69 lineto
closepath
stroke
end grestore

%	Proof_trees -> Proof_type
newpath 548 72 moveto
557 72 565 72 574 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 574 76 moveto
584 72 lineto
574 69 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 574 76 moveto
584 72 lineto
574 69 lineto
closepath
stroke
end grestore

%	Pfedit
gsave 10 dict begin
38 112 29 18 ellipse_path
stroke
gsave 10 dict begin
21 107 moveto
(Pfedit)
[7.68 4.08 6.24 6.96 3.84 3.84]
xshow
end grestore
end grestore

%	Pfedit -> Tacmach
newpath 67 115 moveto
81 117 99 118 115 120 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 115 123 moveto
125 122 lineto
116 117 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 115 123 moveto
125 122 lineto
116 117 lineto
closepath
stroke
end grestore

%	Evar_refiner
gsave 10 dict begin
163 18 49 18 ellipse_path
stroke
gsave 10 dict begin
127 13 moveto
(Evar_refiner)
[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56]
xshow
end grestore
end grestore

%	Pfedit -> Evar_refiner
newpath 53 96 moveto
67 82 90 60 112 45 curveto
116 42 120 40 124 37 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 126 40 moveto
133 32 lineto
123 34 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 126 40 moveto
133 32 lineto
123 34 lineto
closepath
stroke
end grestore

%	Evar_refiner -> Refiner
newpath 195 32 moveto
212 40 233 49 251 57 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 249 60 moveto
260 61 lineto
252 54 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 249 60 moveto
260 61 lineto
252 54 lineto
closepath
stroke
end grestore

%	Clenvtac
gsave 10 dict begin
38 45 38 18 ellipse_path
stroke
gsave 10 dict begin
13 40 moveto
(Clenvtac)
[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24]
xshow
end grestore
end grestore

%	Clenvtac -> Tacmach
newpath 58 61 moveto
73 72 93 87 112 99 curveto
117 102 123 105 128 108 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 127 111 moveto
137 113 lineto
130 105 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 127 111 moveto
137 113 lineto
130 105 lineto
closepath
stroke
end grestore

%	Clenvtac -> Evar_refiner
newpath 73 37 moveto
85 35 98 32 110 29 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 111 32 moveto
120 27 lineto
110 26 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 111 32 moveto
120 27 lineto
110 26 lineto
closepath
stroke
end grestore
endpage
showpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
end
restore
%%EOF