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
|
input drv;
verbatimtex %&latex
% Any piece of code related to font selection in the preambule of
% `coq-sample.tex' (document class, font package, font selection commands ...)
% should be reported here.
\documentclass[8pt]{beamer}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage[varg]{txfonts}
\newcommand{\var}{\text{Var}}
\newcommand{\app}{\text{App}}
\newcommand{\lam}{\text{Lam}}
\begin{document}
etex;
drv_font_size "\small";
drv_labels_position l;
for index=0 upto 6:
beginfig(index)
jgm 0 "\vdash", "(P\to(Q\to R))\to(Q\to(P\to R))";
jgm 1 "P\to(Q\to R)\vdash", "Q\to(P\to R)";
jgm 2 "P\to(Q\to R), Q\vdash", "P\to R";
jgm 3 "P\to(Q\to R), Q, P\vdash", "R";
jgm 4 "P\to(Q\to R), Q, P\vdash", "Q\to R";
jgm 5 "P\to(Q\to R), Q, P\vdash", "P\to(Q\to R)";
jgm 6 "P\to(Q\to R), Q, P\vdash", "P";
jgm 7 "P\to(Q\to R), Q, P\vdash", "Q";
nfr 0 (1) ("\lam", 1);
nfr 1 (2) ("\lam", 1);
nfr 2 (3) ("\lam", 1);
nfr 3 (4, 7) ("\app", 1);
nfr 4 (5, 6) ("\app", 1);
nfr 5 () ("\var", 1);
nfr 6 () ("\var", 1);
nfr 7 () ("\var", 1);
setbounds currentpicture to drv_bbox 0;
% All the pictures will have the same bounding box
% as the complete derivation tree.
draw sbj[0][0];
if index=0:
draw sbj[0][1] withcolor blue;
else:
draw sbj[0][1];
draw iln[0];
draw l_ilb[0];
draw sbj[1][0];
if index=1:
draw sbj[1][1] withcolor blue;
else:
draw sbj[1][1];
draw iln[1];
draw l_ilb[1];
draw sbj[2][0];
if index=2:
draw sbj[2][1] withcolor blue;
else:
draw sbj[2][1];
draw iln[2];
draw l_ilb[2];
draw sbj[3][0];
if index=3:
draw sbj[3][1] withcolor blue;
else:
draw sbj[3][1];
draw iln[3];
draw l_ilb[3];
draw jdg[4];
draw iln[4];
draw l_ilb[4];
draw jdg[5];
draw iln[5];
draw l_ilb[5];
draw sbj[6][0];
draw sbj[7][0];
if index=4:
draw sbj[6][1] withcolor blue;
draw sbj[7][1] withcolor blue;
else:
draw sbj[6][1];
draw iln[6];
draw l_ilb[6];
if index=5:
draw sbj[7][1] withcolor blue;
else:
draw sbj[7][1];
draw iln[7];
draw l_ilb[7];
fi
fi
fi
fi
fi
fi
endfig;
endfor
end
|