summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/prftree
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/prftree
Initial commit
Diffstat (limited to 'macros/latex/contrib/prftree')
-rw-r--r--macros/latex/contrib/prftree/README9
-rw-r--r--macros/latex/contrib/prftree/prftree.sty1446
-rw-r--r--macros/latex/contrib/prftree/prftreedoc.pdfbin0 -> 346581 bytes
-rw-r--r--macros/latex/contrib/prftree/prftreedoc.tex2425
4 files changed, 3880 insertions, 0 deletions
diff --git a/macros/latex/contrib/prftree/README b/macros/latex/contrib/prftree/README
new file mode 100644
index 0000000000..5c6a8ef263
--- /dev/null
+++ b/macros/latex/contrib/prftree/README
@@ -0,0 +1,9 @@
+The prftree package provides a package to write proof trees for
+natural deduction calculi, sequent-like calculi, and similar.
+
+The package is composed by the filed
+- prftree.sty: containing the LaTeX engine to typeset proof trees;
+- prftreedoc.pdf: the human readable documentation for the package;
+- prftreedoc.tex: the source code for the documentation.
+
+The package is distributed under the GNU General Public License.
diff --git a/macros/latex/contrib/prftree/prftree.sty b/macros/latex/contrib/prftree/prftree.sty
new file mode 100644
index 0000000000..10d6fbce6c
--- /dev/null
+++ b/macros/latex/contrib/prftree/prftree.sty
@@ -0,0 +1,1446 @@
+%
+% prftree.sty
+% by Marco Benini - 19th June 2019
+% v1.6
+%
+% 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}[2019/06/19 Natural Deduction Proofs]
+
+% Package options: deactivated by default
+\newif\ifprf@NDOption\prf@NDOptionfalse
+\newif\ifprf@SEQOption\prf@SEQOptionfalse
+\newif\ifprfIMPOption\prfIMPOptionfalse
+\newif\ifprf@EQOption\prf@EQOptionfalse
+\newif\ifprf@MLOption\prf@MLOptionfalse
+\newif\ifprf@MLnodefOption\prf@MLnodefOptionfalse
+% but the STRUT and STRUTlabel are on by default
+\newif\ifprfSTRUToption\prfSTRUToptiontrue
+\newif\ifprfSTRUTlabeloption\prfSTRUTlabeloptiontrue
+
+\DeclareOption{ND}{\prf@NDOptiontrue}
+\DeclareOption{SEQ}{\prf@SEQOptiontrue}
+\DeclareOption{IMP}{\prfIMPOptiontrue}
+\DeclareOption{EQ}{\prf@EQOptiontrue}
+\DeclareOption{ML}{\prf@MLOptiontrue}
+\DeclareOption{MLnodef}{\prf@MLnodefOptiontrue}
+\DeclareOption{Strut}{\prfSTRUToptionfalse}
+\DeclareOption{StrutLabel}{\prfSTRUTlabeloptionfalse}
+\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.
+%--------------------------------------------------------------------
+
+% \prflinepadbefore default 0.3ex
+% the space between the bottom of assumptions and the proof line
+\newdimen\prflinepadbefore\prflinepadbefore.3ex
+
+% \prflinepadafter default 0.3ex
+% the space between the proof line and the top of the conclusion
+\newdimen\prflinepadafter\prflinepadafter.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.12ex
+% the thickness of the proof line
+\newdimen\prflinethickness\prflinethickness.12ex
+
+% \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 .8em
+% the space between two subsequent assumptions
+\newdimen\prfinterspace\prfinterspace.8em
+
+% \prfdoublelineinterspace default 1.2pt
+% the space between a double line
+\newdimen\prfdoublelineinterspace\prfdoublelineinterspace0.06ex
+
+% \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{-.4ex}[.2ex][0pt]{$\sim$}\hss}\hfill}
+
+% \prfConclusionBox
+% the command to draw the conclusion box
+\def\prfConclusionBox#1{%
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
+
+% \prfAssumptionBox
+% the command to draw the assumption box
+\def\prfAssumptionBox#1{%
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
+
+% \prfRuleNameBox
+% the command to draw the rule name box.
+\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
+
+% \prfLabelBox
+% the command to draw the label box.
+\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
+
+% \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 discards 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 prftree environment is used to define the scope of the
+% assumption references
+\newenvironment{prfenv}%
+ {\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 never been referenced before
+\def\ifprf@unrefref<#1>{%
+ \expandafter\ifx\csname prf@refref@@#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
+\newif\ifprf@refhack\prf@refhacktrue
+\protected\def\prfref<#1>{%
+ \ifprf@undefref<#1>\relax\mbox{??}%
+ \ifprf@refhack\label{prf@ref@hack}% to force recompilation
+ \global\prf@refhackfalse\fi%
+ \PackageWarningNoLine{prftree}{Undefined reference <#1>}%
+ \expandafter\gdef\csname prf@ref@@#1\endcsname{\mbox{??}}\else%
+ \csname prf@ref@@#1\endcsname\fi\relax}
+
+% 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% CHANGED FROM v1.0
+ \setbox\prf@fancybox\hbox{$\box\prf@fancybox^{#2}$}%
+ % \wd\prf@fancybox\prf@tmp% CHANGED FROM v1.0
+ \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 to4.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{%
+ \def\prf@hackpar{#2}%
+ \edef\prf@choice{\ifprf@label{#1}{\noexpand\prf@hackpar}\else%
+ {#1}{\noexpand\prf@hackpar}{}\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
+%--------------------------------------------------------------------
+
+\newbox\prf@@@@proofbox
+\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%
+ \hbox to2\prf@linewd{\cleaders\hbox to.5em{%
+ \hss\vrule height\prflinethickness%
+ width.3em depth0pt\hss}\hfill}%
+ \setbox\prf@fancybox\hbox to2\prf@linewd{%
+ \raise.4ex\box\prf@fancybox}\else%
+ \ifprf@dottedline%
+ \setbox\prf@fancybox%
+ \hbox to2\prf@linewd{\cleaders\hbox%
+ to.33em{\hss$\cdot$\hss}\hfill}\else%
+ % it must be a straight line!
+ \setbox\prf@fancybox\hbox{\vrule width2\prf@linewd%
+ height\prflinethickness}%
+ \setbox\prf@fancybox\hbox{\raise.4ex%
+ \box\prf@fancybox}\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@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 \prflinepadbefore; otherwise
+ % it is \linepadbefore 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\prflinepadbefore%
+ \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\prflinepadafter%
+ \ifprf@noline%
+ \ifprf@assum%
+ \advance\prf@temp\prfemptylinethickness\else%
+ \advance\prf@temp-\prflinepadafter\fi\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, 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$}}
+
+% -------------------------------------------------------------------
+% Support macros to define new inference rules
+%
+% \prfMakeInferenceRule#1#2
+% \prfMakeInferenceRuleRef#1#2
+% #1: name of the command associated to the inference rule
+% #2: rule name
+% The plain version generates a command for typesetting a proof with
+% the inference rule; the Ref version uses the first parameter of the
+% rule as a reference that is appended to the rule name
+% -------------------------------------------------------------------
+
+\def\prfMakeInferenceRule#1#2{%
+ \expandafter\def\csname #1\endcsname%
+ {\prftree[by]{$\scriptstyle{#2}$}}}
+\def\prfMakeInferenceRuleRef#1#2{%
+ \expandafter\def\csname #1\endcsname##1%
+ {\prftree[by]{$\scriptstyle{#2}^{\prfref<##1>}$}}}
+
+% -------------------------------------------------------------------
+% Macros to stack the premises of an inference rule
+%
+% \prfStackPremises{a_1}...{a_n} generates a vertical list containing
+% a_1 on the top and a_n on the bottom.
+% -------------------------------------------------------------------
+
+\def\prfStackPremises{\prf@StackPremises{}}
+\def\prf@StackPremises#1{\@ifnextchar\bgroup%
+ {\prf@@StackPremises{\prfassumption{#1}}}%
+ {\prfassumption{#1}}}
+\def\prf@@StackPremises#1#2{\@ifnextchar\bgroup%
+ {\prf@@@StackPremises{\prftree[noline]{#1}{#2}}}%
+ {\prftree[noline]{#1}{#2}}}
+\def\prf@@@StackPremises#1#2{\@ifnextchar\bgroup%
+ {\prf@@@StackPremises{\prftree[noline]{#1}{#2}}}
+ {\prftree[noline]{#1}{#2}}}
+
+% -------------------------------------------------------------------
+% Natural deduction systems
+%
+% Package option [ND]
+% -------------------------------------------------------------------
+
+\ifprf@NDOption%
+ \def\NDA{\prfassumption}
+ \def\NDD{\prfboundedassumption}
+ \def\NDAL#1{\prfassumption<#1>}
+ \def\NDDL#1{\prfboundedassumption<#1>}
+ \def\NDP{\prftree}
+ \prfMakeInferenceRule{NDANDI}{\mathord{\wedge}\textup{I}}
+ \prfMakeInferenceRule{NDANDEL}{\mathord{\wedge}\textup{E}_1}
+ \prfMakeInferenceRule{NDANDER}{\mathord{\wedge}\textup{E}_2}
+ \prfMakeInferenceRule{NDANDE}{\mathord{\wedge}\textup{E}}
+ \prfMakeInferenceRule{NDORIL}{\mathord{\vee}\textup{I}_1}
+ \prfMakeInferenceRule{NDORIR}{\mathord{\vee}\textup{I}_2}
+ \prfMakeInferenceRule{NDORI}{\mathord{\vee}\textup{I}}
+ \prfMakeInferenceRule{NDORE}{\mathord{\vee}\textup{E}}
+ \prfMakeInferenceRuleRef{NDOREL}{\mathord{\vee}\textup{E}}
+ \ifprfIMPOption
+ \prfMakeInferenceRule{NDIMPI}{\mathord{\supset}\textup{I}}
+ \prfMakeInferenceRule{NDIMPE}{\mathord{\supset}\textup{E}}
+ \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\supset}\textup{I}}
+ \else
+ \prfMakeInferenceRule{NDIMPI}{\mathord{\rightarrow}\textup{I}}
+ \prfMakeInferenceRule{NDIMPE}{\mathord{\rightarrow}\textup{E}}
+ \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\rightarrow}\textup{I}}
+ \fi
+ \prfMakeInferenceRule{NDNOTI}{\mathord{\neg}\textup{I}}
+ \prfMakeInferenceRuleRef{NDNOTIL}{\mathord{\neg}\textup{I}}
+ \prfMakeInferenceRule{NDNOTE}{\mathord{\neg}\textup{E}}
+ \prfMakeInferenceRule{NDALLI}{\mathord{\forall}\textup{I}}
+ \prfMakeInferenceRule{NDALLE}{\mathord{\forall}\textup{E}}
+ \prfMakeInferenceRule{NDEXI}{\mathord{\exists}\textup{I}}
+ \prfMakeInferenceRule{NDEXE}{\mathord{\exists}\textup{E}}
+ \prfMakeInferenceRuleRef{NDEXEL}{\mathord{\exists}\textup{E}}
+ \prfMakeInferenceRule{NDTI}{\mathord{\top}\textup{I}}
+ \prfMakeInferenceRule{NDFE}{\mathord{\bot}\textup{E}}
+ \prfMakeInferenceRule{NDLEM}{\textup{lem}}
+ \prfMakeInferenceRule{NDAX}{\textup{ax}}
+\fi
+
+% -------------------------------------------------------------------
+% Sequent systems
+%
+% Package option [SEQ]
+% -------------------------------------------------------------------
+
+\ifprf@SEQOption%
+ \def\SEQA{\prfassumption}
+ \def\SEQD{\prfboundedassumption}
+ \def\SEQP{\prftree}
+ \prfMakeInferenceRule{SEQAX}{\textup{Ax}}
+ \prfMakeInferenceRule{SEQLF}{\textup{L}\mathord{\bot}}
+ \prfMakeInferenceRule{SEQLW}{\textup{LW}}
+ \prfMakeInferenceRule{SEQRW}{\textup{RW}}
+ \prfMakeInferenceRule{SEQLC}{\textup{LC}}
+ \prfMakeInferenceRule{SEQRC}{\textup{RC}}
+ \prfMakeInferenceRule{SEQLAND}{\textup{L}\mathord{\wedge}}
+ \prfMakeInferenceRule{SEQLANDL}{\textup{L}\mathord{\wedge}_1}
+ \prfMakeInferenceRule{SEQLANDR}{\textup{L}\mathord{\wedge}_2}
+ \prfMakeInferenceRule{SEQRAND}{\textup{R}\mathord{\wedge}}
+ \prfMakeInferenceRule{SEQLOR}{\textup{L}\mathord{\vee}}
+ \prfMakeInferenceRule{SEQROR}{\textup{R}\mathord{\vee}}
+ \prfMakeInferenceRule{SEQRORL}{\textup{R}\mathord{\vee}_1}
+ \prfMakeInferenceRule{SEQRORR}{\textup{R}\mathord{\vee}_2}
+ \ifprfIMPOption
+ \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\supset}}
+ \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\supset}}
+ \else
+ \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\rightarrow}}
+ \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\rightarrow}}
+ \fi
+ \prfMakeInferenceRule{SEQLALL}{\textup{L}\mathord{\forall}}
+ \prfMakeInferenceRule{SEQRALL}{\textup{R}\mathord{\forall}}
+ \prfMakeInferenceRule{SEQLEX}{\textup{L}\mathord{\exists}}
+ \prfMakeInferenceRule{SEQREX}{\textup{R}\mathord{\exists}}
+ \prfMakeInferenceRule{SEQCUT}{\textup{Cut}}
+\fi
+
+% -------------------------------------------------------------------
+% Equality rules
+%
+% Package option [EQ]
+% -------------------------------------------------------------------
+
+\ifprf@EQOption%
+ \prfMakeInferenceRule{EQREFL}{\textup{refl}}
+ \prfMakeInferenceRule{EQSYM}{\textup{sym}}
+ \prfMakeInferenceRule{EQTRANS}{\textup{trans}}
+ \prfMakeInferenceRule{EQSUBST}{\textup{subst}}
+\fi
+
+% -------------------------------------------------------------------
+% Martin-Lof and Homotopy Type Theory
+%
+% Package option [ML]
+% -------------------------------------------------------------------
+
+\ifprf@MLOption
+ \ifprf@MLnodefOption\relax\else
+ \def\type{\mathbin{:}}
+ \def\universe{\mathcal{U}}
+ \def\context{\mathsf{ctx}}
+ \def\judgementaldef{\mathbin{:\equiv}}
+ \def\propositionaldef{\mathbin{:=}}
+ \def\identitytype{\mathsf{Id}}
+ \def\refl{\mathsf{refl}}
+ \def\emptytype{\mathbf{0}}
+ \def\unittype{\mathbf{1}}
+ \def\booleantype{\mathbf{2}}
+ \def\axiomofchoice{\mathsf{AC}}
+ \def\accessibility{\mathsf{acc}}
+ \def\ap{\mathsf{ap}}
+ \def\apd{\mathsf{apd}}
+ \def\basepoint{\mathsf{base}}
+ \def\biinv{\mathsf{biinv}}
+ \def\cardtype{\mathsf{Card}}
+ \def\cocone{\mathsf{cocone}}
+ \def\cons{\mathsf{cons}}
+ \def\contr{\mathsf{contr}}
+ \def\equivtype{\mathsf{Equiv}}
+ \def\ext{\mathsf{ext}}
+ \def\fiber{\mathsf{fib}}
+ \def\funext{\mathsf{funext}}
+ \def\glue{\mathsf{glue}}
+ \def\happly{\mathsf{happly}}
+ \def\hom{\mathsf{hom}}
+ \def\id{\mathsf{id}}
+ \def\idtoeqv{\mathsf{idtoeqv}}
+ \def\idtoiso{\mathsf{idtoiso}}
+ \def\im{\mathsf{im}}
+ \def\ind{\mathsf{ind}}
+ \def\inj{\mathsf{inj}}
+ \def\inl{\mathsf{inl}}
+ \def\inr{\mathsf{inr}}
+ \def\iscontr{\mathsf{isContr}}
+ \def\isequiv{\mathsf{isequiv}}
+ \def\ishae{\mathsf{ishae}}
+ \def\isotoid{\mathsf{istoid}}
+ \def\isntype#1{\mathsf{is-}{#1}\mathsf{-type}}
+ \def\isprop{\mathsf{isProp}}
+ \def\isset{\mathsf{isSet}}
+ \def\ker{\mathsf{ker}}
+ \def\LEM{\mathsf{LEM}}
+ \def\linv{\mathsf{linv}}
+ \def\listtype{\mathsf{List}}
+ \def\loopcons{\mathsf{loop}}
+ \def\Map{\mathsf{Map}}
+ \def\merid{\mathsf{merid}}
+ \def\nil{\mathsf{nil}}
+ \def\ordtype{\mathsf{Ord}}
+ \def\pair{\mathsf{pair}}
+ \def\pred{\mathsf{pred}}
+ \def\pr{\mathsf{pr}}
+ \def\Prop{\mathsf{Prop}}
+ \def\qinv{\mathsf{qinv}}
+ \def\rec{\mathsf{rec}}
+ \def\rinv{\mathsf{rinv}}
+ \def\seg{\mathsf{seg}}
+ \def\Set{\mathsf{Set}}
+ \def\Succ{\mathsf{succ}}
+ \def\sup{\mathsf{sup}}
+ \def\total{\mathsf{total}}
+ \def\transport{\mathsf{transport}}
+ \def\transportconst{\mathsf{transportconst}}
+ \def\ua{\mathsf{ua}}
+ \def\Wtype{\mathsf{W}}
+ \fi
+
+ \def\MLctxEMPrule{\ensuremath{\mathsf{ctx}\mathsf{-EMP}}}
+ \def\MLctxEXTrule{\ensuremath{\mathsf{ctx}\mathsf{-EXT}}}
+ \def\MLVblerule{\ensuremath{\mathsf{Vble}}}
+ \def\MLSubstrule{\ensuremath{\mathsf{Subst}}}
+ \def\MLWkgrule{\ensuremath{\mathsf{Wkg}}}
+ \def\MLEQreflrule{\ensuremath{\mathord{\equiv}\mathsf{-refl}}}
+ \def\MLEQsymrule{\ensuremath{\mathord{\equiv}\mathsf{-sym}}}
+ \def\MLEQtransrule{\ensuremath{\mathord{\equiv}\mathsf{-trans}}}
+ \def\MLEQsubstrule{\ensuremath{\mathord{\equiv}\mathsf{-subst}}}
+ \def\MLEQsubsteqrule{\ensuremath{\mathord{\equiv}%
+ \mathsf{-subst}\mathsf{-eq}}}
+ \def\MLUintrorule{\ensuremath{\universe\mathsf{-intro}}}
+ \def\MLUcumulrule{\ensuremath{\universe\mathsf{-cumul}}}
+ \def\MLUcumuleqrule{\ensuremath{\universe%
+ \mathsf{-cumul}\mathsf{-eq}}}
+ \def\MLpiformrule{\ensuremath{\Pi\mathsf{-form}}}
+ \def\MLpiformeqrule{\ensuremath{\Pi\mathsf{-form}\mathsf{-eq}}}
+ \def\MLpiintrorule{\ensuremath{\Pi\mathsf{-intro}}}
+ \def\MLpiintroeqrule{\ensuremath{\Pi\mathsf{-intro}\mathsf{-eq}}}
+ \def\MLpielimrule{\ensuremath{\Pi\mathsf{-elim}}}
+ \def\MLpielimeqrule{\ensuremath{\Pi\mathsf{-elim}\mathsf{-eq}}}
+ \def\MLpicomprule{\ensuremath{\Pi\mathsf{-comp}}}
+ \def\MLpiuniqrule{\ensuremath{\Pi\mathsf{-uniq}}}
+ \def\MLKintrorule{\ensuremath{k\mathsf{-intro}}}
+ \def\MLsigmaformrule{\ensuremath{\Sigma\mathsf{-form}}}
+ \def\MLsigmaintrorule{\ensuremath{\Sigma\mathsf{-intro}}}
+ \def\MLsigmaelimrule{\ensuremath{\Sigma\mathsf{-elim}}}
+ \def\MLsigmacomprule{\ensuremath{\Sigma\mathsf{-comp}}}
+ \def\MLsigmauniqrule{\ensuremath{\Sigma\mathsf{-uniq}}}
+ \def\MLplusformrule{\ensuremath{\mathord{+}\mathsf{-form}}}
+ \def\MLplusintrolrule{\ensuremath{\mathord{+}\mathsf{-intro}_1}}
+ \def\MLplusintrorrule{\ensuremath{\mathord{+}\mathsf{-intro}_2}}
+ \def\MLpluselimrule{\ensuremath{\mathord{+}\mathsf{-elim}}}
+ \def\MLpluscomplrule{\ensuremath{\mathord{+}\mathsf{-comp}_1}}
+ \def\MLpluscomprrule{\ensuremath{\mathord{+}\mathsf{-comp}_2}}
+ \def\MLplusuniqrule{\ensuremath{\mathord{+}\mathsf{-uniq}}}
+ \def\MLzeroformrule{\ensuremath{\mathbf{0}\mathsf{-form}}}
+ \def\MLzeroelimrule{\ensuremath{\mathbf{0}\mathsf{-elim}}}
+ \def\MLzerouniqrule{\ensuremath{\mathbf{0}\mathsf{-uniq}}}
+ \def\MLunitformrule{\ensuremath{\mathbf{1}\mathsf{-form}}}
+ \def\MLunitintrorule{\ensuremath{\mathbf{1}\mathsf{-intro}}}
+ \def\MLunitelimrule{\ensuremath{\mathbf{1}\mathsf{-elim}}}
+ \def\MLunitcomprule{\ensuremath{\mathbf{1}\mathsf{-comp}}}
+ \def\MLunituniqrule{\ensuremath{\mathbf{1}\mathsf{-uniq}}}
+ \def\MLnatformrule{\ensuremath{\mathbb{N}\mathsf{-form}}}
+ \def\MLnatintrozerorule{\ensuremath{\mathbb{N}\mathsf{-intro}_1}}
+ \def\MLnatintrosuccrule{\ensuremath{\mathbb{N}\mathsf{-intro}_2}}
+ \def\MLnatelimrule{\ensuremath{\mathbb{N}\mathsf{-elim}}}
+ \def\MLnatcompzerorule{\ensuremath{\mathbb{N}\mathsf{-comp}_1}}
+ \def\MLnatcompsuccrule{\ensuremath{\mathbb{N}\mathsf{-comp}_2}}
+ \def\MLnatuniqrule{\ensuremath{\mathbb{N}\mathsf{-uniq}}}
+ \def\MLidformrule{\ensuremath{\mathord{=}\mathsf{-form}}}
+ \def\MLidintrorule{\ensuremath{\mathord{=}\mathsf{-intro}}}
+ \def\MLidelimrule{\ensuremath{\mathord{=}\mathsf{-elim}}}
+ \def\MLidcomprule{\ensuremath{\mathord{=}\mathsf{-comp}}}
+ \def\MLiduniqrule{\ensuremath{\mathord{=}\mathsf{-uniq}}}
+ \def\MLwformrule{\ensuremath{\mathsf{W}\mathsf{-form}}}
+ \def\MLwintrorule{\ensuremath{\mathsf{W}\mathsf{-intro}}}
+ \def\MLwelimrule{\ensuremath{\mathsf{W}\mathsf{-elim}}}
+ \def\MLwcomprule{\ensuremath{\mathsf{W}\mathsf{-comp}}}
+ \def\MLwuniqrule{\ensuremath{\mathsf{W}\mathsf{-uniq}}}
+ \def\MLListformrule{\ensuremath{\mathsf{List}\mathsf{-form}}}
+ \def\MLListintronrule{\ensuremath{\mathsf{List}\mathsf{-intro_1}}}
+ \def\MLListintrocrule{\ensuremath{\mathsf{List}\mathsf{-intro_2}}}
+ \def\MLListelimrule{\ensuremath{\mathsf{List}\mathsf{-elim}}}
+ \def\MLListcompnrule{\ensuremath{\mathsf{List}\mathsf{-comp_1}}}
+ \def\MLListcompcrule{\ensuremath{\mathsf{List}\mathsf{-comp_2}}}
+ \def\MLListuniqrule{\ensuremath{\mathsf{List}\mathsf{-uniq}}}
+ \def\MLfunextrule{\ensuremath{\Pi\mathsf{-ext}}}
+ \def\MLunivrule{\ensuremath{\universe_i\mathsf{-univ}}}
+ \def\MLSformrule{\ensuremath{\mathbb{S}^1\mathsf{-form}}}
+ \def\MLSintrorule{\ensuremath{\mathbb{S}^1\mathsf{-intro}}}
+ \def\MLSelimrule{\ensuremath{\mathbb{S}^1\mathsf{-elim}}}
+ \def\MLScomprule{\ensuremath{\mathbb{S}^1\mathsf{-comp}}}
+ \def\MLSuniqrule{\ensuremath{\mathbb{S}^1\mathsf{-uniq}}}
+ \def\MLSpeqintrorule{\ensuremath{\mathbb{S}^1\mathsf{-intro}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLSpeqcomprule{\ensuremath{\mathbb{S}^1\mathsf{-comp}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLIformrule{\ensuremath{I\mathsf{-form}}}
+ \def\MLIintroarule{\ensuremath{I\mathsf{-intro}_1}}
+ \def\MLIintrobrule{\ensuremath{I\mathsf{-intro}_2}}
+ \def\MLIelimrule{\ensuremath{I\mathsf{-elim}}}
+ \def\MLIcomparule{\ensuremath{I\mathsf{-comp}_1}}
+ \def\MLIcompbrule{\ensuremath{I\mathsf{-comp}_2}}
+ \def\MLIuniqrule{\ensuremath{I\mathsf{-uniq}}}
+ \def\MLIpeqintrorule{\ensuremath{I\mathsf{-intro}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLIpeqcomprule{\ensuremath{I\mathsf{-comp}{-}\mathsf{=}}}
+ \def\MLsigmaintroarule{\ensuremath{\Sigma\mathsf{-intro}_1}}
+ \def\MLsigmaintrobrule{\ensuremath{\Sigma\mathsf{-intro}_2}}
+ \def\MLsigmacomparule{\ensuremath{\Sigma\mathsf{-comp}_1}}
+ \def\MLsigmacompbrule{\ensuremath{\Sigma\mathsf{-comp}_2}}
+ \def\MLsigmapeqintrorule{\ensuremath{\Sigma\mathsf{-intro}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLsigmapeqcomprule{\ensuremath{\Sigma\mathsf{-comp}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLPOformrule{\ensuremath{\sqcup\mathsf{-form}}}
+ \def\MLPOintroarule{\ensuremath{\sqcup\mathsf{-intro}_1}}
+ \def\MLPOintrobrule{\ensuremath{\sqcup\mathsf{-intro}_2}}
+ \def\MLPOelimrule{\ensuremath{\sqcup\mathsf{-elim}}}
+ \def\MLPOcomparule{\ensuremath{\sqcup\mathsf{-comp}_1}}
+ \def\MLPOcompbrule{\ensuremath{\sqcup\mathsf{-comp}_2}}
+ \def\MLPOuniqrule{\ensuremath{\sqcup\mathsf{-uniq}}}
+ \def\MLPOpeqintrorule{\ensuremath{\sqcup\mathsf{-intro}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLPOpeqcomprule{\ensuremath{\sqcup%
+ \mathsf{-comp}\mathsf{-}\mathsf{=}}}
+ \def\MLTformrule{\ensuremath{||\cdot||\mathsf{-form}}}
+ \def\MLTintrorule{\ensuremath{||\cdot||\mathsf{-intro}}}
+ \def\MLTelimrule{\ensuremath{||\cdot||\mathsf{-elim}}}
+ \def\MLTcomprule{\ensuremath{||\cdot||\mathsf{-comp}}}
+ \def\MLTuniqrule{\ensuremath{||\cdot||\mathsf{-uniq}}}
+ \def\MLTpeqintrorule{\ensuremath{||\cdot||\mathsf{-intro}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLTpeqcomprule{\ensuremath{||\cdot||\mathsf{-comp}%
+ \mathsf{-}\mathsf{=}}}
+ \def\MLtorusformrule{\ensuremath{T^2\mathsf{-form}}}
+ \def\MLtorusintrorule{\ensuremath{T^2\mathsf{-intro}}}
+ \def\MLtoruselimrule{\ensuremath{T^2\mathsf{-elim}}}
+ \def\MLtoruscomprule{\ensuremath{T^2\mathsf{-comp}}}
+ \def\MLtoruspeqintroarule{\ensuremath{T^2\mathsf{-intro}%
+ \mathsf{-}\mathsf{=_p}}}
+ \def\MLtoruspeqintrobrule{\ensuremath{T^2\mathsf{-intro}%
+ \mathsf{-}\mathsf{=_q}}}
+ \def\MLtoruspeqintrocrule{\ensuremath{T^2\mathsf{-intro}%
+ \mathsf{-}\mathsf{=_t}}}
+ \def\MLtoruspeqcomparule{\ensuremath{T^2\mathsf{-comp}%
+ \mathsf{-}\mathsf{=_p}}}
+ \def\MLtoruspeqcompbrule{\ensuremath{T^2\mathsf{-comp}%
+ \mathsf{-}\mathsf{=_q}}}
+ \def\MLtoruspeqcompcrule{\ensuremath{T^2\mathsf{-comp}%
+ \mathsf{-}\mathsf{=_t}}}
+
+ \prfMakeInferenceRule{MLctxEMP}{\MLctxEMPrule}
+ \prfMakeInferenceRule{MLctxEXT}{\MLctxEXTrule}
+ \prfMakeInferenceRule{MLSubst}{\MLSubstrule}
+ \prfMakeInferenceRule{MLWkg}{\MLWkgrule}
+ \prfMakeInferenceRule{MLVble}{\MLVblerule}
+ \prfMakeInferenceRule{MLEQrefl}{\MLEQreflrule}
+ \prfMakeInferenceRule{MLEQsym}{\MLEQsymrule}
+ \prfMakeInferenceRule{MLEQtrans}{\MLEQtransrule}
+ \prfMakeInferenceRule{MLEQsubst}{\MLEQsubstrule}
+ \prfMakeInferenceRule{MLEQsubsteq}{\MLEQsubsteqrule}
+ \prfMakeInferenceRule{MLUintro}{\MLUintrorule}
+ \prfMakeInferenceRule{MLUcumul}{\MLUcumulrule}
+ \prfMakeInferenceRule{MLUcumuleq}{\MLUcumuleqrule}
+ \prfMakeInferenceRule{MLpiform}{\MLpiformrule}
+ \prfMakeInferenceRule{MLpiformeq}{\MLpiformeqrule}
+ \prfMakeInferenceRule{MLpiintro}{\MLpiintrorule}
+ \prfMakeInferenceRule{MLpiintroeq}{\MLpiintroeqrule}
+ \prfMakeInferenceRule{MLpielim}{\MLpielimrule}
+ \prfMakeInferenceRule{MLpielimeq}{\MLpielimeqrule}
+ \prfMakeInferenceRule{MLpicomp}{\MLpicomprule}
+ \prfMakeInferenceRule{MLpiuniq}{\MLpiuniqrule}
+ \prfMakeInferenceRule{MLKintro}{\MLKintrorule}
+ \prfMakeInferenceRule{MLsigmaform}{\MLsigmaformrule}
+ \prfMakeInferenceRule{MLsigmaintro}{\MLsigmaintrorule}
+ \prfMakeInferenceRule{MLsigmaelim}{\MLsigmaelimrule}
+ \prfMakeInferenceRule{MLsigmacomp}{\MLsigmacomprule}
+ \prfMakeInferenceRule{MLsigmauniq}{\MLsigmauniqrule}
+ \prfMakeInferenceRule{MLplusform}{\MLplusformrule}
+ \prfMakeInferenceRule{MLplusintrol}{\MLplusintrolrule}
+ \prfMakeInferenceRule{MLplusintror}{\MLplusintrorrule}
+ \prfMakeInferenceRule{MLpluselim}{\MLpluselimrule}
+ \prfMakeInferenceRule{MLpluscompl}{\MLpluscomplrule}
+ \prfMakeInferenceRule{MLpluscompr}{\MLpluscomprrule}
+ \prfMakeInferenceRule{MLplusuniq}{\MLplusuniqrule}
+ \prfMakeInferenceRule{MLzeroform}{\MLzeroformrule}
+ \prfMakeInferenceRule{MLzeroelim}{\MLzeroelimrule}
+ \prfMakeInferenceRule{MLzerouniq}{\MLzerouniqrule}
+ \prfMakeInferenceRule{MLunitform}{\MLunitformrule}
+ \prfMakeInferenceRule{MLunitintro}{\MLunitintrorule}
+ \prfMakeInferenceRule{MLunitelim}{\MLunitelimrule}
+ \prfMakeInferenceRule{MLunitcomp}{\MLunitcomprule}
+ \prfMakeInferenceRule{MLunituniq}{\MLunituniqrule}
+ \prfMakeInferenceRule{MLnatform}{\MLnatformrule}
+ \prfMakeInferenceRule{MLnatintrozero}{\MLnatintrozerorule}
+ \prfMakeInferenceRule{MLnatintrosucc}{\MLnatintrosuccrule}
+ \prfMakeInferenceRule{MLnatelim}{\MLnatelimrule}
+ \prfMakeInferenceRule{MLnatcompzero}{\MLnatcompzerorule}
+ \prfMakeInferenceRule{MLnatcompsucc}{\MLnatcompsuccrule}
+ \prfMakeInferenceRule{MLnatuniq}{\MLnatuniqrule}
+ \prfMakeInferenceRule{MLidform}{\MLidformrule}
+ \prfMakeInferenceRule{MLidintro}{\MLidintrorule}
+ \prfMakeInferenceRule{MLidelim}{\MLidelimrule}
+ \prfMakeInferenceRule{MLidcomp}{\MLidcomprule}
+ \prfMakeInferenceRule{MLiduniq}{\MLiduniqrule}
+ \prfMakeInferenceRule{MLwform}{\MLwformrule}
+ \prfMakeInferenceRule{MLwintro}{\MLwintrorule}
+ \prfMakeInferenceRule{MLwelim}{\MLwelimrule}
+ \prfMakeInferenceRule{MLwcomp}{\MLwcomprule}
+ \prfMakeInferenceRule{MLwuniq}{\MLwuniqrule}
+ \prfMakeInferenceRule{MLListform}{\MLListformrule}
+ \prfMakeInferenceRule{MLListintron}{\MLListintronrule}
+ \prfMakeInferenceRule{MLListintroc}{\MLListintrocrule}
+ \prfMakeInferenceRule{MLListelim}{\MLListelimrule}
+ \prfMakeInferenceRule{MLListcompn}{\MLListcompnrule}
+ \prfMakeInferenceRule{MLListcompc}{\MLListcompcrule}
+ \prfMakeInferenceRule{MLListuniq}{\MLListuniqrule}
+ \prfMakeInferenceRule{MLfunext}{\MLfunextrule}
+ \prfMakeInferenceRule{MLuniv}{\MLunivrule}
+ \prfMakeInferenceRule{MLSform}{\MLSformrule}
+ \prfMakeInferenceRule{MLSintro}{\MLSintrorule}
+ \prfMakeInferenceRule{MLSelim}{\MLSelimrule}
+ \prfMakeInferenceRule{MLScomp}{\MLScomprule}
+ \prfMakeInferenceRule{MLSuniq}{\MLSuniqrule}
+ \prfMakeInferenceRule{MLSpeqintro}{\MLSpeqintrorule}
+ \prfMakeInferenceRule{MLSpeqcomp}{\MLSpeqcomprule}
+ \prfMakeInferenceRule{MLIform}{\MLIformrule}
+ \prfMakeInferenceRule{MLIintroa}{\MLIintroarule}
+ \prfMakeInferenceRule{MLIintrob}{\MLIintrobrule}
+ \prfMakeInferenceRule{MLIelim}{\MLIelimrule}
+ \prfMakeInferenceRule{MLIcompa}{\MLIcomparule}
+ \prfMakeInferenceRule{MLIcompb}{\MLIcompbrule}
+ \prfMakeInferenceRule{MLIuniq}{\MLIuniqrule}
+ \prfMakeInferenceRule{MLIpeqintro}{\MLIpeqintrorule}
+ \prfMakeInferenceRule{MLIpeqcomp}{\MLIpeqcomprule}
+ \prfMakeInferenceRule{MLsigmaintroa}{\MLsigmaintroarule}
+ \prfMakeInferenceRule{MLsigmaintrob}{\MLsigmaintrobrule}
+ \prfMakeInferenceRule{MLsigmacompa}{\MLsigmacomparule}
+ \prfMakeInferenceRule{MLsigmacompb}{\MLsigmacompbrule}
+ \prfMakeInferenceRule{MLsigmapeqintro}{\MLsigmapeqintrorule}
+ \prfMakeInferenceRule{MLsigmapeqcomp}{\MLsigmapeqcomprule}
+ \prfMakeInferenceRule{MLPOform}{\MLPOformrule}
+ \prfMakeInferenceRule{MLPOintroa}{\MLPOintroarule}
+ \prfMakeInferenceRule{MLPOintrob}{\MLPOintrobrule}
+ \prfMakeInferenceRule{MLPOelim}{\MLPOelimrule}
+ \prfMakeInferenceRule{MLPOcompa}{\MLPOcomparule}
+ \prfMakeInferenceRule{MLPOcompb}{\MLPOcompbrule}
+ \prfMakeInferenceRule{MLPOuniq}{\MLPOuniqrule}
+ \prfMakeInferenceRule{MLPOpeqintro}{\MLPOpeqintrorule}
+ \prfMakeInferenceRule{MLPOpeqcomp}{\MLPOpeqcomprule}
+ \prfMakeInferenceRule{MLTform}{\MLTformrule}
+ \prfMakeInferenceRule{MLTintro}{\MLTintrorule}
+ \prfMakeInferenceRule{MLTelim}{\MLTelimrule}
+ \prfMakeInferenceRule{MLTcomp}{\MLTcomprule}
+ \prfMakeInferenceRule{MLTuniq}{\MLTuniqrule}
+ \prfMakeInferenceRule{MLTpeqintro}{\MLTpeqintrorule}
+ \prfMakeInferenceRule{MLTpeqcomp}{\MLTpeqcomprule}
+ \prfMakeInferenceRule{MLtorusform}{\MLtorusformrule}
+ \prfMakeInferenceRule{MLtorusintro}{\MLtorusintrorule}
+ \prfMakeInferenceRule{MLtoruselim}{\MLtoruselimrule}
+ \prfMakeInferenceRule{MLtoruscomp}{\MLtoruscomprule}
+ \prfMakeInferenceRule{MLtoruspeqintroa}{\MLtoruspeqintroarule}
+ \prfMakeInferenceRule{MLtoruspeqintrob}{\MLtoruspeqintrobrule}
+ \prfMakeInferenceRule{MLtoruspeqintroc}{\MLtoruspeqintrocrule}
+ \prfMakeInferenceRule{MLtoruspeqcompa}{\MLtoruspeqcomparule}
+ \prfMakeInferenceRule{MLtoruspeqcompb}{\MLtoruspeqcompbrule}
+ \prfMakeInferenceRule{MLtoruspeqcompc}{\MLtoruspeqcompcrule}
+\fi
+% -------------------------------------------------------------------
diff --git a/macros/latex/contrib/prftree/prftreedoc.pdf b/macros/latex/contrib/prftree/prftreedoc.pdf
new file mode 100644
index 0000000000..5f3b0a615e
--- /dev/null
+++ b/macros/latex/contrib/prftree/prftreedoc.pdf
Binary files differ
diff --git a/macros/latex/contrib/prftree/prftreedoc.tex b/macros/latex/contrib/prftree/prftreedoc.tex
new file mode 100644
index 0000000000..19477fa856
--- /dev/null
+++ b/macros/latex/contrib/prftree/prftreedoc.tex
@@ -0,0 +1,2425 @@
+\documentclass{amsart}
+\usepackage{color}
+\usepackage{graphics}
+\usepackage[ND,SEQ,EQ,ML]{prftree}
+\usepackage{url}
+\usepackage{microtype}
+
+\setlength{\fboxsep}{0pt}
+
+\begin{document}
+\title{Proof Trees in \LaTeX}
+\date{}
+\author{Marco Benini}
+\address{Dipartimento di Scienza e Alta Tecnologia\\
+ Universit\`a degli Studi dell'Insubria\\
+ via Valleggio 11, I-22100 Como, Italy}
+\email{marco.benini@uninsubria.it}
+\urladdr{http://marcobenini.wordpress.com}
+\maketitle
+
+% --------------------------
+
+\section{Introduction}\label{sec:introduction}
+Writing proofs in natural deduction or in similar, tree-like calculi,
+is always a challenge: from the typographical point of view, these
+proofs are complex objects that cannot be simply typeset using the
+standard \LaTeX{} commands. Thus, many packages have been developed:
+Sam Buss's \texttt{bussproofs.sty},
+\url{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}; Makoto
+Tatsuta's \texttt{proof.sty},
+\url{http://research.nii.ac.jp/~tatsuta/proof-sty.html}; and
+\texttt{prooftree.sty} by Paul Taylor,
+\url{http://mirror.ctan.org/macros/generic/proofs/taylor}.
+
+All these packages have their merits and weaknesses. For example,
+Buss's package is extremely flexible but inference rules with more
+than five assumptions cannot be directly typeset. On the other hand,
+Tatsuta's package provides a very simple set of commands doing a
+fine job, but customisation is very limited. Taylor's package provides
+a natural syntax for writing proofs, but customisation is limited, and
+the package has an expire date.
+
+The package presented in the following provides most of the features
+which are already present in Buss's package, coupled with some new
+ones. This package uses a syntax which is closer to Tatsuta's one, but
+almost all the typesetting process is parametric, so that each bit of
+a proof can be customised at will.
+
+The graphical appearance of a proof is similar to the one obtained
+using Taylor's package, but the additional features allow to set up
+the graphical output to follow the style of some of the standard
+textbooks, e.g., A.S.~Troelstra and H.~Schwichtenberg, \textit{Basic
+ Proof Theory}, Cambridge University Press (2000).
+
+% --------------------------
+\clearpage
+\section{Basic Commands}\label{sec:basic_commands}
+The package is invoked by putting \verb|\usepackage{prftree.sty}| in
+the preamble of the document, and installation reduces to put the file
+\texttt{prftree.sty} somewhere in the \LaTeX{} search
+path.\vspace{2ex}
+
+A proof tree constructs a box with the following internal structure:
+\begin{center}
+ {\setlength{\unitlength}{1em}
+ \begin{picture}(31,6)
+ \put(7,4){\framebox(17,2){$\mbox{assumption}_1 \cdots
+ \mbox{assumption}_n$}}
+ \put(6,3){\line(1,0){19}}
+ \put(26,2){\framebox(5,2){rule name}}
+ \put(0,2){\framebox(5,2){label}}
+ \put(10,0){\framebox(11,2){conclusion}}
+ \end{picture}}
+\end{center}
+In turn, each assumption is typeset as a box which has usually the
+shape of another proof tree, while the rule name and the label are
+typeset in a text box, and the conclusion in a math box. The aspect of
+the proof line is controlled by suitable options, as is the presence
+of the rule name and of the label. Options cover other aspects of the
+graphical rendering of a proof tree, as it will be explained
+later. The basic command to build a proof tree is \verb|\prftree|.
+
+For example, the proof of $A \supset \neg\neg A$ in natural deduction
+is:
+\begin{displaymath}
+ \prftree[r]{$\scriptstyle\supset\mathrm{I}$}
+ {\prftree[r]{$\scriptstyle\supset\mathrm{I}$}
+ {\prftree[r]{$\scriptstyle\supset\mathrm{E}$}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+This proof is generated by the following \LaTeX{} code:
+\begin{verbatim}
+ \begin{displaymath}
+ \prftree[r]{$\scriptstyle\supset\mathrm{I}$}
+ {\prftree[r]{$\scriptstyle\supset\mathrm{I}$}
+ {\prftree[r]{$\scriptstyle\supset\mathrm{E}$}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+ \end{displaymath}
+\end{verbatim}
+
+In general, the syntax of the \verb|\prftree| command is:
+\begin{displaymath}
+ \verb|\prftree|[\mbox{options}] \cdots
+ [\mbox{options}]\{\mbox{assumption}_1\} \cdots
+ \{\mbox{assumption}_n\}\{\mbox{conclusion}\}
+\end{displaymath}
+Assumptions are optional and there may be any number of them. Each
+assumption may contain a proof tree, which is typeset independently:
+the order allows to use indentation to help reading the source. The
+conclusion is mandatory, and it is supposed to be a
+formula.
+
+Assumptions and the conclusion are typeset in a display style math
+environment. Options control the way the proof is generated: in the
+example, the \verb|r| option has been used to signal that the first
+argument of \verb|\prftree| is the name of the inference rule.
+
+The available options are:
+\begin{itemize}
+\item\ [\textbf{r}], [\textbf{rule}], [\textbf{by rule}],
+ [\textbf{by}], [\textbf{right}]: the first argument after the
+ options is the rule name, which is typeset in text mode;
+\item\ [\textbf{l}], [\textbf{left}], [\textbf{label}]: the first
+ argument after the options is the label of the rule, which is
+ typeset in text mode. If a rule name is present, the first argument
+ is the rule name, and the second one is the label;
+\item\ [\textbf{straight}], [\textbf{straight line}],
+ [\textbf{straightline}]: makes the proof line solid;
+\item\ [\textbf{dotted}], [\textbf{dotted line}],
+ [\textbf{dottedline}]: makes the proof line dotted;
+\item\ [\textbf{dashed}], [\textbf{dashed line}],
+ [\textbf{dashedline}]: makes the proof line dashed;
+\item\ [\textbf{f}], [\textbf{fancy}], [\textbf{fancy line}],
+ [\textbf{fancyline}]: the proof line will be fancy;
+\item\ [\textbf{s}], [\textbf{single}], [\textbf{single line}],
+ [\textbf{singleline}]: makes the proof line single;
+\item\ [\textbf{d}], [\textbf{double}], [\textbf{double line}],
+ [\textbf{doubleline}]: makes the proof line double;
+\item\ [\textbf{noline}]: suppresses the proof line (prevails over all
+ other line options);
+\item\ [\textbf{summary}]: renders the proof line as the summary
+ symbol (prevails over all other line options except \textbf{noline}).
+\end{itemize}
+By default the proof line is straight and single. Options may be
+written in sequence, as in \verb|[r,f,d]|, which means that the proof
+tree will have a rule name, and the proof line will be fancy and
+double, or separately, as in \verb|[r][f][d]|, or even as a
+combination, like \verb|[r][f,d]|. Options are evaluated
+left-to-right, so \verb|[d,s]| is the same as \verb|[s]|, while
+\verb|[noline,straight,d]| is the same as \verb|[noline]|.
+
+The conjunction introduction rule illustrates the various line
+options:
+\begin{displaymath}
+ \begin{array}{lcc@{\qquad}l}
+ \mbox{default (single straight)} &
+ \prftree{A}{B}{A \wedge B} &
+ \prftree[r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[straight]} \\
+ \mbox{double straight} &
+ \prftree[d]{A}{B}{A \wedge B} &
+ \prftree[d,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[double,straight]} \\
+ \mbox{single dotted} &
+ \prftree[dotted]{A}{B}{A \wedge B} &
+ \prftree[dotted,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[dotted]} \\
+ \mbox{double dotted} &
+ \prftree[dotted,d]{A}{B}{A \wedge B} &
+ \prftree[dotted,d,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[double,dotted]} \\
+ \mbox{single dashed} &
+ \prftree[dashed]{A}{B}{A \wedge B} &
+ \prftree[dashed,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[dashed]} \\
+ \mbox{double dashed} &
+ \prftree[dashed,d]{A}{B}{A \wedge B} &
+ \prftree[dashed,d,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[double,dashed]} \\
+ \mbox{single fancy} &
+ \prftree[f]{A}{B}{A \wedge B} &
+ \prftree[f,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[fancy]} \\
+ \mbox{double fancy} &
+ \prftree[f,d]{A}{B}{A \wedge B} &
+ \prftree[f,d,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[double,fancy]} \\
+ \mbox{noline} &
+ \prftree[noline]{A}{B}{A \wedge B} &
+ \prftree[noline,r]{$\scriptstyle\wedge\mathrm{I}$}
+ {A}{B}{A \wedge B} &
+ \texttt{[noline]}
+ \end{array}
+\end{displaymath}
+These examples are implemented in an array whose cells have the form
+\begin{center}
+ \verb|\prftree[|\emph{option}\verb|]{A}{B}{A \wedge B} &|
+ \verb|\prftree[|\emph{option}\verb|,r]{$\scriptstyle\wedge\mathrm{I}$}|
+\end{center}
+in which the option part is the one on the right of the
+picture.\vspace{1ex}
+
+An assumption is a special proof tree, built by the command:
+\begin{displaymath}
+ \verb|\prfassumption|\{\text{formula}\}
+\end{displaymath}
+Similarly, a bounded assumption is produced by the command:
+\begin{displaymath}
+ \verb|\prfboundedassumption|\{\text{formula}\}
+\end{displaymath}
+as in the previous example.
+
+Although it is possible to type assumptions directly as argument of
+\verb|\prftree|, it is better to use the commands above: as explained
+later, since a proof tree is a box with an internal structure, the
+assumption commands take care of building this structure
+appropriately, while the direct typing does not, which may produce
+unexpected results.\vspace{2ex}
+
+Similarly, axioms are produced by the commands
+\begin{displaymath}
+ \verb|\prfaxiom|\{\mbox{axiom}\}
+\end{displaymath}
+and
+\begin{displaymath}
+ \verb|\prfbyaxiom|\{\mbox{name}\}\{\mbox{axiom}\}
+\end{displaymath}
+For example, the axiom stating that equality is reflexive, is
+\begin{displaymath}
+ \begin{array}{cc}
+ \prfaxiom{\forall x\, x = x} &
+ \prfbyaxiom{refl}{\forall x\, x = x}
+ \end{array}
+\end{displaymath}
+and they are generated by the \LaTeX{} code
+\begin{displaymath}
+ \begin{array}{l}
+ \verb|\prfaxiom{\forall x\, x = x}|\\
+ \verb|\prfbyaxiom{refl}{\forall x\, x = x}|
+ \end{array}
+\end{displaymath}\vspace{-.2ex}
+
+Finally, a proof summary is used to summarise a proof. The
+corresponding command is:
+\begin{displaymath}
+ \verb|\prfsummary|[\mbox{name}]\{\mbox{assumption}_1\} \cdots
+ \{\mbox{assumption}_n\}\{\mbox{conclusion}\}
+\end{displaymath}
+The name of the proof is optional, while the assumptions and the
+conclusion are treated as in \verb|\prftree|. When present, the proof
+name is typeset in text mode.
+
+For example, \verb|\prfsummary{\forall x\, x = x}| produces
+\begin{displaymath}
+ \prfsummary{\forall x\, x = x}
+\end{displaymath}
+while
+\verb|\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}|
+gives
+\begin{displaymath}
+ \prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}
+\end{displaymath}\vspace{-.2ex}
+
+In general, a proof tree is a \TeX{} box containing all the pieces of
+the tree, with strict bounds: for example,
+\begin{displaymath}
+ \fbox{\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}}
+\end{displaymath}
+
+% --------------------------
+\clearpage
+\section{Parameters}\label{sec:parameters}
+A number of parameters may be used to control the typesetting of proof
+trees. They may be changed globally or locally, following the usual
+scoping rules of \TeX{}. In this respect, remember that each
+assumption is typeset independently, so parameters may be changed on a
+sub-proof basis, as will be done in most examples.\vspace{2ex}
+
+There are various \TeX{} dimensions that influence how proofs are
+constructed:
+\begin{itemize}
+\item\ \verb|\prflinepadbefore| (default 0.3ex): the space between the
+ bottom line of assumptions and the proof line
+\item\ \verb|\prflinepadafter| (default 0.3ex): the space between the
+ proof line and the top of the conclusion;
+\item\ \verb|\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;
+\item\ \verb|\prflinethickness| (default 0.12ex): the thickness of the
+ proof line;
+\item\ \verb|\prfemptylinethickness| (default 4 times the line
+ thickness): in the rare case when the line is empty, but there are
+ assumptions, this is the distance between the assumptions and the
+ conclusion;
+\item\ \verb|\prfrulenameskip| (default 0.2em): the space between the
+ proof line and the rule name;
+\item\ \verb|\prflabelskip| (default 0.2em): the space between the
+ proof label and the proof line;
+\item\ \verb|\prfinterspace| (default .8em): the space between two
+ subsequent assumptions in the assumption list;
+\item\ \verb|\prfdoublelineinterspace| (default 0.06ex): the space
+ between the two lines of a double line.
+\end{itemize}
+
+For example,
+\begin{displaymath}
+ \prflinepadafter=0ex
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+is typeset by
+\begin{verbatim}
+ \prflinepadafter=0ex
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{verbatim}
+
+Similarly, \verb|\prflineextra=-.4em| and \verb|\prfrulenameskip=.8em|
+produce:
+\begin{displaymath}
+ {\prflineextra=-.4em
+ \prfrulenameskip=.8em
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}}
+\end{displaymath}
+
+Also, \verb|\prflinethickness=3pt| and
+\verb|\prfdoublelineinterspace=2pt| in the upper sub-proof generate:
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prflinethickness=3pt
+ \prfdoublelineinterspace=2pt
+ \prftree[r,d]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+The corresponding code is
+\begin{verbatim}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prflinethickness=3pt
+ \prfdoublelineinterspace=2pt
+ \prftree[r,d]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{verbatim}
+
+Line thickness does not affect dashed, dotted, and fancy lines, but
+interline space does: in the example,
+\verb|\prfdoublelineinterspace=4pt| on a fancy line produces
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prfdoublelineinterspace=4pt
+ \prftree[r,d,f]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}\vspace{.2ex}
+
+Fancy lines are drawn by the \verb|\prffancyline| command. This can be
+redefined: as a guideline, the package defines it as
+\begin{verbatim}
+ \def\prffancyline{\cleaders\hbox to .63em%
+ {\hss\raisebox{-.5ex}[.2ex][0pt]{$\sim$}\hss}\hfill}
+\end{verbatim}\vspace{2ex}
+
+Label spacing works exactly as rule name spacing. Actually, it is
+possible to have a proof with both a label and a rule name:
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prflabelskip=.7em
+ \prftree[r,l]{$\supset$I}
+ {[\textsl{$\bot\mathrm{E}$ will not work here!}]}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+which has been typeset by
+\begin{verbatim}
+ \prftree[r]{$\supset$I}
+ {\prflabelskip=.7em
+ \prftree[r,l]{$\supset$I}
+ {[\textsl{$\bot\mathrm{E}$ will not work here!}]}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{verbatim}\vspace{2ex}
+
+The \verb|\prfinterspace| controls the distance between
+assumptions. Specifically, this is the space between the \emph{boxes}
+containing two assumptions.
+
+Consider the following example
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}
+Although the assumptions in the top line are well spaced, the two
+sub-proofs on the top are too close. This can be corrected in two
+different ways: by putting an explicit space, via \verb|\hspace|, in
+front of the second sub-proof, or after the first
+sub-proof---remember, they are just boxes
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}\hspace{1.5em}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}
+otherwise, putting $\verb|\prfinterspace|=1.5\mathrm{em}$ before the
+sub-proof whose conclusion is $C$, one obtains the more pleasant
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prfinterspace=1.5em
+ \prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}\vspace{.2ex}
+
+The \verb|Strut| option of the package controls a subtle point about
+spacing around a proof line: assumptions and conclusion are usually
+typeset so that the height and the depth of their box is at least the
+one of \verb|\mathstrut|. In this way, adjacent proofs will have their
+proof lines aligned (well, whenever they don't have huge
+conclusions). But, as signalled by Dominic Hughes, sometimes one wants
+the height and the depth to be the ``real'' ones, especially when
+there are no characters/symbols with a positive depth: this forces the
+perceived space above and below the proof line to be exactly the
+values of \verb|\prflinepadbefore| and \verb|\prflinepadafter|. This
+behaviour can be achieved by calling the package with the \verb|STRUT|
+option. Alternatively, one may use the \verb|\prfSTRUToptionfalse|
+command to locally force this behaviour, and
+\verb|\prfSTRUToptiontrue| to return to the standard one. Similarly,
+the \verb|STRUTlabel| package option, together with the pair of
+commands \verb|\prfSTRUTlabeloptiontrue| and
+\verb|\prfSTRUTlabeloptionfalse|, operate on rule names and rule
+labels.\vspace{2ex}
+
+The rendering of bounded assumptions is modified by
+\verb|\prfboundedstyle|. When $\verb|\prfboundedstyle| = 0$, the
+format of the assumption is $[\mbox{formula}]$, which is the default
+behaviour; with $\verb|\prfboundedstyle| = 1$, the formula is
+cancelled by a horizontal line; with $\verb|\prfboundedstyle| > 1$,
+the custom \verb|\prfdiscargedassumption| command is invoked:
+\begin{displaymath}
+ \begin{array}{c@{\qquad}c@{\qquad}c}
+ \prfboundedassumption{A(x)} &
+ {\prfboundedstyle=1\prfboundedassumption{A(x)}} &
+ {\prfboundedstyle=2\prfboundedassumption{A(x)}}
+ \end{array}
+\end{displaymath}
+
+The \verb|\prfdiscargedassumption| can be freely redefined. The
+package provides a reference implementation:
+\begin{verbatim}
+ \def\prfdiscargedassumption#1{\left\langle{#1}\right\rangle}
+\end{verbatim}\vspace{2ex}
+
+Proof summaries are drawn according to \verb|\prfsummarystyle|. The
+default value is $0$, which produces a vertical dotted line. Setting
+$\verb|\prfsummarystyle| = 1$ produces a huge $\Pi$, while
+$\verb|\prfsummarystyle| = 2$ produces a $\prod$. The value $3$ uses a
+$\mathcal{D}$ as the derivation symbol. Values greater than $3$ force
+the summary to be rendered by the \verb|\prffancysummarybox| command.
+\begin{displaymath}
+ \begin{array}{@{}c@{\quad}c@{\qquad}c@{\qquad}c@{}}
+ \verb|\prfsummarystyle| = 0 &
+ {\prfsummary{\forall x.\, x = x}} &
+ {\prfsummary{B(x)}{A(x)}} &
+ {\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}} \\[2ex]
+ \verb|\prfsummarystyle| = 1 &
+ {\prfsummarystyle1\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle1\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle1\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge
+ C(x)}} \\[1ex]
+ \verb|\prfsummarystyle| = 2 &
+ {\prfsummarystyle2\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle2\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle2\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge
+ C(x)}} \\[1ex]
+ \verb|\prfsummarystyle| = 3 &
+ {\prfsummarystyle3\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle3\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle3\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}}
+ \\[1ex]
+ \verb|\prfsummarystyle| = 4 &
+ {\prfsummarystyle4\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle4\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle4\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}}
+ \end{array}
+\end{displaymath}
+
+The fancy summary box is composed by the \verb|\prffancysummarybox|
+command. This can be modified at will. The package defines it as
+\begin{verbatim}
+ \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}
+\end{verbatim}\vspace{2ex}
+
+The assumptions, conclusions, labels, and rule names are drawn using
+the following commands, which may be redefined:
+\begin{verbatim}
+\def\prfConclusionBox#1{%
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+\def\prfAssumptionBox#1{%
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
+\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
+\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
+\end{verbatim}
+It is not advisable to change these commands in a radical way, unless
+one understands how the graphical engine works.
+
+% -------------------------------------
+\clearpage
+\section{Labels and References}\label{sec:references}
+As discharged assumptions are often hard to track in a proof, the
+package provides a mechanism to label them and to reference them
+inside a proof tree. A reference is made up of three pieces: the
+\emph{label}, which is the name to denote the reference inside the
+text, the \emph{reference value}, which is the value denoted by the
+label, and the \emph{anchor}, which is the graphical rendering of the
+value aside the labelled point of the proof.
+
+For example,
+\begin{displaymath}
+ \begin{prfenv}
+ \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
+ {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption<assum:A>{A}}
+ {\prfboundedassumption<assum:not_A>{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+ \end{prfenv}
+\end{displaymath}
+is generated by the following code
+\begin{verbatim}
+ \begin{prfenv}
+ \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
+ {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption<assum:A>{A}}
+ {\prfboundedassumption<assum:not_A>{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+ \end{prfenv}
+\end{verbatim}
+The labels are \verb|assum:A| and \verb|assum:not_A|, the reference
+values are $1$ and $2$, respectively, and the anchors are these values
+on the discharged assumptions on the top of the proof. The references
+to these labels are the values in the rule names.\vspace{2ex}
+
+The \verb|prfenv| environment delimits the scope of labels: the
+\verb|\end{prfenv}| declaration makes the labels still available
+for reference, but numbering of new labels will restart from
+$1$. Enclosing a proof tree in a \verb|prfenv| environment is not
+mandatory: in such case, labels will be global to the
+document.\vspace{2ex}
+
+Sometimes, labels require two compilation steps to be correctly
+generated: in fact, as \LaTeX{} labels, forward references may be
+undefined in the first compilation step. The package issues a warning
+in this case, and display a \verb|??| for the invalid reference. Also,
+notice how the assumption reference mechanism is analogous to \LaTeX{}
+labels, but it is independent from it.\vspace{2ex}
+
+A reference to a label is made by the
+$\verb|\prfref|\langle\mathrm{label}\rangle$ command: its argument is
+a label, i.e., a string of text following the same rules as the
+argument of the \LaTeX{} \verb|\label| command. As in the \verb|\ref|
+command, the resulting value has no formatting.\vspace{2ex}
+
+A labelled assumption is generated by the following commands:
+\begin{displaymath}
+ \begin{array}{l}
+ \verb|\prfassumption|\langle[\mathrm{option}]\mathrm{label}\rangle
+ \{\mathrm{assumption}\}
+ \\
+ \verb|\prfboundedassumption|\langle[\mathrm{option}]
+ \mathrm{label}\rangle\{\mathrm{assumption}\}
+ \end{array}
+\end{displaymath}
+The first one acts as \verb|\prfassumption| but also declares the
+assumption label and decorates the assumption text with the
+anchor. The second one does the same on bounded assumptions.
+
+The generation of labels is controlled by the option value:
+\begin{itemize}
+\item \textbf{n}, \textbf{number}, \textbf{arabic}: generates a number
+ (default);
+\item \textbf{r}, \textbf{roman}: generates a lowercase roman number;
+\item \textbf{R}, \textbf{Roman}: generates an uppercase
+ roman number;
+\item \textbf{a}, \textbf{alph}, \textbf{alpha}, \textbf{alphabetic}:
+ produces a lowercase letter;
+\item \textbf{A}, \textbf{Alph}, \textbf{Alpha}, \textbf{Alphabetic}:
+ produces an uppercase letter;
+\item \textbf{f}, \textbf{s}, \textbf{function}, \textbf{symbol},
+ \textbf{function symbol}: produces a footnote symbol, as in
+ Section~C.8.4 of Lamport's, \textit{\LaTeX: A document preparation
+ system};
+\item \textbf{l}, \textbf{label}: tells that the label has not to be
+ defined. This is used to generate a labelled assumption sharing the
+ label with another one, which declares the value and the format.
+\end{itemize}
+
+Except for \textbf{l} and \textbf{label}, all the options are used to
+format the anchor following the standard \LaTeX{} way available for
+counters. No multiple options are allowed.
+
+For example, the disjunction elimination rule is a perfect way to
+illustrate the reason behind the \textbf{label} option, i.e., the need
+to discharge a pair of assumptions:
+\begin{displaymath}
+ \begin{prfenv}
+ \prfinterspace=1.2em
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:orE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orE>{B}}{C}}{C}
+ \end{prfenv}
+\end{displaymath}
+\begin{verbatim}
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:orE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orE>{B}}{C}}{C}
+\end{verbatim}
+
+If a label is declared more than once, a warning is issued when the
+\textbf{label} option is not used: although this is not a mistake, it
+may indicate that a label is reused when it should not.
+
+The same example can be used to show how the other options work:
+\begin{displaymath}
+ \renewcommand{\arraystretch}{6}
+ \begin{array}{@{}ccc@{}}
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[n]assum:orEn>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEn>{B}}{C}}
+ {C}
+ \end{prfenv} &
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[r]assum:orEr>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEr>{B}}{C}}
+ {C}
+ \end{prfenv} &
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[R]assum:orER>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orER>{B}}{C}}
+ {C}
+ \end{prfenv} \\
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[a]assum:orEa>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEa>{B}}{C}}
+ {C}
+ \end{prfenv} &
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[A]assum:orEA>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEA>{B}}{C}}
+ {C}
+ \end{prfenv} &
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[f]assum:orEf>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEf>{B}}{C}}
+ {C}
+ \end{prfenv}
+ \end{array}
+\end{displaymath}
+
+Also, as the \verb|\prfboundedstyle| varies, the resulting proof trees
+are:
+\begin{displaymath}
+ \begin{array}{ccc}
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfboundedstyle=0
+ \prfsummarystyle=4
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:AorE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:AorE>{B}}{C}}
+ {C}
+ \end{prfenv} &
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfboundedstyle=1
+ \prfsummarystyle=4
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:BorE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:BorE>{B}}{C}}
+ {C}
+ \end{prfenv} &
+ \begin{prfenv}
+ \prfinterspace=.6em
+ \prfboundedstyle=2
+ \prfsummarystyle=4
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:CorE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:CorE>{B}}{C}}
+ {C}
+ \end{prfenv}
+ \end{array}
+\end{displaymath}
+
+The \verb|prfassumptioncounter| is the \LaTeX{} counter used to
+generate the assumption values. It contains the last used value, and
+initially, it is set to $0$. By modifying its value, e.g., to
+\verb|\setcounter{prfassumptioncounter}{1}|,
+\begin{displaymath}
+ \begin{prfenv}
+ \setcounter{prfassumptioncounter}{1}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEff>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[f]assum:orEff>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEff>{B}}{C}}
+ {C}
+ \end{prfenv}
+\end{displaymath}
+
+A labelled assumption box is graphically constructed by the package
+command \verb|\prflabelledassumptionbox| which can be redefined if
+needed. It takes two arguments: the assumption and the anchor. Its
+standard definition is
+\begin{verbatim}
+ \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}}
+\end{verbatim}
+
+Moreover, also a labelled and bounded assumption is graphically
+rendered by the same command. There is just one exception: when
+$\verb|\prfboundedstyle| > 1$. In fact, since that style is
+controlled by a command that can be redefined, the same must hold for
+references in that style. The command which is called in this case is
+\verb|\prflabelleddiscargedassumption| which can be redefined if
+needed; its standard definition in the package is
+\begin{verbatim}
+ \def\prflabelleddiscargedassumption#1#2{%
+ \prflabelledassumptionbox{\left\langle{#1}\right\rangle}{#2}}
+\end{verbatim}\vspace{2ex}
+
+Also proof summaries can be labelled and referenced. The syntax
+extends the \verb|\prfsummary| command:
+\begin{displaymath}
+ \verb|\prfsummary|\langle[\mathrm{option}]\mathrm{label}\rangle
+ [\mathrm{name}]\{\mathrm{assumption}1\} \cdots
+ \{\mathrm{assumption}_n\}\{\mathrm{conclusion}\}
+\end{displaymath}
+The reference argument works in the same way as the corresponding one
+for assumptions, and the options are the same.
+
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \begin{array}{c@{\qquad}c@{\qquad}c@{\qquad}c@{\qquad}c}
+ {\prfsummarystyle=0
+ \prfsummary<proof:a0>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<proof:a1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=2
+ \prfsummary<proof:a2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=3
+ \prfsummary<proof:a3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=4
+ \prfsummary<proof:a4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{displaymath}
+
+These examples have been generated by the following code snippet:
+\begin{verbatim}
+ {\prfsummarystyle=X
+ \prfsummary<proof:aX>{A}{B}{A \wedge B}}
+\end{verbatim}
+
+The \verb|[option]| part of the label specification is optional, and
+it works exactly as the option field of labelled assumptions. This is
+best illustrated by an example:
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \begin{array}{cccc}
+ {\prfsummarystyle=1
+ \prfsummary<[r]proof:b1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[R]proof:b2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[f]proof:b3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[a]proof:b4>{A}{B}{A \wedge B}} \\ &
+ {\prfsummarystyle=1
+ \prfsummary<[A]proof:b5>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ \end{array}
+\end{displaymath}
+
+These examples have been generated by the following code snippet:
+\begin{verbatim}
+ {\prfsummarystyle=1
+ \prfsummary<[r]proof:bX>{A}{B}{A \wedge B}}
+\end{verbatim}
+and the last line uses the \verb|label| option.\vspace{2ex}
+
+The value of the summary labelling is controlled by the
+\verb|prfsummarycounter| counter, which is initially $0$ and contains
+the last used value.
+
+% -------------------------------------
+\clearpage
+\section{Simplified Commands}\label{sec:simplified_commands}
+The basic commands illustrated so far allow to control proof trees in
+all aspects, but they tend to be verbose in practise. Thus, a number
+of abbreviations are provided to make handier the writing of proofs.
+Since they may collide with other packages, these macros are activated
+by suitable options. Multiple options can be used at the same time.
+
+\subsection{Natural deduction}
+By loading the package with the \verb|ND| option, the following
+abbreviations are available, which correspond to the inference rules
+of natural deduction calculi:
+\begin{itemize}
+\item \verb|\NDA|: assumption;
+\item \verb|\NDAL|: labelled assumption;
+\item \verb|\NDD|: discharged assumption;
+\item \verb|\NDDL|: labelled discharged assumption;
+\item \verb|\NDP|: generic proof tree;
+\item \verb|\NDAX|: a generic axiom rule;
+ \begin{displaymath}
+ \vcenter{\NDAX{x = x}}\enspace;
+ \end{displaymath}
+\item \verb|\NDANDI|: conjunction introduction
+ \begin{displaymath}
+ \vcenter{\NDANDI{\NDA{A}}{\NDA{B}}{A \wedge B}}\enspace;
+ \end{displaymath}
+\item \verb|\NDANDER|, \verb|\NDANDEL|, \verb|\NDANDE|: conjunction
+ elimination right, left, and unspecified, respectively
+ \begin{displaymath}
+ \vcenter{\NDANDEL{\NDA{A \wedge B}}{\NDA{A}}} \quad
+ \vcenter{\NDANDER{\NDA{A \wedge B}}{\NDA{B}}}\enspace;
+ \end{displaymath}
+\item \verb|\NDORIR|, \verb|\NDORIL|, \verb|\NDORI|: disjunction
+ introduction right, left, and unspecified, respectively
+ \begin{displaymath}
+ \vcenter{\NDORIL{\NDA{A}}{\NDA{A \vee B}}} \quad
+ \vcenter{\NDORIR{\NDA{B}}{\NDA{A \vee B}}}\enspace;
+ \end{displaymath}
+\item \verb|\NDOREL|, \verb|\NDORE|: disjunction elimination, possibly
+ labelled
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDOREL{ndorel:1}{\NDA{A \vee B}}
+ {\prfsummary{\NDDL{ndorel:1}{A}}{C}}
+ {\prfsummary{\NDDL{[l]ndorel:1}{B}}{C}}{C}} \quad
+ \vcenter{\NDORE{\NDA{A \vee B}}{\prfsummary{\NDA{A}}{C}}
+ {\prfsummary{\NDA{B}}{C}}{C}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDIMPIL|, \verb|\NDIMPI|: implication introduction,
+ possibly labelled
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDIMPIL{ndimpil:1}
+ {\prfsummary{\NDDL{ndimpil:1}{A}}{B}}
+ {A \rightarrow B}} \quad
+ \vcenter{\NDIMPI{\prfsummary{\NDA{A}}{B}}{A \rightarrow B}}
+ \enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDIMPE|: implication elimination
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDIMPE{\NDA{A \rightarrow B}}{\NDA{A}}{B}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDNOTIL|, \verb|\NDNOTI|: negation introduction, possibly
+ labelled
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDNOTIL{ndnotil:1}
+ {\prfsummary{\NDDL{ndnotil:1}{A}}{\bot}}{\neg A}}\quad
+ \vcenter{\NDNOTI{\prfsummary{\NDA{A}}{\bot}}{\neg A}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDNOTE|: negation elimination
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDNOTE{\NDA{\neg A}}{\NDA{A}}{\bot}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDALLI|: universal quantifier introduction
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDALLI{\NDA{A}}{\forall x.\, A}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDALLE|: universal quantifier elimination
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDALLE{\NDA{\forall x.\, A}}{A[t/x]}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDEXI|: existential quantifier introduction
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDEXI{\NDA{A[t/x]}}{\exists x.\, A}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDEXEL|, \verb|\NDEXE|: existential quantifier
+ elimination, possibly labelled
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDEXEL{ndexel:1}{\NDA{\exists x.\, A}}
+ {\prfsummary{\NDDL{ndexel:1}{A}}{B}}{B}}\quad
+ \vcenter{\NDEXE{\NDA{\exists x.\, A}}
+ {\prfsummary{\NDA{A}}{B}}{B}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDTI|: truth introduction
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDTI{\top}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDFE|: falsity elimination
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDFE{\NDA{\bot}}{A}}\enspace;
+ \end{prfenv}
+ \end{displaymath}
+\item \verb|\NDLEM|: law of Excluded Middle
+ \begin{displaymath}
+ \begin{prfenv}
+ \vcenter{\NDLEM{A \vee \neg A}}\enspace.
+ \end{prfenv}
+ \end{displaymath}
+\end{itemize}
+
+The labels, when present, are the first argument, the rest being the
+assumptions and, finally, the conclusion. The rules do not have a
+fixed format, so extensions are allowed, e.g., on conjunction
+elimination or disjunction introduction.
+
+For example, the proof
+\begin{displaymath}
+ \begin{prfenv}
+ \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{simp:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{simp:notnotA}{\neg\neg A}}
+ {\NDDL{simp:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prfenv}
+\end{displaymath}
+is typeset in abbreviated form by the following code
+\begin{verbatim}
+ \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{simp:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{simp:notnotA}{\neg\neg A}}
+ {\NDDL{simp:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}\vspace{2ex}
+
+\subsection{Sequents}
+Similarly, by loading the package with the \verb|SEQ| option, the
+following abbreviations are available, which roughly correspond to the
+inference rule of sequent calculi:
+\begin{itemize}
+\item \verb|\SEQA|: assumption;
+\item \verb|\SEQD|: bounded assumption (not normally used, but handy
+ to have in case of fancy calculi);
+\item \verb|\SEQP|: generic proof;
+\item \verb|\SEQAX|: axiom rule
+ \begin{displaymath}
+ \vcenter{\SEQAX{A \Rightarrow A}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLF|: left falsity
+ \begin{displaymath}
+ \vcenter{\SEQLF{\bot \Rightarrow {}}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLW|, \verb|\SEQRW|: left and right weakening
+ \begin{displaymath}
+ \vcenter{\SEQLW{\Gamma \Rightarrow \Delta}{A, \Gamma \Rightarrow
+ \Delta}}\quad
+ \vcenter{\SEQLW{\Gamma \Rightarrow \Delta}{\Gamma \Rightarrow
+ \Delta, A}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLC|, \verb|\SEQRC|: left and right contraction
+ \begin{displaymath}
+ \vcenter{\SEQLC{A, A, \Gamma \Rightarrow \Delta}{A, \Gamma
+ \Rightarrow \Delta}}\quad
+ \vcenter{\SEQRC{\Gamma \Rightarrow \Delta, A, A}{\Gamma
+ \Rightarrow \Delta, A}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLAND|, \verb|\SEQLANDL|, \verb|\SEQLANDR|: left
+ conjunction; the \verb|L| and \verb|R| variants specify which side
+ of the conjunction is introduced
+ \begin{displaymath}
+ \vcenter{\SEQLANDL{A, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma
+ \Rightarrow \Delta}}\quad
+ \vcenter{\SEQLANDR{B, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma
+ \Rightarrow \Delta}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQRAND|: right conjunction
+ \begin{displaymath}
+ \vcenter{\SEQRAND{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow
+ \Delta, B}{\Gamma \Rightarrow \Delta, A \wedge B}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLOR|: left disjunction
+ \begin{displaymath}
+ \vcenter{\SEQLOR{A, \Gamma \Rightarrow \Delta}{B, \Gamma
+ \Rightarrow \Delta}{A \vee B, \Gamma \Rightarrow
+ \Delta}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQROR|, \verb|\SEQRORL|, \verb|\SEQRORR|: right
+ disjunction; the \verb|R| and \verb|L| variants specify which side
+ of the disjunction is introduced
+ \begin{displaymath}
+ \vcenter{\SEQRORL{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow
+ \Delta, A \vee B}}\quad
+ \vcenter{\SEQRORR{\Gamma \Rightarrow \Delta, B}{\Gamma \Rightarrow
+ \Delta, A \vee B}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLIMP|: left implication
+ \begin{displaymath}
+ \vcenter{\SEQLIMP{\Gamma \Rightarrow \Delta, A}{B, \Gamma
+ \Rightarrow \Delta}{A \rightarrow B, \Gamma \Rightarrow
+ \Delta}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQRIMP|: right implication
+ \begin{displaymath}
+ \vcenter{\SEQRIMP{A, \Gamma \Rightarrow \Delta, B}{\Gamma
+ \Rightarrow, \Delta, A \rightarrow B}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLALL|: left universal quantification
+ \begin{displaymath}
+ \vcenter{\SEQLALL{A[t/x], \Gamma \Rightarrow \Delta}{\forall x.\,
+ A, \Gamma \Rightarrow \Delta}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQRALL|: right universal quantification
+ \begin{displaymath}
+ \vcenter{\SEQRALL{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow
+ \Delta, \forall x.\, A}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQLEX|: left existential quantification
+ \begin{displaymath}
+ \vcenter{\SEQLEX{A, \Gamma \Rightarrow \Delta}{\exists x.\, A,
+ \Gamma \Rightarrow \Delta}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQREX|: right existential quantification
+ \begin{displaymath}
+ \vcenter{\SEQREX{\Gamma \Rightarrow \Delta, A[t/x]}{\Gamma
+ \Rightarrow \Delta, \exists x.\, A}}\enspace;
+ \end{displaymath}
+\item \verb|\SEQCUT|: cut rule
+ \begin{displaymath}
+ \vcenter{\SEQCUT{\Gamma \Rightarrow \Delta, A}{A, \Gamma'
+ \Rightarrow \Delta'}{\Gamma \Gamma' \Rightarrow \Delta
+ \Delta'}}\enspace.
+ \end{displaymath}
+\end{itemize}
+
+\subsection{Equality}
+Invoking the \verb|EQ| option defines the following inference rules:
+\begin{itemize}
+\item \verb|\EQREFL|: reflexivity
+ \begin{displaymath}
+ \vcenter{\EQREFL{t = t}}\enspace;
+ \end{displaymath}
+\item \verb|\EQSYM|: symmetry
+ \begin{displaymath}
+ \vcenter{\EQSYM{t = s}{s = t}}\enspace;
+ \end{displaymath}
+\item \verb|\EQTRANS|: transitivity
+ \begin{displaymath}
+ \vcenter{\EQTRANS{t = s}{s = r}{t = r}}\enspace;
+ \end{displaymath}
+\item \verb|\EQSUBST|: the substitution rule
+ \begin{displaymath}
+ \vcenter{\EQSUBST{t = s}{A[t/x]}{A[s/x]}}\enspace.
+ \end{displaymath}
+\end{itemize}
+
+\subsection{Implication}
+Since the implication symbol is usually represented either as
+$\rightarrow$ or as $\supset$, the package allows to choose which
+representation to use. By default, implication is $\rightarrow$, but
+loading the package with the \verb|[IMP]| option switches to
+$\supset$. The same effect is obtained by the commands
+\verb|\prfIMPOptiontrue| (implication is $\supset$) and
+\verb|prfIMPOptionfalse| (implication is $\rightarrow$).
+
+\subsection{Martin-L{\"o}f Type Theory and Homotopy Type Theory}
+Invoking the package with the \verb|ML| option enables the support for
+these type theories. This part is derived from Roberta Bonacina's PhD
+dissertation, which used this package in an essential way to develop
+proof trees in Homotopy Type Theory.
+
+Enabling the option \verb|ML| defines a number of symbols which are
+useful to have. However, since they may conflict with other packages,
+they can be disabled invoking the option \verb|MLnodef|. These
+operators are
+\begin{itemize}
+\item \verb|\type|: the symbol $\type$ correctly spaced as a
+ mathematical binary operation;
+\item \verb|\universe|: the symbol for universes;
+\item \verb|\judgementaldef| and \verb|\propositionaldef|: the symbols
+ $\judgementaldef$ and $\propositionaldef$ spaced as mathematical
+ binary operations;
+\item \verb|\emptytype| ($\emptytype$), \verb|\unittype|
+ ($\unittype$), \verb|\booleantype| ($\booleantype$): these symbols
+ are ordinary operators typeset in mathematical boldface font;
+\item \verb|\context| ($\context$), \verb|\identitytype|
+ ($\identitytype$), \verb|\refl| ($\refl$), \verb|\axiomofchoice|
+ ($\axiomofchoice$), \verb|\accessibility| ($\accessibility$),
+ \verb|\ap| ($\ap$), \verb|\apd| ($\apd$), \verb|\basepoint|
+ ($\basepoint$), \verb|\biinv| ($\biinv$), \verb|\cardtype|
+ ($\cardtype$), \verb|\cocone| ($\cocone$), \verb|\cons| ($\cons$),
+ \verb|\contr| ($\contr$), \verb|\equivtype| ($\equivtype$),
+ \verb|\ext| ($\ext$), \verb|\fiber| ($\fiber$), \verb|\funext|
+ ($\funext$), \verb|\glue| ($\glue$), \verb|\happly| ($\happly$),
+ \verb|\hom| ($\hom$), \verb|\id| ($\id$), \verb|\idtoeqv|
+ ($\idtoeqv$), \verb|\im| ($\im$), \verb|\idtoiso| ($\idtoiso$),
+ \verb|\ind| ($\ind$), \verb|\inj| ($\inj$), \verb|\inl| ($\inl$),
+ \verb|\inr| ($\inr$), \verb|\iscontr| ($\iscontr$), \verb|\isequiv|
+ ($\isequiv$), \verb|\ishae| ($\ishae$), \verb|\isotoid|
+ ($\isotoid$), \verb|\isprop| ($\isprop$), \verb|\isset| ($\isset$),
+ \verb|\ker| ($\ker$), \verb|\LEM| ($\LEM$), \verb|\linv| ($\linv$),
+ \verb|\listtype| ($\listtype$), \verb|\loopcons| ($\loopcons$),
+ \verb|\Map| ($\Map$), \verb|\merid| ($\merid$), \verb|\nil|
+ ($\nil$), \verb|\ordtype| ($\ordtype$), \verb|\pair| ($\pair$),
+ \verb|\pred| ($\pred$), \verb|\pr| ($\pr$), \verb|\Prop| ($\Prop$),
+ \verb|\qinv| ($\qinv$), \verb|\rec| ($\rec$), \verb|\rinv|
+ ($\rinv$), \verb|\seg| ($\seg$), \verb|\Set| ($\Set$), \verb|\Succ|
+ ($\Succ$), \verb|\sup| ($\sup$), \verb|\total| ($\total$),
+ \verb|\transport| ($\transport$), \verb|\ua| ($\ua$), \verb|\Wtype|
+ ($\Wtype$), \verb|\transportconst| ($\transportconst$): these
+ symbols are ordinary operators, typeset in the mathematical
+ sans-serif font; their graphical appearance is in brackets.
+\end{itemize}
+
+The large number of inference rules is listed below: they cover the
+structural part of the theories, plus most of the usual inductive
+types, comprehending also some higher-order inductive types. To each
+rule is associated a rule name, which is available as a command: the
+convention is that the rule name is obtained appending \verb|rule| to
+the name of the inference rule. In general, the command to typeset a
+rule conforms to the standard name in the book \emph{Homotopy Type
+ Theory}. The name as typeset, is shown in brackets:
+\begin{itemize}
+\item \verb|\MLctxEMP| $(\scriptstyle\MLctxEMPrule)$,\\ \verb|\MLctxEXT|
+ $(\scriptstyle\MLctxEXTrule)$: context manipulation;
+\item \verb|\MLVble| $(\scriptstyle\MLVblerule)$: variable
+ introduction;
+\item \verb|\MLSubst| $(\scriptstyle\MLSubstrule)$,
+ \verb|\MLWkg|
+ $(\scriptstyle\MLWkgrule)$: substitution and weakening;
+\item \verb|\MLEQrefl| $(\scriptstyle\MLEQreflrule)$,
+ \verb|\MLEQsym| $(\scriptstyle\MLEQsymrule)$,
+ \verb|\MLEQtrans| $(\scriptstyle\MLEQtransrule)$, \\
+ \verb|\MLEQsubst| $(\scriptstyle\MLEQsubstrule)$,
+ \verb|\MLEQsubsteq| $(\scriptstyle\MLEQsubsteqrule)$: structural
+ rules about judgemental equality;
+\item \verb|\MLUintro| $(\scriptstyle\MLUintrorule)$,
+ \verb|\MLUcumul| $(\scriptstyle\MLUcumulrule)$,
+ \verb|\MLUcumuleq| $(\scriptstyle\MLUcumuleqrule)$: type universe;
+\item \verb|\MLpiform| $(\scriptstyle\MLpiformrule)$,
+ \verb|\MLpiformeq| $(\scriptstyle\MLpiformeqrule)$, \\
+ \verb|\MLpiintro| $(\scriptstyle\MLpiintrorule)$,
+ \verb|\MLpiintroeq| $(\scriptstyle\MLpiintroeqrule)$, \\
+ \verb|\MLpielim| $(\scriptstyle\MLpielimrule)$,
+ \verb|\MLpielimeq| $(\scriptstyle\MLpielimeqrule)$, \\
+ \verb|\MLpicomp| $(\scriptstyle\MLpicomprule)$,
+ \verb|\MLpiuniq| $(\scriptstyle\MLpiuniqrule)$: dependent function
+ types;
+\item \verb|\MLKintro| $(\scriptstyle\MLKintrorule)$: generic rule for
+ constant introduction;
+\item \verb|\MLsigmaform| $(\scriptstyle\MLsigmaformrule)$,
+ \verb|\MLsigmaintro| $(\scriptstyle\MLsigmaintrorule)$,
+ \verb|\MLsigmaelim| $(\scriptstyle\MLsigmaelimrule)$, \\
+ \verb|\MLsigmacomp| $(\scriptstyle\MLsigmacomprule)$,
+ \verb|\MLsigmauniq| $(\scriptstyle\MLsigmauniqrule)$: dependent pair
+ types;
+\item \verb|\MLplusform| $(\scriptstyle\MLplusformrule)$,
+ \verb|\MLplusintrol| $(\scriptstyle\MLplusintrolrule)$,
+ \verb|\MLplusintror| $(\scriptstyle\MLplusintrorrule)$, \\
+ \verb|\MLpluselim| $(\scriptstyle\MLpluselimrule)$,
+ \verb|\MLpluscompl| $(\scriptstyle\MLpluscomplrule)$,
+ \verb|\MLpluscompr| $(\scriptstyle\MLpluscomprrule)$, \\
+ \verb|\MLplusuniq| $(\scriptstyle\MLplusuniqrule)$: coproduct types;
+\item \verb|\MLzeroform| $(\scriptstyle\MLzeroformrule)$,
+ \verb|\MLzeroelim| $(\scriptstyle\MLzeroelimrule)$,
+ \verb|\MLzerouniq| $(\scriptstyle\MLzerouniqrule)$: the empty type;
+\item \verb|\MLunitform| $(\scriptstyle\MLunitformrule)$,
+ \verb|\MLunitintro| $(\scriptstyle\MLunitintrorule)$,
+ \verb|\MLunitelim| $(\scriptstyle\MLunitelimrule)$, \\
+ \verb|\MLunitcomp| $(\scriptstyle\MLunitcomprule)$,
+ \verb|\MLunituniq| $(\scriptstyle\MLunituniqrule)$: the unit type;
+\item \verb|\MLnatform| $(\scriptstyle\MLnatformrule)$,
+ \verb|\MLnatintrozero| $(\scriptstyle\MLnatintrozerorule)$, \\
+ \verb|\MLnatintrosucc| $(\scriptstyle\MLnatintrosuccrule)$,
+ \verb|\MLnatelim| $(\scriptstyle\MLnatelimrule)$, \\
+ \verb|\MLnatcompzero| $(\scriptstyle\MLnatcompzerorule)$,
+ \verb|\MLnatcompsucc| $(\scriptstyle\MLnatcompsuccrule)$, \\
+ \verb|\MLnatuniq| $(\scriptstyle\MLnatuniqrule)$: the natural number
+ type;
+\item \verb|\MLidform| $(\scriptstyle\MLidformrule)$,
+ \verb|\MLidintro| $(\scriptstyle\MLidintrorule)$,
+ \verb|\MLidelim| $(\scriptstyle\MLidelimrule)$, \\
+ \verb|\MLidcomp| $(\scriptstyle\MLidcomprule)$,
+ \verb|\MLiduniq| $(\scriptstyle\MLiduniqrule)$: identity types;
+\item \verb|\MLwform| $(\scriptstyle\MLwformrule)$,
+ \verb|\MLwintro| $(\scriptstyle\MLwintrorule)$,
+ \verb|\MLwelim| $(\scriptstyle\MLwelimrule)$, \\
+ \verb|\MLwcomp| $(\scriptstyle\MLwcomprule)$,
+ \verb|\MLwuniq| $(\scriptstyle\MLwuniqrule)$: $\mathsf{W}$ types;
+\item \verb|\MLListform| $(\scriptstyle\MLListformrule)$,
+ \verb|\MLListintron| $(\scriptstyle\MLListintronrule)$,\\
+ \verb|\MLListintroc| $(\scriptstyle\MLListintrocrule)$,
+ \verb|\MLListelim| $(\scriptstyle\MLListelimrule)$,\\
+ \verb|\MLListcompn| $(\scriptstyle\MLListcompnrule)$,
+ \verb|\MLListcompc| $(\scriptstyle\MLListcompcrule)$,\\
+ \verb|\MLListuniq| $(\scriptstyle\MLListuniqrule)$:
+ $\mathsf{List}$ types;
+\item \verb|\MLfunext| $(\scriptstyle\MLfunextrule)$: function extensionality;
+\item \verb|\MLuniv| $(\scriptstyle\MLunivrule)$: univalence;
+\item \verb|\MLSform| $(\scriptstyle\MLSformrule)$,
+ \verb|\MLSintro| $(\scriptstyle\MLSintrorule)$,
+ \verb|\MLSelim| $(\scriptstyle\MLSelimrule)$,\\
+ \verb|\MLScomp| $(\scriptstyle\MLScomprule)$,
+ \verb|\MLSuniq| $(\scriptstyle\MLSuniqrule)$,
+ \verb|\MLSpeqintro| $(\scriptstyle\MLSpeqintrorule)$,\\
+ \verb|\MLSpeqcomp| $(\scriptstyle\MLSpeqcomprule)$: the
+ $\mathbb{S}^1$ circle type;
+\item \verb|\MLIform| $(\scriptstyle\MLIformrule)$,
+ \verb|\MLIintroa| $(\scriptstyle\MLIintroarule)$,
+ \verb|\MLIintrob| $(\scriptstyle\MLIintrobrule)$, \\
+ \verb|\MLIelim| $(\scriptstyle\MLIelimrule)$,
+ \verb|\MLIcompa| $(\scriptstyle\MLIcomparule)$,
+ \verb|\MLIcompb| $(\scriptstyle\MLIcompbrule)$, \\
+ \verb|\MLIuniq| $(\scriptstyle\MLIuniqrule)$,
+ \verb|\MLIpeqintro| $(\scriptstyle\MLIpeqintrorule)$,
+ \verb|\MLIpeqcomp| $(\scriptstyle\MLIpeqcomprule)$: the interval
+ type;
+\item \verb|\MLsigmaintroa| $(\scriptstyle\MLsigmaintroarule)$,
+ \verb|\MLsigmaintrob| $(\scriptstyle\MLsigmaintrobrule)$, \\
+ \verb|\MLsigmacompa| $(\scriptstyle\MLsigmacomparule)$,
+ \verb|\MLsigmacompb| $(\scriptstyle\MLsigmacompbrule)$, \\
+ \verb|\MLsigmapeqintro| $(\scriptstyle\MLsigmapeqintrorule)$,
+ \verb|\MLsigmapeqcomp| $(\scriptstyle\MLsigmapeqcomprule)$:
+ suspensions;
+\item \verb|\MLPOform| $(\scriptstyle\MLPOformrule)$,
+ \verb|\MLPOintroa| $(\scriptstyle\MLPOintroarule)$,
+ \verb|\MLPOintrob| $(\scriptstyle\MLPOintrobrule)$, \\
+ \verb|\MLPOelim| $(\scriptstyle\MLPOelimrule)$,
+ \verb|\MLPOcompa| $(\scriptstyle\MLPOcomparule)$,
+ \verb|\MLPOcompb| $(\scriptstyle\MLPOcompbrule)$, \\
+ \verb|\MLPOuniq| $(\scriptstyle\MLPOuniqrule)$,
+ \verb|\MLPOpeqintro| $(\scriptstyle\MLPOpeqintrorule)$,
+ \verb|\MLPOpeqcomp| $(\scriptstyle\MLPOpeqcomprule)$: pushouts;
+\item \verb|\MLTform| $(\scriptstyle\MLTformrule)$,
+ \verb|\MLTintro| $(\scriptstyle\MLTintrorule)$,
+ \verb|\MLTelim| $(\scriptstyle\MLTelimrule)$, \\
+ \verb|\MLTcomp| $(\scriptstyle\MLTcomprule)$,
+ \verb|\MLTuniq| $(\scriptstyle\MLTuniqrule)$,
+ \verb|\MLTpeqintro| $(\scriptstyle\MLTpeqintrorule)$, \\
+ \verb|\MLTpeqcomp| $(\scriptstyle\MLTpeqcomprule)$: truncations;
+\item \verb|\MLtorusform| $(\scriptstyle\MLtorusformrule)$,
+ \verb|\MLtorusintro| $(\scriptstyle\MLtorusintrorule)$,
+ \verb|\MLtoruselim| $(\scriptstyle\MLtoruselimrule)$,\\
+ \verb|\MLtoruscomp| $(\scriptstyle\MLtoruscomprule)$,
+ \verb|\MLtoruspeqintroa| $(\scriptstyle\MLtoruspeqintroarule)$, \\
+ \verb|\MLtoruspeqintrob| $(\scriptstyle\MLtoruspeqintrobrule)$,
+ \verb|\MLtoruspeqintroc| $(\scriptstyle\MLtoruspeqintrocrule)$, \\
+ \verb|\MLtoruspeqcompa| $(\scriptstyle\MLtoruspeqcomparule)$,
+ \verb|\MLtoruspeqcompb| $(\scriptstyle\MLtoruspeqcompbrule)$, \\
+ \verb|\MLtoruspeqcompc| $(\scriptstyle\MLtoruspeqcompcrule)$:
+ the torus type.
+\end{itemize}
+
+\subsection{Defining new inference rules}
+Of course, the reader is encouraged to develop her own abbreviations
+starting from the provided ones. To this aim two commands are
+provided. They share the same syntax: \verb|\prfMakeInferenceRule| and
+\verb|\prfMakeInferenceRuleRef| take two arguments, the first one is
+the name of the command associated to the inference rule, and the
+second one is used to write the rule name. For example,
+\begin{center}
+ \verb|\prfMakeInferenceRule{NDANDI}{\mathord{\wedge}\textup{I}}|
+\end{center}
+is how the conjunction introduction rule is defined, and
+\begin{center}
+ \verb| \prfMakeInferenceRuleRef{NDOREL}{\mathord{\vee}\textup{E}}|
+\end{center}
+is how the disjunction elimination rule is defined. The rules
+generated by the \verb|Ref| variant use their first argument as the
+reference to the assumption(s) they discharge.
+
+\subsection{Stacking proofs and assumptions}
+Sometimes, a proof is too large to fit into the text width. Although
+some strategies could be implemented to compress it, see the next
+section, they fail in extreme cases. For example, the elimination rule
+for the circle in Homotopy type theories is:
+\begin{displaymath}
+ \MLScomp
+ {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+ {\Gamma \vdash b \type C[\basepoint/x]}
+ {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+ {\Gamma \vdash p \type \mathbb{S}^1}
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{displaymath}
+typeset by
+\begin{verbatim}
+ \MLScomp
+ {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+ {\Gamma \vdash b \type C[\basepoint/x]}
+ {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+ {\Gamma \vdash p \type \mathbb{S}^1}
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{verbatim}
+It is clear that on an A5 paper, there is not enough space to write it
+down. In these cases, the package provides a way to \emph{stack} the
+premises of a rule, obtaining
+\begin{displaymath}
+ \MLScomp
+ {\prfStackPremises
+ {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+ {\Gamma \vdash b \type C[\basepoint/x]} }
+ {\prfStackPremises
+ {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+ {\Gamma \vdash p \type \mathbb{S}^1} }
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{displaymath}
+The corresponding \LaTeX{} code is
+\begin{verbatim}
+ \MLScomp
+ {\prfStackPremises
+ {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+ {\Gamma \vdash b \type C[\basepoint/x]}
+ }
+ {\prfStackPremises
+ {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+ {\Gamma \vdash p \type \mathbb{S}^1}
+ }
+ {\Gamma \vdash
+ \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) \type C[p/x]}
+\end{verbatim}
+The command
+\verb|\prfStackPremises{|$a_1$\verb|}{|$\ldots$\verb|}{|$a_n$\verb|}|
+takes the arguments $a_1, \ldots, a_n$ and typeset them as a proof
+tree with no lines with $a_1$ on the top.
+
+Actually, stacking proofs is possible:
+\begin{displaymath}
+ \MLScomp
+ {\prfStackPremises
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+ \universe_i}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \basepoint \type \mathbb{S}^1}} }
+ {\prfStackPremises
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash p \type \mathbb{S}^1}} }
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{displaymath}
+has been typeset by
+\begin{verbatim}
+ \MLScomp
+ {\prfStackPremises
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+ \universe_i}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \basepoint \type \mathbb{S}^1}}
+ }
+ {\prfStackPremises
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash p \type \mathbb{S}^1}}
+ }
+ {\Gamma \vdash
+ \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) \type C[p/x]}
+\end{verbatim}
+
+Since a stack is a proof tree, the parameters could be locally changed
+to control its appearance. For example
+\begin{displaymath}
+ \MLScomp
+ {\prfemptylinethickness20\prflinethickness
+ \prfStackPremises
+ {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+ {\Gamma \vdash b \type C[\basepoint/x]} }
+ {\prfStackPremises
+ {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+ {\Gamma \vdash p \type \mathbb{S}^1} }
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{displaymath}
+makes the lines in the left stack far apart.
+\begin{verbatim}
+ \MLScomp
+ {\prfemptylinethickness20\prflinethickness
+ \prfStackPremises
+ {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i}
+ {\Gamma \vdash b \type C[\basepoint/x]} }
+ {\prfStackPremises
+ {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b}
+ {\Gamma \vdash p \type \mathbb{S}^1} }
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{verbatim}
+
+Spacing in stacks of proofs is normally difficult to control: if
+really sophisticated formatting is needed, it is better to consider
+the following option:
+\begin{displaymath}
+ \MLScomp
+ {\prfassumption{
+ \begin{array}{@{}c@{\quad}c@{}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+ \universe_i}} &
+ {\Gamma \vdash \ell \type \basepoint = \basepoint} \\
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \basepoint \type \mathbb{S}^1}} &
+ {\Gamma \vdash p \type \mathbb{S}^1}
+ \end{array}}}
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{displaymath}
+which uses the \verb|array| environment
+\begin{verbatim}
+ \MLScomp
+ {\prfassumption{
+ \begin{array}{@{}c@{\quad}c@{}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+ \universe_i}} &
+ {\Gamma \vdash \ell \type \basepoint = \basepoint} \\
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \basepoint \type \mathbb{S}^1}} &
+ {\Gamma \vdash p \type \mathbb{S}^1}
+ \end{array}}}
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{verbatim}
+or similar ones, using the multitude of packages to format tables. By
+the way, the obvious solution using stacks is
+\begin{displaymath}
+ \MLScomp
+ {\prfStackPremises
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+ \universe_i}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \basepoint \type \mathbb{S}^1}} }
+ {\prfStackPremises
+ {\prfassumption
+ {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+ {\prfassumption
+ {\Gamma \vdash p \type \mathbb{S}^1}} }
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{displaymath}
+\begin{verbatim}
+ \MLScomp
+ {\prfStackPremises{\prfsummary{\Gamma\;\context}
+ {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type
+ \universe_i}}
+ {\prfsummary{\Gamma\;\context}
+ {\Gamma \vdash \basepoint \type \mathbb{S}^1}} }
+ {\prfStackPremises{\prfassumption
+ {\Gamma \vdash \ell \type \basepoint = \basepoint}}
+ {\prfassumption
+ {\Gamma \vdash p \type \mathbb{S}^1}} }
+ {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint)
+ \type C[p/x]}
+\end{verbatim}
+
+%-------------------------------------
+\clearpage
+\section{Hints and Tricks}\label{sec:hints_and_tricks}
+This section shows a few hints and tricks to use the package at its
+best.\vspace{2ex}
+
+Consider the proof:
+\begin{displaymath}
+ \begin{prfenv}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prfenv}
+\end{displaymath}
+the space between the axiom and the sub-proof of the positive case is
+visually much less than the space between the positive and the
+negative cases. Looking at boxes, the space is exactly the same, but
+the perception is that spacing is wrong.
+
+We can correct this perception in two distinct ways: by adding space
+between the axiom and the positive case; or, conversely, by moving the
+negative case closer to the positive one.
+
+The first strategy yields:
+\begin{displaymath}
+ \begin{prfenv}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.8em}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prfenv}
+\end{displaymath}
+and this effect is given by adding an appropriate \verb|\hspace| after
+the axiom, as in
+\begin{verbatim}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.4em}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}
+
+Adding the same space in front of the positive case is equivalent.
+
+The second strategy yields:
+\begin{displaymath}
+ \begin{prfenv}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.4em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prfenv}
+\end{displaymath}
+Again, this is obtained by adding a negative \verb|hspace| after the
+positive case, or, equivalently, before the negative one:
+\begin{verbatim}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.8em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}
+
+In general, to make a wide proof \emph{compact}, one can appropriately
+add negative spaces in front of sub-proofs so to make them closer and
+letting them to overlap as boxes, but not visually, thus \emph{tiling}
+the space.\vspace{2ex}
+
+Since proof trees are boxes, it is easy to align them on need. For
+example the following proof tree, with the bounding box put in
+evidence
+\begin{displaymath}
+ \fbox{\prfsummarystyle=1
+ \prfsummary{A}{B}{A \wedge B}}
+\end{displaymath}
+can be used wherever a box may appear. In the flow of text, it will
+look like \fbox{\prfsummarystyle=1\prfsummary{A}{B}{A \wedge B}}, so
+that the conclusion is aligned with the baseline. This makes easier to
+align proof trees, as in
+\begin{center}
+ \fbox{\prfsummarystyle=1
+ \prfsummary{f}{g}{f \wedge g}}\qquad
+ \fbox{$\begin{prfenv}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.4em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prfenv}$}
+\end{center}
+since this is the natural way to put proofs side by side:
+\begin{verbatim}
+ \fbox{\prfsummarystyle=1
+ \prfsummary{f}{g}{f \wedge g}}\qquad
+ \fbox{$
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.4em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}$}
+\end{verbatim}
+
+But, if really one has to include a proof tree in the flow of text, it
+is slightly better to vertically centre the box, as in
+\fbox{$\vcenter{\prfsummary{A}{B}{A \wedge B}}$}. This is obtained by
+\begin{verbatim}
+ $\vcenter{\prfsummary{A}{B}{A \wedge B}}$
+\end{verbatim}
+
+Of course, the result is not pleasant, because rows are far apart,
+which is unavoidable because of the height of the proof tree.
+
+The same principle applies also to arrays of proof trees:
+\begin{displaymath}
+ \begin{array}{lcccc}
+ \text{some text} &
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{displaymath}
+which has been typeset by
+\begin{verbatim}
+ \begin{array}{lcccc}
+ \text{some text} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{verbatim}
+vertically aligns the cells to their baselines.
+
+On the contrary
+\begin{displaymath}
+ \begin{array}{lcccc}
+ \text{some text} &
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{displaymath}
+is much better, and it is obtained by
+\begin{verbatim}
+ \begin{array}{lcccc}
+ \text{some text} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{verbatim}\vspace{2ex}
+
+The labelling of proof summaries is useful when a proof is very large
+and there is the need to split it. The strategy is to select some
+sub-proofs and to show them as summaries: instead of writing
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+we may consider to define
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \mbox{Let }
+ \left(\vcenter{\prfsummary<[f]s:abbrev>
+ {\NDDL{s:notnotA}{\neg\neg A}}
+ {\NDAL{s:notA}{\neg A}}
+ {\neg\neg A \supset A}}\right)
+ \equiv
+ \left(\vcenter{\NDIMPIL{s:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}\right)
+\end{displaymath}
+allowing to abbreviate the whole proof as
+\begin{displaymath}
+ \NDOREL{s:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-1em}\prfsummary<s:abbrev>
+ {\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDDL{[l]s:notA}{\neg A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+
+The corresponding \LaTeX{} code is
+\begin{verbatim}
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \mbox{Let }
+ \left(\vcenter{\prfsummary<[f]s:abbrev>
+ {\NDDL{s:notnotA}{\neg\neg A}}
+ {\NDAL{s:notA}{\neg A}}
+ {\neg\neg A \supset A}}\right)
+ \equiv
+ \left(\vcenter{\NDIMPIL{s:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}\right)
+\end{verbatim}
+for the definition of the proof summary, and
+\begin{verbatim}
+ \NDOREL{s:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-1em}\prfsummary<s:abbrev>
+ {\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDDL{[l]s:notA}{\neg A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}
+for its use.
+
+% -------------------------------------
+\clearpage
+\section{More Examples}\label{sec:examples}
+This section shows a number of examples illustrating the package. See
+the previous sections for the description of the features.\vspace{2ex}
+
+The disjunction elimination rule, with various line options:
+\begin{displaymath}
+ \renewcommand{\arraystretch}{3.7}
+ \begin{array}{@{}ccc@{}}
+ {\prfsummarystyle=1
+ \prftree{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[d]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r][d]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l][d]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[dotted]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[d,dotted]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,d,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,d,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[dashed]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[d,dashed]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[d,r,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[d,l,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[f]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,f]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,f]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[noline]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[noline][r]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[noline][l]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}}
+ \end{array}
+\end{displaymath}
+
+Proof that the Law of Excluded middle implies $\neg\neg A \supset A$:
+\begin{displaymath}
+ \prfIMPOptiontrue
+ \NDORE
+ {\NDLEM
+ {A \vee \neg A}\hspace{.4em}}
+ {\NDIMPI
+ {\NDD{A}}
+ {\neg\neg A \supset A}}
+ {\NDIMPI
+ {\NDFE
+ {\NDIMPE
+ {\NDD{\neg\neg A}}
+ {\NDD{\neg A}}
+ {\bot}}
+ {A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \prfIMPOptionfalse
+\end{displaymath}
+
+Proof that the Law of Excluded middle implies $\neg\neg A \supset A$
+with labels instead of rule names, except on axioms:
+\begin{displaymath}
+ \prftree[l]{$\scriptstyle\vee\mathrm{E}$}
+ {\NDLEM
+ {A \vee \neg A}\hspace{.6em}}
+ {\prftree[l]{$\scriptstyle\supset\mathrm{I}$}
+ {\NDD{A}}
+ {\neg\neg A \supset A}}
+ {\prftree[l]{$\scriptstyle\supset\mathrm{I}$}
+ {\prftree[l]{$\scriptstyle\bot\mathrm{E}$}
+ {\prftree[l]{$\scriptstyle\supset\mathrm{E}$}
+ {\NDD{\neg\neg A}}
+ {\NDD{\neg A}}
+ {\bot}}
+ {A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+
+Another simple proof in natural deduction:
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}\hspace{2em}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}
+
+The same proof, under the proposition-as-types interpretation:
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfassumption{u\colon A \rightarrow (B \rightarrow C)}}
+ {\prfassumption{w\colon A}}
+ {u w\colon B \rightarrow C}\hspace{2em}}
+ {\prftree
+ {\prfassumption{v\colon A \rightarrow B}}
+ {\prfassumption{w\colon A}}
+ {v w\colon B}}
+ {u w(v w)\colon C}}
+ {\lambda w.\, u w(v w)\colon A \rightarrow C}}
+ {\lambda v w.\, u w(v w)\colon (A \rightarrow B) \rightarrow (A
+ \rightarrow C)}}
+ {\lambda u v w.\, u w(v w)\colon (A \rightarrow (B \rightarrow C))
+ \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))}
+\end{displaymath}
+
+A deduction in a sequent calculus:
+\begin{displaymath}
+ \prfinterspace=1.2em
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfassumption{A \Rightarrow A}}
+ {\prftree
+ {\prfassumption{A \Rightarrow A}}
+ {\prftree
+ {B \Rightarrow B}
+ {C \Rightarrow C}
+ {B, B \rightarrow C \Rightarrow C}}
+ {A, A \rightarrow B, B \rightarrow C \Rightarrow C}}
+ {A, A \rightarrow B, A \rightarrow (B \rightarrow C)
+ \Rightarrow C}}
+ {A \rightarrow B, A \rightarrow (B \rightarrow C) \Rightarrow A
+ \rightarrow C}}
+ {A \rightarrow (B \rightarrow C) \Rightarrow (A \rightarrow B)
+ \rightarrow (A \rightarrow C)}}
+ {\Rightarrow (A \rightarrow (B \rightarrow C)) \rightarrow ((A
+ \rightarrow B) \rightarrow (A \rightarrow C))}
+\end{displaymath}
+
+Proof trees can be coloured, as kindly pointed out by Dominic Hughes:
+\begin{displaymath}
+ \begin{prfenv}
+ \color{green}\NDIMPIL{ex6:1}
+ {\NDANDI
+ {\color{red}\NDNOTIL{ex6:2}
+ {\NDNOTE
+ {\NDDL{ex6:1}{\neg (A \vee B)}}
+ {\NDORIL
+ {\NDDL{ex6:2}{A}}
+ {A \vee B}}
+ {\bot}}
+ {\neg A}}
+ {\color{blue}\NDNOTIL{ex6:3}
+ {\NDNOTE
+ {\NDDL{[l]ex6:1}{\neg (A \vee B)}}
+ {\NDORIR
+ {\NDDL{ex6:3}{B}}
+ {A \vee B}}
+ {\bot}}
+ {\neg B}}
+ {\neg A \wedge \neg B}}
+ {\neg (A \vee B) \supset \neg A \wedge \neg B}
+ \end{prfenv}
+\end{displaymath}\vspace{.2ex}
+
+Also. all the standard box manipulation commands can be freely applied.
+The following examples are not significant for doing mathematics, but
+the mechanics behind can be occasionally useful, for example, to
+shrink a large proof to fit the page length:
+\begin{displaymath}
+ \rotatebox{15}{\begin{prfenv}
+ \NDIMPIL{ex5:1}
+ {\NDANDI
+ {\NDNOTIL{ex5:2}
+ {\NDNOTE
+ {\NDDL{ex5:1}{\neg (A \vee B)}}
+ {\NDORIL
+ {\NDDL{ex5:2}{A}}
+ {A \vee B}}
+ {\bot}}
+ {\neg A}}
+ {\NDNOTIL{ex5:3}
+ {\NDNOTE
+ {\NDDL{[l]ex5:1}{\neg (A \vee B)}}
+ {\NDORIR
+ {\NDDL{ex5:3}{B}}
+ {A \vee B}}
+ {\bot}}
+ {\neg B}}
+ {\neg A \wedge \neg B}}
+ {\neg (A \vee B) \supset \neg A \wedge \neg B}
+ \end{prfenv}}
+\end{displaymath}
+\begin{displaymath}
+ \begin{prfenv}
+ \NDIMPIL{ex7:1}
+ {\NDANDI
+ {\reflectbox{\NDNOTIL{ex7:2}
+ {\NDNOTE
+ {\NDDL{ex7:1}{\neg (A \vee B)}}
+ {\NDORIL
+ {\NDDL{ex7:2}{A}}
+ {A \vee B}}
+ {\bot}}
+ {\neg A}}}
+ {\resizebox{20em}{!}{\NDNOTIL{ex7:3}
+ {\NDNOTE
+ {\NDDL{[l]ex7:1}{\neg (A \vee B)}}
+ {\scalebox{.7}[1]{\NDORIR
+ {\NDDL{ex7:3}{B}}
+ {A \vee B}}}
+ {\bot}}
+ {\neg B}}}
+ {\neg A \wedge \neg B}}
+ {\neg (A \vee B) \supset \neg A \wedge \neg B}
+ \end{prfenv}
+\end{displaymath}
+
+% -------------------------------------
+\clearpage
+\section{Fonts}\label{sec:fonts}
+The package works with any font. It uses the current math fonts for
+typesetting proofs, while it uses the current text font to typeset
+labels and rule names.
+
+Care has been taken to ensure that the various dimensions and
+parameters in Section~\ref{sec:parameters} are relative to the current
+font, that is, technically, they are expressed with units \texttt{ex}
+for vertical lengths, and \texttt{em} for horizontal lengths. Dashes
+are \TeX\ rules with thickness \verb|\prflinethickness|.
+
+For unknown reasons, the \texttt{fontenc} package modifies slightly
+the values for \texttt{ex} and \texttt{em}, thus the graphical
+appearance of proof trees may vary when comparing the results obtained
+by compiling with and without this package.
+
+In most cases, the graphical appearance of proofs is acceptable, even
+changing font and size. But using fonts whose body is particularly
+heavy, may result in proof lines which are too thin. In this case, the
+user of the package should increment the value of
+\verb|\prflinethickness|.
+
+The package, up to version 1.5, was designed to work with the Computer
+Modern family of fonts. It worked also with other fonts, without any
+major problem, but, as kindly signalled by D{\'e}mi Nollet at ENS Lyon
+and universit{\'e} Paris-Diderot, dashed and dotted lines do not
+behave correctly, as dashes overlap. Please, update to the latest
+version of the package if you plan to use fonts different from
+Computer Modern.
+
+% -------------------------------------
+\clearpage
+\section{Internals}\label{sec:internals}
+A proof tree is typeset as a \TeX{} box in horizontal mode. This means
+that wherever a character can stay, so does a proof: in principle,
+there is no need to put the proof in a math environment. Also, the
+width of a proof is exactly the width of the box; the height of the
+proof is the height of the conclusion plus the total height of all the
+matter above it; the depth of the proof is the depth of the
+conclusion. The proof is aligned so that the current baseline is the
+baseline of the conclusion.
+
+For example, the proof of $g \supset \neg\neg g$ in natural deduction
+is:
+\begin{displaymath}
+ \mbox{proof} \equiv
+ \fbox{\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{g}}
+ {\prfboundedassumption{\neg g}}
+ {\bot}}
+ {\neg\neg g}}
+ {g \supset \neg\neg g}}
+\end{displaymath}
+The proof has been surrounded by a framebox to make evident its
+bounds. Also, since the letter $g$ has a depth, the example shows how
+depth in the conclusion influences the alignment of the proof with
+respect to the preceding text.\vspace{2ex}
+
+Actually, the fundamental command in the package is \verb|\prftree|:
+the commands to construct assumptions (\verb|\prfassumption| and
+\verb|\prfboundedassumption|), those to generate axioms
+(\verb|\prfaxiom| and \verb|\prfbyaxiom|), and \verb|\prfsummary| are
+just appropriate instances.\vspace{2ex}
+
+The \verb|\prftree| command is composed by a parser, which takes care
+of reading the various options and parameters, and by a graphical
+engine, \verb|\prf@draw|, which calculates and draw the box containing
+the proof tree.
+
+It may be useful to understand how the graphical engine works. In the
+first place, each proof tree is a box with a structure:
+\begin{center}
+ {\setlength{\unitlength}{1em}
+ \begin{picture}(27,6)
+ \put(0.8,0){\framebox(26.2,6){}}
+ \put(5,4){\framebox(18,1.8){$\cdots$}}
+ \put(5.2,4.2){\framebox(6,1.4){$\mbox{assumption}_1$}}
+ \put(16.8,4.2){\framebox(6,1.4){$\mbox{assumption}_n$}}
+ \put(7,3){\line(1,0){14}}
+ \put(22,2.3){\framebox(4.8,1.4){rule name}}
+ \put(1,2.3){\framebox(4.8,1.4){label}}
+ \put(8.5,0.2){\framebox(11,1.8){conclusion}}
+ \end{picture}}
+\end{center}
+
+The conclusion, the proof line, and the \emph{assumption line} are
+centred. The assumption line is the line whose first element is the
+conclusion of the first assumption, and whose last element is the
+conclusion of the last assumption, properly spaced so that all the
+assumptions fit in between. The width of the proof line is calculated
+as the maximum of the width of the assumption line and the conclusion,
+with the rule name and the label, if present, hanging on the right and
+the left, respectively.
+
+To calculate the assumption line, the engine keeps track of the
+position of the conclusion within a proof tree, which reduces to
+remember how far is the conclusion from the left margin
+(\verb|Lassum|), and how far it is from the right margin
+(\verb|Rassum|). So, the assumption line starts from the value of
+\verb|Lassum| of the first assumption, and finishes at \verb|Rassum|
+of the last assumption.
+
+Thus, with these values it is not difficult to figure out the
+mathematics to place the various boxes around, so to combine them into
+a proof tree. This is exactly what the graphical engine does.
+
+Unfortunately, when one writes assumptions as simple formulae, without
+the \verb|\prfassumption| command, the corresponding \verb|Lassum| and
+\verb|Rassum| are not set to $0$, which is the right value. In fact,
+the recursive expansion of the \verb|\prf@draw| macro follows the
+\emph{natural} order in the construction of the proof box, which is
+extremely useful because it allows to locally modify parameters in
+sub-proofs; but this order conflicts with proper rendering of
+assumptions which are not proof trees.
+
+Also, the hints on how to put space between assumptions, see
+Section~\ref{sec:hints_and_tricks}, may have strange effects: if space
+is added in front of the first assumption or behind the last one, this
+space makes invalid the values of \verb|Lassum| and \verb|Rassum|,
+respectively, yielding hard to predict results.
+
+It is worth remarking that the mathematics of the graphical engine is
+sound, which means that zero or negative values for the various
+dimensions specified as parameters, or using \emph{bizarre} boxes in
+the fancy commands, yields the expected results, as far as boxes do
+not have parts which extends beyond the bounds.\vspace{2ex}
+
+The implementation of references mimics the implementation of
+\verb|\label| and \verb|\ref| in \LaTeX. Whenever a reference is
+defined, through a command with the $\langle \mathrm{label}\rangle$ as
+the first argument, the reference value is created according to the
+options, and it gets stored in the \texttt{.aux} file, by writing
+$\verb|\prfauxvalue|\{\mathrm{label}\}\{\mathrm{value}\}$ in the
+file. Then, when the source code will be recompiled, and the
+\texttt{.aux} file read, this command will be executed before any
+occurrence of a reference, which can be resolved.
+
+Most difficulties in the implementation of references lie in the way
+to construct the boxes to be used in the proof tree. But, the tricky
+part is the interaction with the \LaTeX{} and \TeX{} kernel for error
+reporting. A small hack has been introduced to force recompilation
+when the references in a proof change.
+
+% -------------------------------------
+\clearpage
+\section{Future Features and Bugs}\label{sec:future_features}
+Essentially, all the features of Buss's package have been implemented
+but one: alignment of proofs according to the $\vdash$ (or equivalent)
+sign. While this feature is occasionally useful in the writing of
+sequent proofs, it requires some trickery in the graphical engine, so
+it has been postponed for the moment.\vspace{2ex}
+
+Moreover, automatic compact proofs have been analysed, but not
+implemented. A compact proof minimises the amount of space between
+subsequent assumptions, eventually making the upper trees to overlap
+as boxes, but not as typed text.
+
+The algorithm to obtain this result is not immediate: one should keep
+track of the left and right \emph{skylines} of a proof. Comparing the
+left skyline of an assumption with the right skyline of the next one,
+one can calculate what is the distance between the boxes so that the
+distance between the closest points in the skylines is exactly
+\verb|\prfinterspace|.
+
+It is not simple to code such an algorithm in \TeX{}, but the real
+difficulty is how to represent skylines and how to store them, since
+\TeX{} provides no abstract data structures. Hence, the implementation
+of this feature has been postponed to a remote future, or to the will
+of a real \TeX{} magician.\vspace{2ex}
+
+The abbreviated commands reflect their use by the author. It is quite
+possible that you want to define your own commands for inference rules
+of your interest. If you think they could be of general interest, send
+them by email to the author (see below) who will include them in a
+future release of the package, acknowledging your contribution.
+\vfill
+
+Although the package has been tested for a long time by now, it is
+possible that a few bugs are still present. To signal a bug, please,
+write an email to the author (see below), possibly attaching a sample
+document which exhibit the misbehaviour, to help tracking and fixing.
+\vfill
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-06 09:24:21 +0000