diff options
author | Karl Berry <karl@freefriends.org> | 2014-12-02 00:55:36 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2014-12-02 00:55:36 +0000 |
commit | ab4c97bb1913e7167819b3e3c2688a0e5200f011 (patch) | |
tree | 3a92d1b788fa89ea4c49b249e57e80162208cb55 /Master/texmf-dist/tex/latex/prftree | |
parent | 5a51ac01bebab92f1bb7e8f4091a423e5ac6905d (diff) |
prftree (1dec14)
git-svn-id: svn://tug.org/texlive/trunk@35712 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/prftree')
-rw-r--r-- | Master/texmf-dist/tex/latex/prftree/prftree.sty | 1046 |
1 files changed, 1046 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty new file mode 100644 index 00000000000..8396b7b9cf5 --- /dev/null +++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty @@ -0,0 +1,1046 @@ +% +% prftree.sty +% by Marco Benini - 30th November 2014 +% +% A package to typeset natural deduction proofs, or sequent proofs, or +% tableau proofs +% +% This package is distributed under the GNU General Public License +% + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{prftree}[2014/11/30 Natural Deduction Proofs] + +% Package options +\newif\ifprf@NDOption\prf@NDOptionfalse +\newif\ifprf@SEQOption\prf@SEQOptionfalse +\newif\ifprfIMPOption\prfIMPOptionfalse + +\DeclareOption{ND}{\prf@NDOptiontrue} +\DeclareOption{SEQ}{\prf@SEQOptiontrue} +\DeclareOption{IMP}{\prf@IMPOptiontrue} +\ProcessOptions\relax + +%-------------------------------------------------------------------- +% A proof tree is composed by a generic cell: +% A1 A2 A3 +% ---------- R +% C +% We call A1, A2, A3. ... assumptions, C the conclusion and R the rule +% name. The line dividing the assumptions from the conclusion is +% called the proof line. A proof tree with no assumptions is an axiom. +% An assumption which is not a proof tree is a pure assumption. +% +% A proof tree is typeset by +% \prftree[<options>]...[<options>] +% {<assumption1>}...{<assumptionN>} +% {<conclusion>} +% The possible options are: +% r : the first argument after the options is the rule +% name, typeset in text mode +% rule : synonym for 'r' +% by rule : synonym for 'r' +% by : synonym for 'r' +% right : synonym for 'r' +% l : the first argument after the options is the rule +% label, typeset in text mode; if there is also a +% rule name, the label is the second argument +% label : synonym for 'l' +% left : synonym for 'l' +% straight : the proof line will be a solid line (default) +% straight line : synonym for 'l' +% straightline : synonym for 'l' +% dotted : the proof line will be a dotted line +% dotted line : synonym for 'dotted' +% dottedline : synonym for 'dotted' +% dashed : the proof line will be a dashed line +% dashed line : synonym for 'dashed' +% dashedline : synonym for 'dashed' +% f : the proof line will be fancy +% fancy : synonym for 'f' +% fancy line : synonym for 'f' +% fancyline : synonym for 'f' +% s : the proof line will be single, not double (default) +% single : synonym for 's' +% single line : synonym for 's' +% singleline : synonym for 's' +% d : the proof line will be double, not single +% double : synonym for 'd' +% double line : synonym for 'd' +% doubleline : synonym for 'd' +% noline : suppresses the proof line (prevails over all other +% line options) +% summary : renders the proof line as the summary symbol +% (prevails over all other line options except +% noline) +% +% The format of options is [<opt1>,...,<optM>]; it is correct to have +% empty options. Options are parsed left-to-right: in case of +% conflicting options, the latest prevails. +% +% If present, the rule name is typeset in text style, while the +% conclusion and the assumptions are typeset in display math mode. +% The result is a box with the correct height and width, whose +% conclusion is aligned with the current baseline. +% +% Notice that the conclusion must be present, while the assumptions +% may be absent. +% +% If there are no assumptions, i.e., if the proof tree represents an +% axiom, you may use the following commands: +% \prfaxiom{<axiom>} +% \prfbyaxiom{<label>}{<axiom>} +% the latter includes also the axiom name. +% +% A pure assumption is just a proof tree composed by the conclusion +% only. It uses an option to suppress the drawing of the proof line. +% The commands are: +% \prfassumption<reference>{<formula>} +% \prfboundedassumption<reference>{<formula>} +% the second command discharges the assumption. +% +% A proof summary is just a proof tree whose proof line is bizarre. It +% uses an option to specify the type of summary. +% The command is: +% \prfsummary<reference>[<label>] +% {<assumption1>}...{<assumptionN>} +% {<conclusion>} +% The label is optional. The shape of the summary is controlled by the +% global option \prfsummarystyle. +% +% The <reference> field above is used for labelling and +% referencing, as explained in the documentation. +%-------------------------------------------------------------------- + +%-------------------------------------------------------------------- +% Parameters +% These values can be safely used to configure the behaviour of the +% macros in the package. Beware to modify them only outside a proof +% tree as the order in which a proof tree is typeset may vary in +% future version of the package. +%-------------------------------------------------------------------- + +% \prflinepad default 0.3ex +% the space between the baseline of assumptions and the proof line and +% also the space between the proof line and the top of the conclusion +\newdimen\prflinepad\prflinepad.3ex + +% \prflineextra default 0.3em +% the length which extends on the left and on the right the proof line +% so that it is slightly longer than the largest between the +% conclusion and the list of (direct) assumptions +\newdimen\prflineextra\prflineextra.3em + +% \prflinethickness default 0.2pt +% the thickness of the proof line +\newdimen\prflinethickness\prflinethickness.2pt + +% \prfemptylinethickness default 4 times the linethickness +% the thickness of the proof line which has to be drawn but it is empty +\newdimen\prfemptylinethickness\prfemptylinethickness4\prflinethickness + +% \prfrulenameskip default 0.2em +% the space between the proof line and the rule name +\newdimen\prfrulenameskip\prfrulenameskip.2em + +% \prflabelskip default 0.2em +% the space between the label and the proof line +\newdimen\prflabelskip\prflabelskip.2em + +% \prfinterspace default .6em +% the space between two subsequent assumptions +\newdimen\prfinterspace\prfinterspace.6em + +% \prfdoublelineinterspace default 1.2pt +% the space between a double line +\newdimen\prfdoublelineinterspace\prfdoublelineinterspace1.2pt + +% \prfboundedstyle default 0 +% defines the style of bounded (discharged) assumptions: +% 0 = [<formula>] +% 1 = <formula> cancelled by a horizontal line +% >1 = uses the custom \prfdiscargedassumption command +\newcount\prfboundedstyle\prfboundedstyle0 + +% \prfsummarystyle default 0 +% defines the style for the summary box. The argument takes the +% following values +% 0 = a vertical dotted line (default) +% 1 = a huge \Pi +% 2 = \prod +% 3 = a calligraphic D +% >3 = uses the custom \prffancysummarybox command +\newcount\prfsummarystyle\prfsummarystyle0 + +% \prffancyline +% the command to draw "fancy" lines +\def\prffancyline{\cleaders\hbox to .63em% + {\hss\raisebox{-.5ex}[.2ex][0pt]{$\sim$}\hss}\hfill} + +% \prfConclusionBox +% the command to draw the conclusion box +\def\prfConclusionBox#1{% + \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}} + +% \prfAssumptionBox +% the command to draw the assumption box +\def\prfAssumptionBox#1{% + \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}} + +% \prfRuleNameBox +% the command to draw the rule name box. +\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}} + +% \prfLabelBox +% the command to draw the label box. +\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}} + +% \prfdiscargedassumption +% the command to draw a discharged assumption in a custom way. +% Users may consider the cancel.sty package +\def\prfdiscargedassumption#1{\left\langle{#1}\right\rangle} + +% \prffancysummarybox +% the command to draw the body of a custom summary +\newbox\prf@@fancysummarybox +\newdimen\prf@@fancysymmarylen +\def\prffancysummarybox{% + \sbox{\prf@@fancysummarybox}{\Huge$\bigtriangledown$}% + \prf@@fancysymmarylen\ht\prf@@fancysummarybox% + \advance\prf@@fancysymmarylen\dp\prf@@fancysummarybox% + \sbox{\prf@@fancysummarybox}{% + \raisebox{.25\prf@@fancysymmarylen}[.8\prf@@fancysymmarylen]% + [0pt]{\usebox{\prf@@fancysummarybox}}}% + \prf@@fancysymmarylen\wd\prf@summary@label% + \ifdim\prf@@fancysymmarylen>\z@\relax% + \prf@@fancysymmarylen\wd\prf@@fancysummarybox% + \wd\prf@summary@label.4em% + \hbox to\prf@@fancysymmarylen{% + \usebox\prf@@fancysummarybox}\kern-.4em% + \box\prf@summary@label% + \else\usebox\prf@@fancysummarybox\fi} + +%==================================================================== + +%-------------------------------------------------------------------- +% What follows is intended for internal use of the package. +% It shouldn't be used in documents and may vary in future versions. +% +% Notice that we use temporary registers shared with TeX & LaTeX, and +% that some registers are shared also inside the drawing procedure! +%-------------------------------------------------------------------- + +% Lengths +\newskip\prf@Lassum% space between the left border of the + % assumption box and the left border of the + % conclusion of the first assumption; +\newskip\prf@Rassum% space between the right border of the + % assumption box and the right border of the + % conclusion of the last assumption +\skipdef\prf@assumline1% +\skipdef\prf@concline3% +\skipdef\prf@linewd5% +\skipdef\prf@lineht3% +\skipdef\prf@linedp1% +\skipdef\prf@temp7% +\skipdef\prf@tmp7% +\skipdef\prf@Aval9% + +% Boxes +\newbox\prf@assumptionsbox% Assumptions +\newbox\prf@conclusionbox% Conclusion +\newbox\prf@rulenamebox% Rule name +\newbox\prf@labelbox% Label +\newbox\prf@linebox% Proof line +\newbox\prf@summarybox% Summary +\newbox\prf@fancybox% To compute the fancy line + +%-------------------------------------------------------------------- +% Stack implementation +%-------------------------------------------------------------------- +%% End-of-stack, wrapper and stack declaration +\def\prf@eos{\noexpand\prf@eos} +\def\prf@cons{\noexpand\prf@cons} +\let\prf@stack\prf@eos + +%% Pushing a value puts the (decorated) value in front +%% of the stack list +\def\prf@push#1{\expandafter\edef\expandafter\prf@stack% + {\prf@cons{#1}\prf@stack}} + +%% Top retrieves the topmost value in the stack +\def\prf@@top\prf@cons#1#2\prf@eos{#1} +\def\prf@top{\expandafter\prf@@top\prf@stack} + +%% Pop discard the topmost value in the stack +\def\prf@@pop\prf@cons#1#2\prf@eos{% + \expandafter\edef\expandafter\prf@stack{#2\prf@eos}} +\def\prf@pop{\expandafter\prf@@pop\prf@stack} + +%-------------------------------------------------------------------- +% Checks whether two strings are equal +% \prf@streq{A}{B} if A = B then the boolean value \ifprf@same is +% true otherwise false +% +% There is also \prf@strlisteq{A}{L} which checks whether A is equal +% to any element in the comma-separated list L of strings +%-------------------------------------------------------------------- +\newif\ifprf@same + +\newcommand{\prf@streq}[2]{% + \global\prf@samefalse\begingroup\def\1{#1}\def\2{#2}% + \ifx\1\2\global\prf@sametrue\fi\endgroup} + +\def\prf@strlisteq#1#2{\prf@@strlisteq{#1}#2,@} +\def\prf@@strlisteq#1#2,{\prf@streq{#1}{#2}% + \ifprf@same\expandafter\prf@@strlistignore% + \else\expandafter\prf@@@strlisteq\fi{#1}} +\def\prf@@strlistignore#1@{\relax} +\def\prf@@@strlisteq#1#2{% + \begingroup\def\1{@}\def\2{#2}% + \ifx\1\2\prf@@@strlistignore\else\prf@hop\fi\endgroup{#1}#2} +\def\prf@hop\fi\endgroup#1#2{\fi\endgroup\prf@@strlisteq{#1}#2} +\def\prf@@@strlistignore\else\prf@hop\fi\endgroup#1@{\fi\endgroup} + +% ------------------------------------------------------------------- +% Labelling and referencing +% The following commands implement the reference mechanism to allow to +% label and then refer to assumptions and summaries of proofs +% ------------------------------------------------------------------- + +% The counter to keep track of assumptions +\newcounter{prfassumptioncounter} +\setcounter{prfassumptioncounter}{0} + +% The counter to keep track of summaries +\newcounter{prfsummarycounter} +\setcounter{prfsummarycounter}{0} + +% To keep track of the options +\newif\ifprf@lbl@arabic\prf@lbl@arabictrue +\newif\ifprf@lbl@roman\prf@lbl@romanfalse +\newif\ifprf@lbl@Roman\prf@lbl@Romanfalse +\newif\ifprf@lbl@alph\prf@lbl@alphfalse +\newif\ifprf@lbl@Alph\prf@lbl@Alphfalse +\newif\ifprf@lbl@fnsymbol\prf@lbl@fnsymbolfalse +\newif\ifprf@lbl@label\prf@lbl@labelfalse + +% The prooftree environment is used to define the scope of the +% assumption references +\newenvironment{prooftree}% + {\setcounter{prfassumptioncounter}{0}}% + {\setcounter{prfassumptioncounter}{0}} + +% Test whether a reference is defined +\def\ifprf@undefref<#1>{% + \expandafter\ifx\csname prf@ref@@#1\endcsname\relax} + +% Test whether a reference has been written in the .aux file +\def\ifprf@unwrittenref<#1>{% + \expandafter\ifx\csname prf@w@ref@#1\endcsname\relax} + +% Write a reference +\def\prfref<#1>{% + \ifprf@undefref<#1>{??}% + \PackageWarningNoLine{prooftree}{Undefined reference <#1>}% + \else\csname prf@ref@@#1\endcsname\relax\fi} + +% Create the anchor from what stored in the .aux file +\def\prfauxlabel#1#2{% + \ifprf@undefref<#1>% + \expandafter\gdef\csname prf@ref@@#1\endcsname{{#2}}\fi} + +% Write the newly created label in the .aux file +\def\prf@auxwrite<#1>#2{% + \ifprf@unwrittenref<#1>% + \protected@write\@auxout{}{\string\prfauxlabel{#1}{#2}}% + \expandafter\gdef\csname prf@w@ref@#1\endcsname{0}\fi} + +% Generate an assumption label +\def\prf@assum@lbl<#1>{\prf@generic@lbl<#1>{prfassumptioncounter}} + +% Generate a summary label +\def\prf@summary@lbl<#1>{\prf@generic@lbl<#1>{prfsummarycounter}} + +% Generate a label on a given counter +\def\prf@generic@lbl<#1>#2{% + \prf@warningtrue\stepcounter{#2}% + \ifprf@lbl@arabic\prf@warningfalse% + \prf@auxwrite<#1>{\arabic{#2}}\fi% + \ifprf@lbl@roman\prf@warningfalse% + \prf@auxwrite<#1>{\roman{#2}}\fi% + \ifprf@lbl@Roman\prf@warningfalse% + \prf@auxwrite<#1>{\Roman{#2}}\fi% + \ifprf@lbl@alph\prf@warningfalse% + \prf@auxwrite<#1>{\alph{#2}}\fi% + \ifprf@lbl@Alph\prf@warningfalse% + \prf@auxwrite<#1>{\Alph{#2}}\fi% + \ifprf@lbl@fnsymbol\prf@warningfalse% + \prf@auxwrite<#1>{\fnsymbol{#2}}\fi% + \ifprf@warning\prf@auxwrite<#1>{\arabic{#2}}\fi} + +% Parsing of the labelled assumption options +\def\prf@lblopt#1{% + \prf@warningtrue% + \global\prf@lbl@arabicfalse% + \global\prf@lbl@romanfalse% + \global\prf@lbl@Romanfalse% + \global\prf@lbl@alphfalse% + \global\prf@lbl@Alphfalse% + \global\prf@lbl@fnsymbolfalse% + \global\prf@lbl@labelfalse% + \prf@strlisteq{#1}{n,number,arabic}% + \ifprf@same\prf@warningfalse\global\prf@lbl@arabictrue\fi% + \prf@strlisteq{#1}{r,roman}% + \ifprf@same\prf@warningfalse\global\prf@lbl@romantrue\fi% + \prf@strlisteq{#1}{R,Roman}% + \ifprf@same\prf@warningfalse\global\prf@lbl@Romantrue\fi% + \prf@strlisteq{#1}{a,alph,alpha,alphabetic}% + \ifprf@same\prf@warningfalse\global\prf@lbl@alphtrue\fi% + \prf@strlisteq{#1}{A,Alph,Alpha,Alphabetic}% + \ifprf@same\prf@warningfalse\global\prf@lbl@Alphtrue\fi + \prf@strlisteq{#1}{f,s,function,symbol,function symbol}% + \ifprf@same\prf@warningfalse\global\prf@lbl@fnsymboltrue\fi% + \prf@strlisteq{#1}{l,label}% + \ifprf@same\prf@warningfalse\global\prf@lbl@labeltrue\fi% + \ifprf@warning% + \PackageWarning{prftree}{Unrecognised option #1}\fi} + +% How a labelled assumption is graphically rendered +\def\prflabelledassumptionbox#1#2{% + \setbox\prf@fancybox\hbox{${#1}$}% + \prf@tmp\wd\prf@fancybox% + \setbox\prf@fancybox\hbox{$\box\prf@fancybox^{#2}$}% + \wd\prf@fancybox\prf@tmp% + \prf@assumption{\box\prf@fancybox}} + +% How a discharged fancy labelled assumption is graphically rendered +\def\prflabelleddiscargedassumption#1#2{% + \prflabelledassumptionbox{\left\langle{#1}\right\rangle}{#2}} + +%-------------------------------------------------------------------- +% \prfassumption{<formula>} +% \prfboundedassumption{<formula>} +% +% Commands to draw a pure assumption: the former draws a pure +% assumption, while the latter draws a pure assumption which is +% discharged. The way to mark discharging is controlled by the global +% option \prfboundedstyle +%-------------------------------------------------------------------- +\def\prfassumption{\@ifnextchar<{\prf@assum@one}{\prf@assumption}} +\def\prf@assum@one<#1>{\global\prf@lbl@labelfalse\prf@assum@two#1>} +\def\prf@assum@two{\@ifnextchar[{\prf@assum@three}{\prf@assum@four}} +\def\prf@assum@three[#1]{\prf@lblopt{#1}\prf@assum@four} +\def\prf@assum@four#1>#2{% + \ifprf@unwrittenref<#1>\relax% + \else\ifprf@lbl@label\relax\else% + \global\prf@lbl@labeltrue% + \PackageWarningNoLine{prftree}{Label <#1> is [label]!}\fi\fi% + \ifprf@lbl@label\relax\else\prf@assum@lbl<#1>\fi% + \prflabelledassumptionbox{#2}{\prfref<#1>}} +\def\prf@assumption#1{\prftree[noline]{#1}\relax} + +\def\prfboundedassumption{% + \@ifnextchar<{\prf@bassum@one}{\prf@boundedassumption}} +\def\prf@bassum@one<#1>{\global\prf@lbl@labelfalse\prf@bassum@two#1>} +\def\prf@bassum@two{\@ifnextchar[{\prf@bassum@three}{\prf@bassum@four}} +\def\prf@bassum@three[#1]{\prf@lblopt{#1}\prf@bassum@four} +\def\prf@bassum@four#1>#2{% + \ifprf@unwrittenref<#1>\relax% + \else\ifprf@lbl@label\relax\else% + \global\prf@lbl@labeltrue% + \PackageWarningNoLine{prftree}{Label <#1> is [label]!}\fi\fi% + \ifprf@lbl@label\relax\else\prf@assum@lbl<#1>\fi% + \prftree[noline]{\prf@labelledbounded{#2}{#1}}\relax} +\def\prf@boundedassumption#1{\prftree[noline]{\prf@bounded{#1}}\relax} +\def\prf@bounded#1{% + \ifnum\prfboundedstyle=0\left[{#1}\right]% + \else\ifnum\prfboundedstyle=1% + \setbox\prf@conclusionbox\prfConclusionBox{#1}% + \prf@tmp\wd\prf@conclusionbox% + \prf@linedp.5\ht\prf@conclusionbox% + \advance\prf@linedp-.5\dp\prf@conclusionbox% + \prf@lineht\prf@linedp\advance\prf@lineht\prflinethickness% + \edef\prf@cancel{\hskip-\prf@tmp% + \vrule width\prf@tmp height\prf@lineht depth-\prf@linedp}% + {#1}\prf@cancel% + \else\prfdiscargedassumption{#1}\fi\fi} +\def\prf@labelledbounded#1#2{% + \ifnum\prfboundedstyle=0% + \prflabelledassumptionbox{\left[{#1}\right]}{\prfref<#2>}% + \else\ifnum\prfboundedstyle=1% + \setbox\prf@conclusionbox\prfConclusionBox{#1}% + \prf@tmp\wd\prf@conclusionbox% + \prf@linedp.5\ht\prf@conclusionbox% + \advance\prf@linedp-.5\dp\prf@conclusionbox% + \prf@lineht\prf@linedp\advance\prf@lineht\prflinethickness% + \edef\prf@cancel{\hskip-\prf@tmp% + \vrule width\prf@tmp height\prf@lineht depth-\prf@linedp}% + \prflabelledassumptionbox{{#1}\prf@cancel}{\prfref<#2>}% + \else\prflabelleddiscargedassumption{#1}{\prfref<#2>}\fi\fi} + +%-------------------------------------------------------------------- +% \prfaxiom{<axiom>} +% \prfbyaxiom{<label>}{<axiom>} +% +% Commands to draw an axiom: the former draws the axiom, while the +% latter includes also a rule name for the axiom. +%-------------------------------------------------------------------- +\def\prfaxiom#1{\prftree[single,straight]{#1}\relax} +\def\prfbyaxiom#1#2{\prftree[single,straight,rule]{#1}{#2}\relax} + +%-------------------------------------------------------------------- +% \prfsummary[<label>] +% {<assumption1>}...{<assumptionN>} +% {<conclusion>} +% +% Command to draw a proof summary, i.e., a structure with assumptions +% 1 to N and a conclusion which stands for a complex proof not +% explicited. The label is optional. +% The shape of the summary is controlled by the global option +% \prfsummarystyle +%-------------------------------------------------------------------- +\def\prfsummary{\@ifnextchar<{\prf@summary@one}{\prf@summary}} +\def\prf@summary@one<#1>{% + \global\prf@lbl@labelfalse\prf@summary@four#1>} +\def\prf@summary@four{% + \@ifnextchar[{\prf@summary@five}{\prf@summary@six}} +\def\prf@summary@five[#1]#2>{% + \prf@lblopt{#1}% + \ifprf@unwrittenref<#2>\relax% + \else\ifprf@lbl@label\relax\else% + \global\prf@lbl@labeltrue% + \PackageWarningNoLine{prftree}{Label <#2> is [label]!}\fi\fi% + \ifprf@lbl@label\relax\else\prf@summary@lbl<#2>\fi% + \setbox\prf@summary@label\hbox{\scriptsize\prfref<#2>}% + \prf@summary} +\def\prf@summary@six#1>{% + \ifprf@lbl@label\relax\else\prf@summary@lbl<#1>\fi% + \setbox\prf@summary@label\hbox{\scriptsize\prfref<#1>}% + \prf@summary} +\def\prf@summary{\@ifnextchar[{\prf@summary@two}{\prf@summary@three}} +\def\prf@summary@two[#1]{\prftree[summary,rule]{#1}} +\def\prf@summary@three{\prftree[summary]} + +\newbox\prf@summary@label +\def\prf@@summarystyle{% + \ifnum3=\prfsummarystyle\relax% + \setbox\prf@summarybox\hbox{$\mathcal{D}$}% + \prf@tmp\wd\prf@summarybox% + \setbox\prf@summarybox\hbox{$\mathcal{D}% + \hbox{\box\prf@summary@label}\mathstrut$}% + \wd\prf@summarybox\prf@tmp% + \else\ifnum2=\prfsummarystyle\relax% + \setbox\prf@summarybox\hbox{$\prod$}% + \prf@tmp\wd\prf@summarybox% + \setbox\prf@summarybox\hbox{$\prod\hbox{\box\prf@summary@label}$}% + \wd\prf@summarybox\prf@tmp% + \else\ifnum1=\prfsummarystyle\relax% + \setbox\prf@summarybox\hbox{\hbox{\Huge$\Pi$}}% + \prf@tmp\wd\prf@summarybox% + \setbox\prf@summarybox\hbox{\hbox{\Huge$\Pi$}% + \hbox{\box\prf@summary@label}}% + \wd\prf@summarybox\prf@tmp% + \else\ifnum0=\prfsummarystyle\relax% + \setbox\prf@summarybox\hbox{$\cdot$}% + \prf@tmp\wd\prf@summarybox% + \setbox\prf@summarybox% + \vbox to5.2ex{\cleaders\hbox{$\cdot$}\vfill}% + \setbox\prf@summarybox\hbox{\usebox{\prf@summarybox}% + \hbox{\ \box\prf@summary@label}}% + \wd\prf@summarybox\prf@tmp% + \else\setbox\prf@summarybox\hbox{\prffancysummarybox}\fi\fi\fi\fi% + \prf@tmp.5\ht\prf@summarybox% + \advance\prf@tmp-.5\dp\prf@summarybox% + \setbox\prf@summarybox% + \hbox{\lower\prf@tmp\hbox{\box\prf@summarybox}}}% + +%-------------------------------------------------------------------- +% \prftree[<options>]...[<options>] +% {<assumption1>}...{<assumptionN>} +% {<conclusion>} +% +% The format of options is [<opt1>,...,<optM>]; it is correct to have +% empty options. Options are parsed left-to-right: in case of +% conflicting options, the latest prevails. See the documentation for +% their description. +% +% If present, the rule name is typesetted in text style, while the +% conclusion and the assumptions are typesetted in math mode. +% The result is a box with the correct height and width, whose +% conclusion is aligned with the current baseline. +% +% Notice that the conclusion must be present, while the assumptions +% may be absent. +% +% Options and the way things are drawn can be modified via the global +% settings of the package (see above). Notice that changing these +% settings inside a proof tree may lead to impredictable results, as +% the typesetting may proceed in an arbitrary order. +%-------------------------------------------------------------------- +\newif\ifprf@rule% +\newif\ifprf@label% +\newif\ifprf@noline% +\newif\ifprf@doubleline% +\newif\ifprf@straightline% +\newif\ifprf@dottedline% +\newif\ifprf@dashedline% +\newif\ifprf@fancyline% +\newif\ifprf@summary% +\newif\ifprf@first% +\newif\ifprf@warning% +\newif\ifprf@assum + +% The real parsing command is \prf@Ntree; the external command sets +% the right values for the various switches controlling the options +\def\prftree{\prf@init\prf@Ntree} +\def\prf@init{% + \global\prf@rulefalse% + \global\prf@labelfalse% + \global\prf@nolinefalse% + \global\prf@doublelinefalse% + \global\prf@straightlinetrue% + \global\prf@dottedlinefalse% + \global\prf@dashedlinefalse% + \global\prf@fancylinefalse% + \global\prf@summaryfalse} + +% If there are options then parse them, eventually setting the +% booleans to their appropriate values. Then, expand \prf@@tree +\def\prf@Ntree{\@ifnextchar[{\prf@options}{\prf@@tree}} + +% Parses a block [<opt>,...,<opt>] of options one by one, left to +% right +\def\prf@options[#1]{\prf@opts#1,]\prf@Ntree} +\def\prf@opts#1,{\prf@opt#1,\@ifnextchar]{\prf@optsskip}{\prf@opts}} +\def\prf@optsskip]{\relax} % to consume the final ] + +% Parses a single option eventually setting the appropriate flag +\def\prf@opt#1,{\prf@warningtrue% + \prf@strlisteq{#1}{r,by rule,rule,by,right}% + \ifprf@same\prf@warningfalse\global\prf@ruletrue\fi% + \prf@strlisteq{#1}{l,label,left}% + \ifprf@same\prf@warningfalse\global\prf@labeltrue\fi% + \prf@strlisteq{#1}{s,single line,single,singleline}% + \ifprf@same\prf@warningfalse\global\prf@doublelinefalse\fi% + \prf@strlisteq{#1}{d,double line,double,doubleline}% + \ifprf@same\prf@warningfalse\global\prf@doublelinetrue\fi% + \prf@strlisteq{#1}{straight,straight line,straightline}% + \ifprf@same\prf@warningfalse% + \global\prf@straightlinetrue\global\prf@dottedlinefalse% + \global\prf@dashedlinefalse\global\prf@fancylinefalse\fi% + \prf@strlisteq{#1}{dotted,dotted line,dottedline}% + \ifprf@same\prf@warningfalse% + \global\prf@straightlinefalse\global\prf@dottedlinetrue% + \global\prf@dashedlinefalse\global\prf@fancylinefalse\fi% + \prf@strlisteq{#1}{dashed,dashed line,dashedline}% + \ifprf@same\prf@warningfalse% + \global\prf@straightlinefalse\global\prf@dottedlinefalse% + \global\prf@dashedlinetrue\global\prf@fancylinefalse\fi% + \prf@strlisteq{#1}{f,fancy line,fancy,fancyline}% + \ifprf@same\prf@warningfalse% + \global\prf@straightlinefalse\global\prf@dottedlinefalse% + \global\prf@dashedlinefalse\global\prf@fancylinetrue\fi% + \prf@strlisteq{#1}{noline}% + \ifprf@same\prf@warningfalse\global\prf@nolinetrue\fi% + \prf@strlisteq{#1}{summary}% + \ifprf@same\prf@warningfalse\global\prf@summarytrue\fi% + \ifprf@warning\PackageWarning{prftree}% + {Unrecognised option #1}\fi}% + +% At this point, options have been parsed. So, we process them +% preparing the right parameters for the drawing procedure. +% We start from the proof line options: +% 0 = single straight line +% 1 = double straight line +% 2 = single dotted line +% 3 = double dotted line +% 4 = single dashed line +% 5 = double dashed line +% 6 = single fancy line +% 7 = double fancy line +% 8 = no line +% 9 = summary +\def\prf@@tree{% + \countdef\prf@linetype1\prf@linetype0% + \ifprf@dottedline\prf@linetype2\fi% + \ifprf@dashedline\prf@linetype4\fi% + \ifprf@fancyline\prf@linetype6\fi% + \ifprf@doubleline\advance\prf@linetype1\fi% + \ifprf@noline\prf@linetype8\fi% + \ifprf@summary\prf@linetype9\fi\relax% + \expandafter\prf@@Ntree\the\prf@linetype} + +% If there is no rule name, we put an empty one in place +% #1 the line options +\def\prf@@Ntree#1{% + \edef\prf@choice{\ifprf@rule{#1}\else{#1}{}\fi}% + \expandafter\prf@@NNtree\prf@choice} + +% If there is no label, we put an empty one in place +% #1 the line options +% #2 the rule name +\def\prf@@NNtree#1#2{% + \edef\prf@choice{\ifprf@label{#1}{#2}\else{#1}{#2}{}\fi}% + \expandafter\prf@tree\prf@choice} + +% We collect the first assumption, if any, or the conclusion otherwise +% and we look if there is another argument. If not, we draw the proof. +% #1 the line options' value +% #2 the rule name +% #3 the label +% #4 the conclusion or the first assumption +\def\prf@tree#1#2#3#4{\@ifnextchar\bgroup% + {\prf@assumptions{#1}{#2}{#3}{\prf@preprf{#4}}}% + {\prf@draw{#1}{#2}{#3}{#4}{\prf@preprf}{}}} + +% We examine assumptions from left to right. If we hit the last +% argument, it is the conclusion and the proof is ready to be drawn. +% #1 the line options' value +% #2 the rule name +% #3 the label +% #4 the first assumptions +% #5 the current argument +\def\prf@assumptions#1#2#3#4#5{\@ifnextchar\bgroup% + {\prf@assumenext{#1}{#2}{#3}{#4}{\prf@interprf{#5}}}% + {\prf@draw{#1}{#2}{#3}{#5}{#4}{}}} + +% An intermediate assumption is added to the assumptions' box, until +% the last assumption has been collected. Then the proof is drawn. +% #1 the line options' value +% #2 the rule name +% #3 the label +% #4 the first assumption +% #5 the complete list of assumptions +% #6 the new argument +\def\prf@assumenext#1#2#3#4#5#6{\@ifnextchar\bgroup% + {\prf@assumenext{#1}{#2}{#3}{#4}{{#5}\prf@interprf{#6}}}% + {\prf@draw{#1}{#2}{#3}{#6}{#4}{#5}}} + +% We need to reset some internal variables during the generation of +% the assumptions +\def\prf@preprf{\global\prf@Lassum\z@\global\prf@Rassum\z@} + +% We need to put some space between assumptions when generating them +\def\prf@interprf{\hskip\prfinterspace} + +%-------------------------------------------------------------------- +% The drawing procedure, i.e., the "core" of the package +% #1 the line options' value +% #2 the rule name +% #3 the label +% #4 the conclusion +% #5 the first assumption +% #6 the list of assumptions +%-------------------------------------------------------------------- + +\def\prf@draw#1#2#3#4#5#6{% + % We construct the boxes which will constitute the proof + \ifprf@first\prf@push{1}\else\prf@push{0}\fi% + \global\prf@firsttrue% + \setbox\prf@assumptionsbox\prfAssumptionBox{#5}% + \prf@push{\the\prf@Lassum}% + \global\prf@firstfalse% + \ifdim\wd\prf@assumptionsbox>\z@\relax\prf@assumtrue% + \setbox\prf@assumptionsbox% + \hbox{\box\prf@assumptionsbox\prfAssumptionBox{#6}}% + \else\prf@assumfalse% + \setbox\prf@assumptionsbox\hbox{}\fi% + \prf@push{\the\prf@Rassum}% + \setbox\prf@conclusionbox\prfConclusionBox{#4}% + \setbox\prf@rulenamebox\prfRuleNameBox{#2}% + \setbox\prf@labelbox\prfLabelBox{#3}% + % We set up the flags needed to format the proof tree box + \prf@nolinefalse\prf@doublelinefalse\prf@straightlinetrue% + \prf@dottedlinefalse\prf@dashedlinefalse\prf@fancylinefalse% + \prf@summaryfalse\prf@rulefalse\prf@labelfalse% + \ifcase#1\relax\or% + \prf@doublelinetrue\or% + \prf@dottedlinetrue\prf@straightlinefalse\or% + \prf@doublelinetrue\prf@dottedlinetrue\prf@straightlinefalse\or% + \prf@dashedlinetrue\prf@straightlinefalse\or% + \prf@doublelinetrue\prf@dashedlinetrue\prf@straightlinefalse\or% + \prf@fancylinetrue\prf@straightlinefalse\or% + \prf@doublelinetrue\prf@fancylinetrue\prf@straightlinefalse\or% + \prf@nolinetrue\prf@straightlinefalse\or% + \prf@summarytrue\prf@straightlinefalse\fi% + \ifdim\wd\prf@rulenamebox>\z@\relax\prf@ruletrue% + \else\prf@rulefalse\fi% + \ifdim\wd\prf@labelbox>\z@\relax\prf@labeltrue% + \else\prf@labelfalse\fi% + \ifdim\wd\prf@assumptionsbox>\z@\relax\prf@assumtrue% + \else\prf@assumfalse\fi% + % Now, we retrieve the right values for Lassum and Rassum + % since box construction may have overwritten them. Also, we need to + % know if this proof is the first of a list of assumptions + \edef\prf@tok{\prf@top}\prf@pop\global\prf@Rassum\prf@tok% + \edef\prf@tok{\prf@top}\prf@pop\global\prf@Lassum\prf@tok% + \edef\prf@tok{\prf@top}\prf@pop\global\prf@firstfalse% + \ifnum\prf@tok=1\global\prf@firsttrue\fi% + % The assumptions' box has the following shape + % -------------------------------- + % |<---------------------wd------->| + % | ----------- ------------ | + % ||<--> | | <---->|| + % || Lassum | ... | Rassum || + % || | | | | || + % || V | | V || + % | ----------- ------------ | + % -------------------------------- + % The assumptions' line is composed by the conclusions of the + % proofs which are the antecedents of the application of the + % inference rule + % The final box will be something like + % -------------------------------- + % |<---------------------wd------->| + % | ----------- ------------ | + % ||<--> | | <---->|| + % || Lassum | ... | Rassum || + % || | | | | || + % || V | | V || + % | ----------- ------------ | + % -------------------------------- + % ======================== rule name + % conclusion + % <--Lassum--> <-----Rassum-----> + % + % We calculate the length of the assumptions' line: + % assumline = assumptionsbox - Lassum - Rassum + % if there are no assumption, assumline = 0 + % (for efficiency reasons, we actually calculate 1/2assumline) + \ifprf@assum\prf@assumline.5\wd\prf@assumptionsbox% + \advance\prf@assumline-.5\prf@Lassum% + \advance\prf@assumline-.5\prf@Rassum% + \else\prf@assumline\z@\fi% + % The length of the conclusionbox + % (for efficiency reasons, we actually calculate 1/2concline) + \prf@concline.5\wd\prf@conclusionbox% + % The length of the proof line is + % linewd = if summary then width of summary box else + % max(concline,assumline) + % if there is a line, we add 2extra + % (for efficiency reasons, we actually calculate 1/2linewd) + \ifprf@summary\prf@@summarystyle\prf@linewd.5\wd\prf@summarybox% + \else\prf@linewd\prf@assumline% + \ifdim\prf@assumline<\prf@concline\prf@linewd\prf@concline\fi% + \ifprf@noline\relax\else\advance\prf@linewd\prflineextra\fi\fi% + % We calculate the proofline without label and rule name. + \ifprf@noline\setbox\prf@fancybox\hbox{\hskip2\prf@linewd}% + \else\ifprf@summary\setbox\prf@fancybox\copy\prf@summarybox% + \else\ifprf@fancyline% + \setbox\prf@fancybox\hbox to2\prf@linewd{\prffancyline}\else% + \ifprf@dashedline% + \setbox\prf@fancybox% + \hbox to2\prf@linewd{\cleaders\hbox to.5em{\hss\_\hss}\hfill}\else% + \ifprf@dottedline% + \setbox\prf@fancybox% + \hbox to2\prf@linewd{\cleaders\hbox to.33em{\hss.\hss}\hfill}\else% + % it must be a straight line! + \setbox\prf@fancybox\hbox{\vrule width2\prf@linewd% + height\prflinethickness}\fi\fi\fi% + % If the line is double, we draw it twice with enough + % (doublelineinterspace) space between the two copies. + \ifprf@doubleline% + \setbox\prf@fancybox\hbox{\vbox{\copy\prf@fancybox% + \nointerlineskip\vskip\prfdoublelineinterspace\nointerlineskip% + \box\prf@fancybox}}\fi\fi\fi% + \prf@tmp\dp\prf@fancybox% + \setbox\prf@fancybox\hbox{\raise\prf@tmp\box\prf@fancybox}% + % Let A = max(1/2assumline + Lassum, 1/2conclusionbox, 1/2linewd + + % delta), where delta is 0 if there is no label, and it is the width + % of the label box plus prflabelskip otherwise. + % Then + % Assumptions shift = A - (1/2assumline + Lassum) + % Rule line shift = A - (1/2linewd + delta) + % Lassum = Conclusion shift = A - 1/2conclusionbox + % And, so, we can prepare the assumptions box and the conclusion box + \prf@Aval\prf@assumline\advance\prf@Aval\prf@Lassum% + \prf@tmp\prf@linewd\relax% + \ifprf@label\advance\prf@tmp\wd\prf@labelbox% + \advance\prf@tmp\prflabelskip\fi% + \ifdim\prf@Aval<\prf@tmp\prf@Aval\prf@tmp\fi% + \ifdim\prf@Aval<\prf@concline\prf@Aval\prf@concline\fi% + \prf@temp\prf@Aval\advance\prf@temp-\prf@assumline% + \advance\prf@temp-\prf@Lassum% + \setbox\prf@assumptionsbox% + \hbox{\hskip\prf@temp\box\prf@assumptionsbox}% + \prf@temp\prf@Aval\advance\prf@temp-\prf@concline% + \setbox\prf@conclusionbox% + \hbox{\hskip\prf@temp\box\prf@conclusionbox}% + \global\prf@Lassum\prf@temp% + % Rassum will be the width of the composition of all boxes (but we + % still have to cope with heigths...) minus (concline + conclusion + % shift) + \global\prf@Rassum-2\prf@concline% + \global\advance\prf@Rassum-\prf@temp% + % Then, if there is a rule name, the line is raised to align with + % the centre of the rule name and the rule box gets attached to the + % proof line box. + \prf@linedp\z@% + \ifprf@noline\setbox\prf@fancybox\hbox to2\prf@linewd{}\fi% + \ifprf@rule\advance\prf@linedp.5\ht\prf@fancybox% + \advance\prf@linedp-.5\ht\prf@rulenamebox% + \advance\prf@linedp.5\dp\prf@rulenamebox% + \setbox\prf@linebox% + \hbox{\copy\prf@fancybox\hskip\prfrulenameskip% + \raise\prf@linedp\box\prf@rulenamebox}% + \else\setbox\prf@linebox\copy\prf@fancybox\fi% + \setbox\prf@linebox\hbox{\raise\dp\prf@linebox\box\prf@linebox}% + % Then, if there is a label, the line is raised to align with + % the centre of the label and the label box gets attached to the + % proof line box. + \prf@linedp\z@% + \prf@temp\prf@Aval\advance\prf@temp-\prf@linewd% + \ifprf@label\advance\prf@linedp.5\ht\prf@linebox% + \advance\prf@linedp-.5\ht\prf@labelbox% + \advance\prf@linedp.5\dp\prf@labelbox% + \advance\prf@temp-\prflabelskip% + \advance\prf@temp-\wd\prf@labelbox% + \setbox\prf@linebox% + \hbox{\raise\prf@linedp\box\prf@labelbox% + \hskip\prflabelskip\box\prf@linebox}\fi% + \setbox\prf@linebox% + \hbox{\hskip\prf@temp\raise\dp\prf@linebox\box\prf@linebox}% + % We need to calculate the distance between the assumptions and the + % proofline: if there are no assumptions, it is zero; if there are + % assumptions but no rule name, it is \prflinepad; otherwise it is + % \linepad plus half of the "real" line's height + \prf@tmp\z@% + \ifprf@assum% + \ifprf@rule\prf@tmp-.5\ht\prf@linebox% + \advance\prf@tmp.5\ht\prf@fancybox% + \advance\prf@tmp.5\dp\prf@fancybox\fi\relax% + \ifprf@label\ifprf@rule\relax\else% + \prf@tmp-.5\ht\prf@linebox% + \advance\prf@tmp.5\ht\prf@fancybox% + \advance\prf@tmp.5\dp\prf@fancybox\fi\fi% + \advance\prf@tmp\prflinepad% + \setbox\prf@assumptionsbox% + \vbox{\box\prf@assumptionsbox\nointerlineskip\vskip\prf@tmp}\fi% + % We need to calculate the distance between the proofline and the + % conclusion: it is slightly complex to explain... try to draw the + % whole thing to make it clear!! + \prf@temp\prflinepad% + \ifprf@noline% + \ifprf@assum% + \advance\prf@temp\prfemptylinethickness\fi% + \advance\prf@temp-\prflinepad\fi% + \ifprf@rule% + \advance\prf@temp-.5\ht\prf@linebox% + \advance\prf@temp.5\ht\prf@fancybox% + \advance\prf@temp.5\dp\prf@fancybox\fi% + \ifprf@label\ifprf@rule\relax\else% + \advance\prf@temp-.5\ht\prf@linebox% + \advance\prf@temp.5\ht\prf@fancybox% + \advance\prf@temp.5\dp\prf@fancybox\fi\fi% + \setbox\prf@conclusionbox% + \vbox{\vskip\prf@temp\box\prf@conclusionbox}% + % And, finally, at the very end, we can prepare the proof box and we + % can calculate the right value from Rassum. At the very end, we can + % output the result (!!) + \setbox\prf@rulenamebox% + \vbox{\box\prf@assumptionsbox\nointerlineskip% + \box\prf@linebox\nointerlineskip% + \box\prf@conclusionbox\nointerlineskip}% + \global\advance\prf@Rassum\wd\prf@rulenamebox% + \hbox{$\box\prf@rulenamebox$}} + +% ------------------------------------------------------------------- +% The following macros are used to simplify the writing of proofs in +% natural deduction, and they roughly follow the format of proofs as +% in Troelstra, Schwichtenberg "Basic Proof Theory". +% +% Since they may conflict with other packages, they are controlled by +% options in the package. +% ------------------------------------------------------------------- + +% ------------------------------------------------------------------- +% Natural deduction systems +% +% Package option [ND] +% ------------------------------------------------------------------- + +\newbox\prf@charbox +\def\prfscript#1{\setbox\prf@charbox% + \hbox{$\scriptstyle\mathrm{#1}$}\copy\prf@charbox} +\ifprf@NDOption% + \def\NDA{\prfassumption} + \def\NDD{\prfboundedassumption} + \def\NDAL#1{\prfassumption<#1>} + \def\NDDL#1{\prfboundedassumption<#1>} + \def\NDP{\prftree} + \def\NDANDI{\prftree[by]{$\scriptstyle\wedge\prfscript{I}$}} + \def\NDANDER{\prftree[by]{% + $\scriptstyle\wedge\prfscript{E}_{\prfscript{R}}$}} + \def\NDANDEL{\prftree[by]{% + $\scriptstyle\wedge\prfscript{E}_{\prfscript{L}}$}} + \def\NDANDE{\prftree[by]{$\scriptstyle\wedge\prfscript{E}$}} + \ifprfIMPOption + \def\NDIMPI{\prftree[by]{$\scriptstyle\supset\prfscript{I}$}} + \def\NDIMPE{\prftree[by]{$\scriptstyle\supset\prfscript{E}$}} + \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\supset% + \prfscript{I}_{\prfref<#1>}$}} + \else + \def\NDIMPI{\prftree[by]{$\scriptstyle\rightarrow% + \prfscript{I}$}} + \def\NDIMPE{\prftree[by]{$\scriptstyle\rightarrow% + \prfscript{E}$}} + \def\NDIMPIL#1{% + \prftree[by]{$\scriptstyle\rightarrow% + \prfscript{I}_{\prfref<#1>}$}}\fi + \def\NDORIR{\prftree[by]{$\scriptstyle\vee% + \prfscript{I}_{\prfscript{R}}$}} + \def\NDORIL{\prftree[by]{$\scriptstyle\vee% + \prfscript{I}_{\prfscript{L}}$}} + \def\NDORI{\prftree[by]{$\scriptstyle\vee\prfscript{I}$}} + \def\NDORE{\prftree[by]{$\scriptstyle\vee\prfscript{E}$}} + \def\NDOREL#1{\prftree[by]{$\scriptstyle\vee% + \prfscript{I}_{\prfref<#1>}$}} + \def\NDALLI{\prftree[by]{$\scriptstyle\forall\prfscript{I}$}} + \def\NDALLE{\prftree[by]{$\scriptstyle\forall\prfscript{E}$}} + \def\NDEXI{\prftree[by]{$\scriptstyle\exists\prfscript{I}$}} + \def\NDEXE{\prftree[by]{$\scriptstyle\exists\prfscript{E}$}} + \def\NDEXEL#1{% + \prftree[by]{$\scriptstyle\exists\prfscript{E}_{\prfref<#1>}$}} + \def\NDTI{\prftree[by]{$\scriptstyle\top\prfscript{I}$}} + \def\NDFE{\prftree[by]{$\scriptstyle\bot\prfscript{E}$}} + \def\NDLEM{\prftree[by]{$\scriptstyle\prfscript{lem}$}} +\fi + +% ------------------------------------------------------------------- +% Sequent systems +% +% Package option [SEQ] +% ------------------------------------------------------------------- + +\ifprf@SEQOption% + \def\SEQA{\prfassumption} + \def\SEQD{\prfboundedassumption} + \def\SEQP{\prftree} + \def\SEQAX{\prftree[by]{$\scriptstyle\prfscript{Ax}$}} + \def\SEQLF{\prftree[by]{$\scriptstyle\prfscript{L}\bot$}} + \def\SEQLW{\prftree[by]{$\scriptstyle\prfscript{LW}$}} + \def\SEQRW{\prftree[by]{$\scriptstyle\prfscript{RW}$}} + \def\SEQLC{\prftree[by]{$\scriptstyle\prfscript{LC}$}} + \def\SEQRC{\prftree[by]{$\scriptstyle\prfscript{RC}$}} + \def\SEQLAND{\prftree[by]{$\scriptstyle\prfscript{L}\wedge$}} + \def\SEQRAND{\prftree[by]{$\scriptstyle\prfscript{R}\wedge$}} + \def\SEQLOR{\prftree[by]{$\scriptstyle\prfscript{L}\vee$}} + \def\SEQROR{\prftree[by]{$\scriptstyle\prfscript{R}\vee$}} + \ifprfIMPOption + \def\SEQLIMP{\prftree[by]{$\scriptstyle\prfscript{L}\supset$}} + \def\SEQRIMP{\prftree[by]{$\scriptstyle\prfscript{R}\supset$}} + \else + \def\SEQLIMP{\prftree[by]{$\scriptstyle\prfscript{L}% + \rightarrow$}} + \def\SEQRIMP{\prftree[by]{$\scriptstyle\prfscript{R}% + \rightarrow$}} + \fi + \def\SEQLALL{\prftree[by]{$\scriptstyle\prfscript{L}\forall$}} + \def\SEQRALL{\prftree[by]{$\scriptstyle\prfscript{R}\forall$}} + \def\SEQLEX{\prftree[by]{$\scriptstyle\prfscript{L}\exists$}} + \def\SEQREX{\prftree[by]{$\scriptstyle\prfscript{R}\exists$}} + \def\SEQCUT{\prftree[by]{$\scriptstyle\prfscript{Cut}$}} +\fi + +% ------------------------------------------------------------------- |