diff options
Diffstat (limited to 'Master/texmf-dist/doc/metapost/drv/template/template.mp')
-rw-r--r-- | Master/texmf-dist/doc/metapost/drv/template/template.mp | 45 |
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; + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % |