added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)
%!PS-Adobe-2.0
%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005)
%%For: (haftmann) Florian Haftmann
%%Title: _anonymous_0
%%Pages: (atend)
%%BoundingBox: 35 35 417 289
%%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 417 289
%%PageOrientation: Portrait
gsave
35 35 382 254 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0 0 translate 0 rotate
[ /CropBox [36 36 417 289] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% theory
gsave 10 dict begin
newpath 57 252 moveto
3 252 lineto
3 216 lineto
57 216 lineto
closepath
stroke
gsave 10 dict begin
11 229 moveto
(theory)
[4.08 6.96 6.24 6.96 4.8 6.96]
xshow
end grestore
end grestore
% selection
gsave 10 dict begin
149 234 38 18 ellipse_path
stroke
gsave 10 dict begin
124 229 moveto
(selection)
[5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
xshow
end grestore
end grestore
% theory -> selection
newpath 57 234 moveto
70 234 86 234 101 234 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 101 238 moveto
111 234 lineto
101 231 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 101 238 moveto
111 234 lineto
101 231 lineto
closepath
stroke
end grestore
% sml
gsave 10 dict begin
newpath 57 144 moveto
3 144 lineto
3 108 lineto
57 108 lineto
closepath
stroke
gsave 10 dict begin
15 121 moveto
(SML)
[7.68 12.48 8.64]
xshow
end grestore
end grestore
% other
gsave 10 dict begin
gsave 10 dict begin
24 67 moveto
(...)
[3.6 3.6 3.6]
xshow
end grestore
end grestore
% haskell
gsave 10 dict begin
newpath 60 36 moveto
0 36 lineto
0 0 lineto
60 0 lineto
closepath
stroke
gsave 10 dict begin
8 13 moveto
(Haskell)
[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
xshow
end grestore
end grestore
% preprocessing
gsave 10 dict begin
149 180 52 18 ellipse_path
stroke
gsave 10 dict begin
109 175 moveto
(preprocessing)
[6.96 4.56 6.24 6.96 4.56 6.96 6.24 6.24 5.52 5.52 3.84 6.96 6.96]
xshow
end grestore
end grestore
% selection -> preprocessing
newpath 149 216 moveto
149 213 149 211 149 208 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 153 208 moveto
149 198 lineto
146 208 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 153 208 moveto
149 198 lineto
146 208 lineto
closepath
stroke
end grestore
% code_thm
gsave 10 dict begin
newpath 358 198 moveto
260 198 lineto
260 162 lineto
358 162 lineto
closepath
stroke
gsave 10 dict begin
268 175 moveto
(code theorems)
[6.24 6.96 6.96 6.24 3.6 4.08 6.96 6.24 6.96 4.56 6.24 10.8 5.52]
xshow
end grestore
end grestore
% preprocessing -> code_thm
newpath 202 180 moveto
218 180 234 180 250 180 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 250 184 moveto
260 180 lineto
250 177 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 250 184 moveto
260 180 lineto
250 177 lineto
closepath
stroke
end grestore
% serialization
gsave 10 dict begin
149 72 47 18 ellipse_path
stroke
gsave 10 dict begin
114 67 moveto
(serialization)
[5.52 6.24 4.8 3.84 6.24 3.84 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
xshow
end grestore
end grestore
% serialization -> sml
newpath 118 86 moveto
102 94 83 102 66 110 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 65 107 moveto
57 114 lineto
68 113 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 65 107 moveto
57 114 lineto
68 113 lineto
closepath
stroke
end grestore
% serialization -> other
gsave 10 dict begin
dotted
newpath 101 72 moveto
90 72 78 72 67 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 67 69 moveto
57 72 lineto
67 76 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 67 69 moveto
57 72 lineto
67 76 lineto
closepath
stroke
end grestore
end grestore
% serialization -> haskell
newpath 118 58 moveto
103 51 85 43 69 36 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 71 33 moveto
60 32 lineto
68 39 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 71 33 moveto
60 32 lineto
68 39 lineto
closepath
stroke
end grestore
% extraction
gsave 10 dict begin
309 126 41 18 ellipse_path
stroke
gsave 10 dict begin
281 121 moveto
(extraction)
[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96]
xshow
end grestore
end grestore
% code_thm -> extraction
newpath 309 162 moveto
309 159 309 157 309 154 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 313 154 moveto
309 144 lineto
306 154 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 313 154 moveto
309 144 lineto
306 154 lineto
closepath
stroke
end grestore
% iml
gsave 10 dict begin
newpath 379 90 moveto
239 90 lineto
239 54 lineto
379 54 lineto
closepath
stroke
gsave 10 dict begin
246 67 moveto
(intermediate language)
[3.84 6.96 3.84 6.24 4.8 10.8 6.24 6.96 3.84 6.24 3.84 6.24 3.6 3.84 6.24 6.96 6.96 6.96 6.24 6.72 6.24]
xshow
end grestore
end grestore
% extraction -> iml
newpath 309 108 moveto
309 105 309 103 309 100 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 313 100 moveto
309 90 lineto
306 100 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 313 100 moveto
309 90 lineto
306 100 lineto
closepath
stroke
end grestore
% iml -> serialization
newpath 238 72 moveto
228 72 217 72 207 72 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
newpath 207 69 moveto
197 72 lineto
207 76 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
newpath 207 69 moveto
197 72 lineto
207 76 lineto
closepath
stroke
end grestore
endpage
showpage
grestore
%%PageTrailer
%%EndPage: 1
%%Trailer
%%Pages: 1
end
restore
%%EOF