blob: fda7a33c2ebe525609617324d9250d40cc79be1f (
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
|
%!PS-Adobe-2.0
%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
%%For: (notin) Jean-Marc Notin,,,
%%Title: G
%%Pages: (atend)
%%BoundingBox: (atend)
%%EndComments
save
%%BeginProlog
/DotDict 200 dict def
DotDict begin
/setupLatin1 {
mark
/EncodingVector 256 array def
EncodingVector 0
ISOLatin1Encoding 0 255 getinterval putinterval
EncodingVector 45 /hyphen put
% 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
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
setupLatin1
%%Page: 1 1
%%PageBoundingBox: 36 36 576 753
%%PageOrientation: Landscape
gsave
36 36 576 753 boxprim clip newpath
0 0 1 beginpage
0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate
0.000 0.000 1.000 graphcolor
newpath -4 -4 moveto
-4 544 lineto
724 544 lineto
724 -4 lineto
closepath fill
0.985401 setlinewidth
0.000 0.000 1.000 graphcolor
newpath -4 -4 moveto
-4 544 lineto
724 544 lineto
724 -4 lineto
closepath stroke
% Constrextern
gsave
0.502 1.000 0.820 nodecolor
172 417 49.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
172 417 49.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
172 412 moveto 72 -0.5 (Constrextern) alignedtext
grestore
% Reserve
gsave
0.502 1.000 0.820 nodecolor
264 319 35.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
264 319 35.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
264 314 moveto 44 -0.5 (Reserve) alignedtext
grestore
% Constrextern->Reserve
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 188 400 moveto
203 384 225 361 242 343 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 245.049 344.831 moveto
249 335 lineto
239.781 340.221 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 245.049 344.831 moveto
249 335 lineto
239.781 340.221 lineto
closepath stroke
grestore
% Notation
gsave
0.502 1.000 0.820 nodecolor
268 122 37.1753 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
268 122 37.1753 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
268 117 moveto 49 -0.5 (Notation) alignedtext
grestore
% Constrextern->Notation
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 178 399 moveto
194 349 240 209 259 150 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 262.479 150.584 moveto
262 140 lineto
255.774 148.573 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 262.479 150.584 moveto
262 140 lineto
255.774 148.573 lineto
closepath stroke
grestore
% Topconstr
gsave
0.502 1.000 0.820 nodecolor
82 24 41.1755 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
82 24 41.1755 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
82 19 moveto 57 -0.5 (Topconstr) alignedtext
grestore
% Notation->Topconstr
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 243 109 moveto
211 91 154 62 117 43 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 118.441 39.7969 moveto
108 38 lineto
115.042 45.916 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 118.441 39.7969 moveto
108 38 lineto
115.042 45.916 lineto
closepath stroke
grestore
% Ppextend
gsave
0.502 1.000 0.820 nodecolor
278 24 39.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
278 24 39.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
278 19 moveto 52 -0.5 (Ppextend) alignedtext
grestore
% Notation->Ppextend
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 270 104 moveto
272 89 273 68 275 52 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 278.488 52.2987 moveto
276 42 lineto
271.522 51.6021 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 278.488 52.2987 moveto
276 42 lineto
271.522 51.6021 lineto
closepath stroke
grestore
% Constrintern
gsave
0.502 1.000 0.820 nodecolor
472 417 48.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
472 417 48.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
472 412 moveto 70 -0.5 (Constrintern) alignedtext
grestore
% Constrintern->Reserve
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 442 403 moveto
404 385 340 355 299 335 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 300.56 331.863 moveto
290 331 lineto
297.717 338.26 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 300.56 331.863 moveto
290 331 lineto
297.717 338.26 lineto
closepath stroke
grestore
% Implicit_quantifiers
gsave
0.502 1.000 0.820 nodecolor
508 319 69.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
508 319 69.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
508 314 moveto 112 -0.5 (Implicit_quantifiers) alignedtext
grestore
% Constrintern->Implicit_quantifiers
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 479 399 moveto
484 385 492 364 498 347 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 501.479 347.584 moveto
501 337 lineto
494.774 345.573 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 501.479 347.584 moveto
501 337 lineto
494.774 345.573 lineto
closepath stroke
grestore
% Syntax_def
gsave
0.502 1.000 0.820 nodecolor
396 220 45.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
396 220 45.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
396 215 moveto 64 -0.5 (Syntax_def) alignedtext
grestore
% Implicit_quantifiers->Syntax_def
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 488 302 moveto
469 285 442 261 422 244 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 424.546 241.596 moveto
415 237 lineto
419.596 246.546 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 424.546 241.596 moveto
415 237 lineto
419.596 246.546 lineto
closepath stroke
grestore
% Coqlib
gsave
0.502 1.000 0.820 nodecolor
656 515 32.1777 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
656 515 32.1777 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
656 510 moveto 38 -0.5 (Coqlib) alignedtext
grestore
% Genarg
gsave
0.502 1.000 0.820 nodecolor
82 122 33.175 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
82 122 33.175 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
82 117 moveto 41 -0.5 (Genarg) alignedtext
grestore
% Genarg->Topconstr
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 82 104 moveto
82 89 82 69 82 52 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 85.5001 52 moveto
82 42 lineto
78.5001 52 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 85.5001 52 moveto
82 42 lineto
78.5001 52 lineto
closepath stroke
grestore
% Syntax_def->Notation
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 375 204 moveto
354 187 320 161 296 143 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 298.1 140.2 moveto
288 137 lineto
293.9 145.8 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 298.1 140.2 moveto
288 137 lineto
293.9 145.8 lineto
closepath stroke
grestore
% Modintern
gsave
0.502 1.000 0.820 nodecolor
472 515 42.1756 18 ellipse_path fill
0.985401 setlinewidth
filled
0.502 1.000 0.820 nodecolor
472 515 42.1756 18 ellipse_path stroke
0.000 0.000 0.000 nodecolor
14.00 /Times-Roman set_font
472 510 moveto 59 -0.5 (Modintern) alignedtext
grestore
% Modintern->Constrintern
gsave
0.985401 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 472 497 moveto
472 482 472 462 472 445 curveto
stroke
0.000 0.000 0.000 edgecolor
newpath 475.5 445 moveto
472 435 lineto
468.5 445 lineto
closepath fill
0.985401 setlinewidth
solid
0.000 0.000 0.000 edgecolor
newpath 475.5 445 moveto
472 435 lineto
468.5 445 lineto
closepath stroke
grestore
endpage
showpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
%%BoundingBox: 36 36 576 753
end
restore
%%EOF
|
