/usr/share/texlive/texmf-dist/metapost/metaobj/proofex.mp is in texlive-metapost 2015.20160320-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | % D. Roegel, 20/5/2001
input metaobj
% Proof from
% David, Nour, Raffalli: Introduction à la logique, Paris: Dunod, 2001
% p. 197
verbatimtex
\newcount\pntcnt
\pntcnt=0
\def\npoints#1{\pntcnt=#1\vbox{\offinterlineskip\kern5pt\npointsa}}
\def\npointsa{\ifnum\pntcnt>0\hbox{$.$}\kern5pt\advance\pntcnt-1
\expandafter\npointsa\fi}
etex
beginfig(1);
% setObjectDefaultOption("PTree")("treemode")("U"); % default is down
newAssumption.pi1(btex $\Pi_1$ etex);
newConclusion.pi1c1(btex \npoints3 etex);
newPTreeR.pi1proof(pi1c1)(pi1)("") "rule(0)";
newConclusion.pi1c2(btex $\Gamma,B \vdash \Delta$ etex);
newPTreeR.a1(pi1c2)(pi1proof)("") "rule(0)";
newAssumption.pi2(btex $\Pi_2$ etex);
newConclusion.pi2c1(btex \npoints3 etex);
newPTreeR.pi2proof(pi2c1)(pi2)("") "rule(0)";
newConclusion.pi2c2(btex $\Gamma,C \vdash \Delta$ etex);
newPTreeR.a2(pi2c2)(pi2proof)("") "rule(0)";
newConclusion.c1(btex $\Gamma,B\lor C \vdash \Delta$ etex);
newPTreeR.proof1(c1)(a1,a2)(btex $\lor_g$ etex);
newAssumption.pi3(btex $\Pi_3$ etex);
newConclusion.pi3c1(btex \npoints3 etex);
newPTreeR.pi3proof(pi3c1)(pi3)("") "rule(0)";
newConclusion.pi3c2(btex $\Gamma' \vdash B,C, \Delta'$ etex);
newPTreeR.a3(pi3c2)(pi3proof)("") "rule(0)";
newConclusion.c2
(btex $\Gamma_A,\Gamma'\vdash B,C,\Delta,\Delta'_A$ etex);
newPTreeR.proof2(c2)(proof1,a3)(btex {\it mix\/}$(1)$ etex);
newConclusion.c2points
(btex $\npoints{12}$ etex);
newPTreeR.proof2a(c2points)(proof2)("") "rule(0)";
duplicateObj(a4,a1);
duplicateObj(a5,a3);
newConclusion.c3(btex $\Gamma' \vdash B\lor C, \Delta'$ etex);
newPTreeR.proof3(c3)(a5)(btex $\lor_d$ etex);
newConclusion.c4(btex $\Gamma_A,\Gamma',B \vdash \Delta, \Delta'_A$ etex);
newPTreeR.proof4(c4)(a4,proof3)(btex {\it mix\/}$(2)$ etex);
newConclusion.c5(btex $\Gamma_A,\Gamma',\Gamma_A,\Gamma'
\vdash C,\Delta, \Delta'_A,\Delta, \Delta'_A$ etex);
newHRazor.hr1(-4cm);
newPTreeR.proof5(c5)(proof2a,hr1,proof4)(btex {\it mix\/}$(3)$ etex);
duplicateObj(a6,a2);
duplicateObj(proof3a,proof3);
newConclusion.c7(btex $\Gamma_A,\Gamma',C
\vdash \Delta, \Delta'_A$ etex);
newPTreeR.proof3b(c7)(a6,proof3a)(btex {\it mix\/}$(4)$ etex);
newConclusion.c8(btex $\Gamma_A,\Gamma',\Gamma_A,\Gamma',\Gamma_A,\Gamma'
\vdash \Delta, \Delta'_A,\Delta, \Delta'_A,\Delta, \Delta'_A$ etex);
newPTreeR.proof3d(c8)(proof5,proof3b)(btex {\it mix\/}$(5)$ etex)
"hsep(5mm)";
newConclusion.c9(btex $\Gamma_A,\Gamma'\vdash \Delta, \Delta'_A$ etex);
newPTreeR.proof3E(c9)(proof3d)(btex contr$_g$,contr$_d$ etex);
%yscaleObj(proof3E,2);
%reflectObj(proof3E,(0,0),(0,1));
%slantObj(proof3E,0.2);
proof3E.c=origin;
drawObj(proof3E);
endfig;
clearObj pi,a,c,proof,hr;
beginfig(2);
setObjectDefaultOption("PTree")("treemode")("U"); % default is down
newAssumption.pi1(btex $\Pi_1$ etex);
newConclusion.pi1c1(btex \npoints3 etex);
newPTreeR.pi1proof(pi1c1)(pi1)("") "rule(0)";
newConclusion.pi1c2(btex $\Gamma,B \vdash \Delta$ etex);
newPTreeR.a1(pi1c2)(pi1proof)("") "rule(0)";
newAssumption.pi2(btex $\Pi_2$ etex);
newConclusion.pi2c1(btex \npoints3 etex);
newPTreeR.pi2proof(pi2c1)(pi2)("") "rule(0)";
newConclusion.pi2c2(btex $\Gamma,C \vdash \Delta$ etex);
newPTreeR.a2(pi2c2)(pi2proof)("") "rule(0)";
newConclusion.c1(btex $\Gamma,B\lor C \vdash \Delta$ etex);
newPTreeR.proof1(c1)(a1,a2)(btex $\lor_g$ etex);
newAssumption.pi3(btex $\Pi_3$ etex);
newConclusion.pi3c1(btex \npoints3 etex);
newPTreeR.pi3proof(pi3c1)(pi3)("") "rule(0)";
newConclusion.pi3c2(btex $\Gamma' \vdash B,C, \Delta'$ etex);
newPTreeR.a3(pi3c2)(pi3proof)("") "rule(0)";
newConclusion.c2
(btex $\Gamma_A,\Gamma'\vdash B,C,\Delta,\Delta'_A$ etex);
newPTreeR.proof2(c2)(proof1,a3)(btex {\it mix\/}$(1)$ etex);
newConclusion.c2points
(btex $\npoints{12}$ etex);
newPTreeR.proof2a(c2points)(proof2)("") "rule(0)";
duplicateObj(a4,a1);
duplicateObj(a5,a3);
newConclusion.c3(btex $\Gamma' \vdash B\lor C, \Delta'$ etex);
newPTreeR.proof3(c3)(a5)(btex $\lor_d$ etex);
newConclusion.c4(btex $\Gamma_A,\Gamma',B \vdash \Delta, \Delta'_A$ etex);
newPTreeR.proof4(c4)(a4,proof3)(btex {\it mix\/}$(2)$ etex);
newConclusion.c5(btex $\Gamma_A,\Gamma',\Gamma_A,\Gamma'
\vdash C,\Delta, \Delta'_A,\Delta, \Delta'_A$ etex);
newHRazor.hr1(-4cm);
newPTreeR.proof5(c5)(proof2a,hr1,proof4)(btex {\it mix\/}$(3)$ etex);
duplicateObj(a6,a2);
duplicateObj(proof3a,proof3);
newConclusion.c7(btex $\Gamma_A,\Gamma',C
\vdash \Delta, \Delta'_A$ etex);
newPTreeR.proof3b(c7)(a6,proof3a)(btex {\it mix\/}$(4)$ etex);
newConclusion.c8(btex $\Gamma_A,\Gamma',\Gamma_A,\Gamma',\Gamma_A,\Gamma'
\vdash \Delta, \Delta'_A,\Delta, \Delta'_A,\Delta, \Delta'_A$ etex);
newPTreeR.proof3d(c8)(proof5,proof3b)(btex {\it mix\/}$(5)$ etex)
"hsep(5mm)";
newConclusion.c9(btex $\Gamma_A,\Gamma'\vdash \Delta, \Delta'_A$ etex);
newPTreeR.proof3E(c9)(proof3d)(btex contr$_g$,contr$_d$ etex);
%yscaleObj(proof3E,2);
%reflectObj(proof3E,(0,0),(0,1));
%slantObj(proof3E,0.2);
proof3E.c=origin;
drawObj(proof3E);
endfig;
end
|