]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/whelp/engine.eps
absolute path and factorization for matita.basedir
[helm.git] / helm / papers / whelp / engine.eps
1 %!PS-Adobe-2.0 EPSF-2.0
2 %%Title: /home/zacchiro/dati/papers/moogle/engine.dia
3 %%Creator: Dia v0.94
4 %%CreationDate: Mon Mar 14 18:26:27 2005
5 %%For: zacchiro
6 %%Orientation: Portrait
7 %%Magnification: 1.0000
8 %%BoundingBox: 0 0 848 117
9 %%BeginSetup
10 %%EndSetup
11 %%EndComments
12 %%BeginProlog
13 [ /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
14 /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
15 /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
16 /.notdef /.notdef /space /exclam /quotedbl /numbersign /dollar /percent /ampersand /quoteright
17 /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash /zero /one
18 /two /three /four /five /six /seven /eight /nine /colon /semicolon
19 /less /equal /greater /question /at /A /B /C /D /E
20 /F /G /H /I /J /K /L /M /N /O
21 /P /Q /R /S /T /U /V /W /X /Y
22 /Z /bracketleft /backslash /bracketright /asciicircum /underscore /quoteleft /a /b /c
23 /d /e /f /g /h /i /j /k /l /m
24 /n /o /p /q /r /s /t /u /v /w
25 /x /y /z /braceleft /bar /braceright /asciitilde /.notdef /.notdef /.notdef
26 /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
27 /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
28 /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef
29 /space /exclamdown /cent /sterling /currency /yen /brokenbar /section /dieresis /copyright
30 /ordfeminine /guillemotleft /logicalnot /hyphen /registered /macron /degree /plusminus /twosuperior /threesuperior
31 /acute /mu /paragraph /periodcentered /cedilla /onesuperior /ordmasculine /guillemotright /onequarter /onehalf
32 /threequarters /questiondown /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla
33 /Egrave /Eacute /Ecircumflex /Edieresis /Igrave /Iacute /Icircumflex /Idieresis /Eth /Ntilde
34 /Ograve /Oacute /Ocircumflex /Otilde /Odieresis /multiply /Oslash /Ugrave /Uacute /Ucircumflex
35 /Udieresis /Yacute /Thorn /germandbls /agrave /aacute /acircumflex /atilde /adieresis /aring
36 /ae /ccedilla /egrave /eacute /ecircumflex /edieresis /igrave /iacute /icircumflex /idieresis
37 /eth /ntilde /ograve /oacute /ocircumflex /otilde /odieresis /divide /oslash /ugrave
38 /uacute /ucircumflex /udieresis /yacute /thorn /ydieresis] /isolatin1encoding exch def
39 /cp {closepath} bind def
40 /c {curveto} bind def
41 /f {fill} bind def
42 /a {arc} bind def
43 /ef {eofill} bind def
44 /ex {exch} bind def
45 /gr {grestore} bind def
46 /gs {gsave} bind def
47 /sa {save} bind def
48 /rs {restore} bind def
49 /l {lineto} bind def
50 /m {moveto} bind def
51 /rm {rmoveto} bind def
52 /n {newpath} bind def
53 /s {stroke} bind def
54 /sh {show} bind def
55 /slc {setlinecap} bind def
56 /slj {setlinejoin} bind def
57 /slw {setlinewidth} bind def
58 /srgb {setrgbcolor} bind def
59 /rot {rotate} bind def
60 /sc {scale} bind def
61 /sd {setdash} bind def
62 /ff {findfont} bind def
63 /sf {setfont} bind def
64 /scf {scalefont} bind def
65 /sw {stringwidth pop} bind def
66 /tr {translate} bind def
67
68 /ellipsedict 8 dict def
69 ellipsedict /mtrx matrix put
70 /ellipse
71 { ellipsedict begin
72    /endangle exch def
73    /startangle exch def
74    /yrad exch def
75    /xrad exch def
76    /y exch def
77    /x exch def   /savematrix mtrx currentmatrix def
78    x y tr xrad yrad sc
79    0 0 1 startangle endangle arc
80    savematrix setmatrix
81    end
82 } def
83
84 /mergeprocs {
85 dup length
86 3 -1 roll
87 dup
88 length
89 dup
90 5 1 roll
91 3 -1 roll
92 add
93 array cvx
94 dup
95 3 -1 roll
96 0 exch
97 putinterval
98 dup
99 4 2 roll
100 putinterval
101 } bind def
102 /Times-Roman-latin1
103     /Times-Roman findfont
104     dup length dict begin
105         {1 index /FID ne {def} {pop pop} ifelse} forall
106         /Encoding isolatin1encoding def
107     currentdict end
108 definefont pop
109 /Times-Italic-latin1
110     /Times-Italic findfont
111     dup length dict begin
112         {1 index /FID ne {def} {pop pop} ifelse} forall
113         /Encoding isolatin1encoding def
114     currentdict end
115 definefont pop
116 /Times-Bold-latin1
117     /Times-Bold findfont
118     dup length dict begin
119         {1 index /FID ne {def} {pop pop} ifelse} forall
120         /Encoding isolatin1encoding def
121     currentdict end
122 definefont pop
123 /Times-BoldItalic-latin1
124     /Times-BoldItalic findfont
125     dup length dict begin
126         {1 index /FID ne {def} {pop pop} ifelse} forall
127         /Encoding isolatin1encoding def
128     currentdict end
129 definefont pop
130 /AvantGarde-Book-latin1
131     /AvantGarde-Book findfont
132     dup length dict begin
133         {1 index /FID ne {def} {pop pop} ifelse} forall
134         /Encoding isolatin1encoding def
135     currentdict end
136 definefont pop
137 /AvantGarde-BookOblique-latin1
138     /AvantGarde-BookOblique findfont
139     dup length dict begin
140         {1 index /FID ne {def} {pop pop} ifelse} forall
141         /Encoding isolatin1encoding def
142     currentdict end
143 definefont pop
144 /AvantGarde-Demi-latin1
145     /AvantGarde-Demi findfont
146     dup length dict begin
147         {1 index /FID ne {def} {pop pop} ifelse} forall
148         /Encoding isolatin1encoding def
149     currentdict end
150 definefont pop
151 /AvantGarde-DemiOblique-latin1
152     /AvantGarde-DemiOblique findfont
153     dup length dict begin
154         {1 index /FID ne {def} {pop pop} ifelse} forall
155         /Encoding isolatin1encoding def
156     currentdict end
157 definefont pop
158 /Bookman-Light-latin1
159     /Bookman-Light findfont
160     dup length dict begin
161         {1 index /FID ne {def} {pop pop} ifelse} forall
162         /Encoding isolatin1encoding def
163     currentdict end
164 definefont pop
165 /Bookman-LightItalic-latin1
166     /Bookman-LightItalic findfont
167     dup length dict begin
168         {1 index /FID ne {def} {pop pop} ifelse} forall
169         /Encoding isolatin1encoding def
170     currentdict end
171 definefont pop
172 /Bookman-Demi-latin1
173     /Bookman-Demi findfont
174     dup length dict begin
175         {1 index /FID ne {def} {pop pop} ifelse} forall
176         /Encoding isolatin1encoding def
177     currentdict end
178 definefont pop
179 /Bookman-DemiItalic-latin1
180     /Bookman-DemiItalic findfont
181     dup length dict begin
182         {1 index /FID ne {def} {pop pop} ifelse} forall
183         /Encoding isolatin1encoding def
184     currentdict end
185 definefont pop
186 /Courier-latin1
187     /Courier findfont
188     dup length dict begin
189         {1 index /FID ne {def} {pop pop} ifelse} forall
190         /Encoding isolatin1encoding def
191     currentdict end
192 definefont pop
193 /Courier-Oblique-latin1
194     /Courier-Oblique findfont
195     dup length dict begin
196         {1 index /FID ne {def} {pop pop} ifelse} forall
197         /Encoding isolatin1encoding def
198     currentdict end
199 definefont pop
200 /Courier-Bold-latin1
201     /Courier-Bold findfont
202     dup length dict begin
203         {1 index /FID ne {def} {pop pop} ifelse} forall
204         /Encoding isolatin1encoding def
205     currentdict end
206 definefont pop
207 /Courier-BoldOblique-latin1
208     /Courier-BoldOblique findfont
209     dup length dict begin
210         {1 index /FID ne {def} {pop pop} ifelse} forall
211         /Encoding isolatin1encoding def
212     currentdict end
213 definefont pop
214 /Helvetica-latin1
215     /Helvetica findfont
216     dup length dict begin
217         {1 index /FID ne {def} {pop pop} ifelse} forall
218         /Encoding isolatin1encoding def
219     currentdict end
220 definefont pop
221 /Helvetica-Oblique-latin1
222     /Helvetica-Oblique findfont
223     dup length dict begin
224         {1 index /FID ne {def} {pop pop} ifelse} forall
225         /Encoding isolatin1encoding def
226     currentdict end
227 definefont pop
228 /Helvetica-Bold-latin1
229     /Helvetica-Bold findfont
230     dup length dict begin
231         {1 index /FID ne {def} {pop pop} ifelse} forall
232         /Encoding isolatin1encoding def
233     currentdict end
234 definefont pop
235 /Helvetica-BoldOblique-latin1
236     /Helvetica-BoldOblique findfont
237     dup length dict begin
238         {1 index /FID ne {def} {pop pop} ifelse} forall
239         /Encoding isolatin1encoding def
240     currentdict end
241 definefont pop
242 /Helvetica-Narrow-latin1
243     /Helvetica-Narrow findfont
244     dup length dict begin
245         {1 index /FID ne {def} {pop pop} ifelse} forall
246         /Encoding isolatin1encoding def
247     currentdict end
248 definefont pop
249 /Helvetica-Narrow-Oblique-latin1
250     /Helvetica-Narrow-Oblique findfont
251     dup length dict begin
252         {1 index /FID ne {def} {pop pop} ifelse} forall
253         /Encoding isolatin1encoding def
254     currentdict end
255 definefont pop
256 /Helvetica-Narrow-Bold-latin1
257     /Helvetica-Narrow-Bold findfont
258     dup length dict begin
259         {1 index /FID ne {def} {pop pop} ifelse} forall
260         /Encoding isolatin1encoding def
261     currentdict end
262 definefont pop
263 /Helvetica-Narrow-BoldOblique-latin1
264     /Helvetica-Narrow-BoldOblique findfont
265     dup length dict begin
266         {1 index /FID ne {def} {pop pop} ifelse} forall
267         /Encoding isolatin1encoding def
268     currentdict end
269 definefont pop
270 /NewCenturySchoolbook-Roman-latin1
271     /NewCenturySchoolbook-Roman findfont
272     dup length dict begin
273         {1 index /FID ne {def} {pop pop} ifelse} forall
274         /Encoding isolatin1encoding def
275     currentdict end
276 definefont pop
277 /NewCenturySchoolbook-Italic-latin1
278     /NewCenturySchoolbook-Italic findfont
279     dup length dict begin
280         {1 index /FID ne {def} {pop pop} ifelse} forall
281         /Encoding isolatin1encoding def
282     currentdict end
283 definefont pop
284 /NewCenturySchoolbook-Bold-latin1
285     /NewCenturySchoolbook-Bold findfont
286     dup length dict begin
287         {1 index /FID ne {def} {pop pop} ifelse} forall
288         /Encoding isolatin1encoding def
289     currentdict end
290 definefont pop
291 /NewCenturySchoolbook-BoldItalic-latin1
292     /NewCenturySchoolbook-BoldItalic findfont
293     dup length dict begin
294         {1 index /FID ne {def} {pop pop} ifelse} forall
295         /Encoding isolatin1encoding def
296     currentdict end
297 definefont pop
298 /Palatino-Roman-latin1
299     /Palatino-Roman findfont
300     dup length dict begin
301         {1 index /FID ne {def} {pop pop} ifelse} forall
302         /Encoding isolatin1encoding def
303     currentdict end
304 definefont pop
305 /Palatino-Italic-latin1
306     /Palatino-Italic findfont
307     dup length dict begin
308         {1 index /FID ne {def} {pop pop} ifelse} forall
309         /Encoding isolatin1encoding def
310     currentdict end
311 definefont pop
312 /Palatino-Bold-latin1
313     /Palatino-Bold findfont
314     dup length dict begin
315         {1 index /FID ne {def} {pop pop} ifelse} forall
316         /Encoding isolatin1encoding def
317     currentdict end
318 definefont pop
319 /Palatino-BoldItalic-latin1
320     /Palatino-BoldItalic findfont
321     dup length dict begin
322         {1 index /FID ne {def} {pop pop} ifelse} forall
323         /Encoding isolatin1encoding def
324     currentdict end
325 definefont pop
326 /Symbol-latin1
327     /Symbol findfont
328 definefont pop
329 /ZapfChancery-MediumItalic-latin1
330     /ZapfChancery-MediumItalic findfont
331     dup length dict begin
332         {1 index /FID ne {def} {pop pop} ifelse} forall
333         /Encoding isolatin1encoding def
334     currentdict end
335 definefont pop
336 /ZapfDingbats-latin1
337     /ZapfDingbats findfont
338     dup length dict begin
339         {1 index /FID ne {def} {pop pop} ifelse} forall
340         /Encoding isolatin1encoding def
341     currentdict end
342 definefont pop
343 28.346000 -28.346000 scale
344 3.875000 -17.750000 translate
345 %%EndProlog
346
347
348 1.000000 1.000000 1.000000 srgb
349 n -0.150000 13.700000 m -0.150000 17.700000 l 21.450000 17.700000 l 21.450000 13.700000 l f
350 n -0.150000 14.200000 m -0.150000 14.200000 0.500000 0.500000 180.000000 270.000000 ellipse f
351 n 21.450000 14.200000 m 21.450000 14.200000 0.500000 0.500000 270.000000 360.000000 ellipse f
352 n -0.650000 14.200000 m -0.650000 17.200000 l 21.950000 17.200000 l 21.950000 14.200000 l f
353 n -0.150000 17.200000 m -0.150000 17.200000 0.500000 0.500000 90.000000 180.000000 ellipse f
354 n 21.450000 17.200000 m 21.450000 17.200000 0.500000 0.500000 0.000000 90.000000 ellipse f
355 0.100000 slw
356 [0.200000] 0 sd
357 [0.200000] 0 sd
358 0 slj
359 0.000000 0.000000 0.000000 srgb
360 n -0.150000 13.700000 m 21.450000 13.700000 l s
361 n -0.150000 17.700000 m 21.450000 17.700000 l s
362 n -0.150000 14.200000 0.500000 0.500000 180.000000 270.000000 ellipse s
363 n 21.450000 14.200000 0.500000 0.500000 270.000000 360.000000 ellipse s
364 n -0.650000 14.200000 m -0.650000 17.200000 l s
365 n 21.950000 14.200000 m 21.950000 17.200000 l s
366 n -0.150000 17.200000 0.500000 0.500000 90.000000 180.000000 ellipse s
367 n 21.450000 17.200000 0.500000 0.500000 0.000000 90.000000 ellipse s
368 1.000000 1.000000 1.000000 srgb
369 n 7.825000 15.050000 m 7.825000 16.950000 l 14.425000 16.950000 l 14.425000 15.050000 l f
370 0.100000 slw
371 [] 0 sd
372 [] 0 sd
373 0 slj
374 0.000000 0.000000 0.000000 srgb
375 n 7.825000 15.050000 m 7.825000 16.950000 l 14.425000 16.950000 l 14.425000 15.050000 l cp s
376 /Helvetica-latin1 ff 0.560000 scf sf
377 (disambiguation) dup sw 2 div 11.125000 ex sub 16.200000 m gs 1 -1 sc sh gr
378 /Helvetica-latin1 ff 0.560000 scf sf
379 (user) dup sw 2 div -2.850000 ex sub 15.875000 m gs 1 -1 sc sh gr
380 (query) dup sw 2 div -2.850000 ex sub 16.675000 m gs 1 -1 sc sh gr
381 0.100000 slw
382 [] 0 sd
383 [] 0 sd
384 0 slc
385 n -1.750000 16.035000 m 0.008256 16.007588 l s
386 [] 0 sd
387 0 slj
388 0 slc
389 n 0.383210 16.001743 m -0.112832 16.259507 l 0.008256 16.007588 l -0.120626 15.759567 l ef
390 n 0.383210 16.001743 m -0.112832 16.259507 l 0.008256 16.007588 l -0.120626 15.759567 l cp s
391 1.000000 1.000000 1.000000 srgb
392 n 17.845000 15.050000 m 17.845000 16.950000 l 20.995000 16.950000 l 20.995000 15.050000 l f
393 0.100000 slw
394 [] 0 sd
395 [] 0 sd
396 0 slj
397 0.000000 0.000000 0.000000 srgb
398 n 17.845000 15.050000 m 17.845000 16.950000 l 20.995000 16.950000 l 20.995000 15.050000 l cp s
399 /Helvetica-latin1 ff 0.560000 scf sf
400 (query) dup sw 2 div 19.420000 ex sub 16.200000 m gs 1 -1 sc sh gr
401 0.100000 slw
402 [] 0 sd
403 [] 0 sd
404 0 slc
405 n 14.425000 16.000000 m 17.358197 16.000000 l s
406 [] 0 sd
407 0 slj
408 0 slc
409 n 17.733197 16.000000 m 17.233197 16.250000 l 17.358197 16.000000 l 17.233197 15.750000 l ef
410 n 17.733197 16.000000 m 17.233197 16.250000 l 17.358197 16.000000 l 17.233197 15.750000 l cp s
411 /Helvetica-latin1 ff 0.560000 scf sf
412 (CIC) dup sw 2 div 16.070000 ex sub 14.621250 m gs 1 -1 sc sh gr
413 (term) dup sw 2 div 16.070000 ex sub 15.421250 m gs 1 -1 sc sh gr
414 0.100000 slw
415 [] 0 sd
416 [] 0 sd
417 0 slc
418 n 20.995000 16.000000 m 22.863197 16.000000 l s
419 [] 0 sd
420 0 slj
421 0 slc
422 n 23.238197 16.000000 m 22.738197 16.250000 l 22.863197 16.000000 l 22.738197 15.750000 l ef
423 n 23.238197 16.000000 m 22.738197 16.250000 l 22.863197 16.000000 l 22.738197 15.750000 l cp s
424 /Helvetica-latin1 ff 0.560000 scf sf
425 (results) dup sw 2 div 24.770000 ex sub 15.725000 m gs 1 -1 sc sh gr
426 (\(URIs\)) dup sw 2 div 24.770000 ex sub 16.525000 m gs 1 -1 sc sh gr
427 0.100000 slw
428 [] 0 sd
429 [] 0 sd
430 0 slc
431 n 4.295000 16.000000 m 7.338197 16.000000 l s
432 [] 0 sd
433 0 slj
434 0 slc
435 n 7.713197 16.000000 m 7.213197 16.250000 l 7.338197 16.000000 l 7.213197 15.750000 l ef
436 n 7.713197 16.000000 m 7.213197 16.250000 l 7.338197 16.000000 l 7.213197 15.750000 l cp s
437 /Helvetica-latin1 ff 0.560000 scf sf
438 1.000000 1.000000 1.000000 srgb
439 n 0.495000 15.050000 m 0.495000 16.950000 l 4.295000 16.950000 l 4.295000 15.050000 l f
440 0.100000 slw
441 [] 0 sd
442 [] 0 sd
443 0 slj
444 0.000000 0.000000 0.000000 srgb
445 n 0.495000 15.050000 m 0.495000 16.950000 l 4.295000 16.950000 l 4.295000 15.050000 l cp s
446 /Helvetica-latin1 ff 0.560000 scf sf
447 (parsing) dup sw 2 div 2.395000 ex sub 16.200000 m gs 1 -1 sc sh gr
448 /Helvetica-latin1 ff 0.560000 scf sf
449 (AST) dup sw 2 div 6.020000 ex sub 15.465000 m gs 1 -1 sc sh gr
450 showpage