diff options
author | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
commit | e0c6872cf40896c7be36b11dcc744620f10adf1d (patch) | |
tree | 60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/prftree/prftree.sty |
Initial commit
Diffstat (limited to 'macros/latex/contrib/prftree/prftree.sty')
-rw-r--r-- | macros/latex/contrib/prftree/prftree.sty | 1446 |
1 files changed, 1446 insertions, 0 deletions
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 +% ------------------------------------------------------------------- |