summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/metapost/drv/template/template.mp
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/metapost/drv/template/template.mp')
-rw-r--r--Master/texmf-dist/doc/metapost/drv/template/template.mp45
1 files changed, 44 insertions, 1 deletions
diff --git a/Master/texmf-dist/doc/metapost/drv/template/template.mp b/Master/texmf-dist/doc/metapost/drv/template/template.mp
index 0875f9df042..019c8f12da7 100644
--- a/Master/texmf-dist/doc/metapost/drv/template/template.mp
+++ b/Master/texmf-dist/doc/metapost/drv/template/template.mp
@@ -1,6 +1,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
-% Structure of a MetaPost file using drv.mp
+% Structure of a MetaPost file using drv
% 1. Preamble
% input drv;
% verbatimtex %&latex
@@ -97,6 +97,9 @@ etex;
% drv_box_mode off;
% drv_fraction_mode on;
% drv_proof_mode off;
+% drv_radial_mode off;
+% drv_scale (crv, 1);
+% drv_azimuth 90;
beginfig(100)
jgm 0 "\Gamma, \Delta, \Theta, \Pi, \Upsilon\vdash F";
@@ -122,6 +125,46 @@ nfr 0 (1, 2) ("\text{cut}", 1);
draw drv_tree;
endfig;
+string Lor, Ror[], Land[], Rand;
+Lor:="\vee L";
+Ror1:="\vee R_1";
+Ror2:="\vee R_2";
+Land1:="\wedge L_1";
+Land2:="\wedge L_2";
+Rand:="\wedge R";
+
+beginfig(110)
+jgm 0 "p\wedge(q\vee(r_1\wedge r_2))\vdash p\wedge(q\vee(r_1\wedge r_2))";
+ jgm 1 "p\wedge(q\vee(r_1\wedge r_2))\vdash p";
+ jgm 2 "p\vdash p";
+ jgm 3 "p\wedge(q\vee(r_1\wedge r_2))\vdash q\vee(r_1\wedge r_2)";
+ jgm 4 "q\vee(r_1\wedge r_2)\vdash q\vee(r_1\wedge r_2)";
+ jgm 5 "q\vdash q\vee(r_1\wedge r_2)";
+ jgm 6 "q\vdash q";
+ jgm 7 "r_1\wedge r_2\vdash q\vee(r_1\wedge r_2)";
+ jgm 8 "r_1\wedge r_2\vdash r_1\wedge r_2";
+ jgm 9 "r_1\wedge r_2\vdash r_1";
+ jgm 10 "r_1\vdash r_1";
+ jgm 11 "r_1\wedge r_2\vdash r_2";
+ jgm 12 "r_2\vdash r_2";
+nfr 0 (1, 3) (Rand, 1);
+ nfr 1 (2) (Land1, 1);
+ nfr 2 () ("", 0);
+ nfr 3 (mvd 4 (1, 3)) (Land2, 1);
+ Nfr 4 (5, 7) (Lor, "\text{Id\,}_{q\vee(r_1\wedge r_2)}", "", 1);
+ nfr 5 (6) (Ror1, 1);
+ nfr 6 () ("", 0);
+ nfr 7 (mvd 8 (1, 3)) (Ror2, 1);
+ Nfr 8 (9, 11) (Rand, "\text{Id\,}_{r_1\wedge r_2}", "", 1);
+ nfr 9 (10) (Land1, 1);
+ nfr 10 () ("", 0);
+ nfr 11 (12) (Land2, 1);
+ nfr 12 () ("", 0);
+fill drv_bbox 4 withcolor (255, 230, 205)/255;
+fill drv_bbox 8 withcolor (236, 211, 185)/255;
+draw drv_tree;
+endfig;
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%