summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/prftree/prftree.sty
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2014-12-02 00:55:36 +0000
committerKarl Berry <karl@freefriends.org>2014-12-02 00:55:36 +0000
commitab4c97bb1913e7167819b3e3c2688a0e5200f011 (patch)
tree3a92d1b788fa89ea4c49b249e57e80162208cb55 /Master/texmf-dist/tex/latex/prftree/prftree.sty
parent5a51ac01bebab92f1bb7e8f4091a423e5ac6905d (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/prftree.sty')
-rw-r--r--Master/texmf-dist/tex/latex/prftree/prftree.sty1046
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
+
+% -------------------------------------------------------------------