summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/prftree
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2019-06-19 20:35:11 +0000
committerKarl Berry <karl@freefriends.org>2019-06-19 20:35:11 +0000
commita1eb6c9ee4af7077c2880c37f051b564b8e05ca7 (patch)
tree5c34083fb183cb91bcdb5d92bc88bb1bc1d45c1c /Master/texmf-dist/tex/latex/prftree
parent41be7740176343cd88808bef0d403a044b4c5895 (diff)
prftree (19jun19)
git-svn-id: svn://tug.org/texlive/trunk@51404 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/prftree')
-rw-r--r--Master/texmf-dist/tex/latex/prftree/prftree.sty532
1 files changed, 437 insertions, 95 deletions
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty
index 8f77541c058..10d6fbce6c2 100644
--- a/Master/texmf-dist/tex/latex/prftree/prftree.sty
+++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty
@@ -1,7 +1,7 @@
%
% prftree.sty
-% by Marco Benini - 3rd September 2016
-% v1.5
+% by Marco Benini - 19th June 2019
+% v1.6
%
% A package to typeset natural deduction proofs, or sequent proofs, or
% tableau proofs
@@ -10,18 +10,25 @@
%
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{prftree}[2016/09/03 Natural Deduction Proofs]
+\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
@@ -977,14 +984,42 @@
\hbox{$\box\prf@rulenamebox$}}
% -------------------------------------------------------------------
-% The following macros are used to simplify the writing of proofs in
-% natural deduction, and they roughly follow the format of proofs as
-% in Troelstra, Schwichtenberg "Basic Proof Theory".
-%
-% Since they may conflict with other packages, they are controlled by
-% options in the package.
+% 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
%
@@ -997,62 +1032,36 @@
\def\NDAL#1{\prfassumption<#1>}
\def\NDDL#1{\prfboundedassumption<#1>}
\def\NDP{\prftree}
- \def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \textup{I}$}}
- \def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \textup{E}_1$}}
- \def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \textup{E}_2$}}
- \def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \textup{E}$}}
- \def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \textup{I}_1$}}
- \def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \textup{I}_2$}}
- \def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \textup{I}$}}
- \def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \textup{E}$}}
- \def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}%
- {\textup{E}}^{\prfref<#1>}$}}
+ \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
- \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \textup{I}$}}
- \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \textup{E}$}}
- \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \textup{I}^{\prfref<#1>}$}}
+ \prfMakeInferenceRule{NDIMPI}{\mathord{\supset}\textup{I}}
+ \prfMakeInferenceRule{NDIMPE}{\mathord{\supset}\textup{E}}
+ \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\supset}\textup{I}}
\else
- \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \textup{I}$}}
- \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \textup{E}$}}
- \def\NDIMPIL#1{%
- \prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \textup{I}^{\prfref<#1>}$}}\fi
- \def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}%
- \textup{I}$}}
- \def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}%
- \textup{I}^{\prfref<#1>}$}}
- \def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}%
- \textup{E}$}}
- \def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}%
- \textup{I}$}}
- \def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}%
- \textup{E}$}}
- \def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}%
- \textup{I}$}}
- \def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}%
- \textup{E}$}}
- \def\NDEXEL#1{%
- \prftree[by]{$\scriptstyle\mathord{\exists}%
- \textup{E}^{\prfref<#1>}$}}
- \def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}%
- \textup{I}$}}
- \def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}%
- \textup{E}$}}
- \def\NDLEM{\prftree[by]{$\scriptstyle\textup{lem}$}}
- \def\NDAX{\prftree[by]{$\scriptstyle\textup{ax}$}}
+ \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
% -------------------------------------------------------------------
@@ -1064,41 +1073,374 @@
\ifprf@SEQOption%
\def\SEQA{\prfassumption}
\def\SEQD{\prfboundedassumption}
- \def\SEQP{\prftree}
- \def\SEQAX{\prftree[by]{$\scriptstyle\textup{Ax}$}}
- \def\SEQLF{\prftree[by]{$\scriptstyle\textup{L}\bot$}}
- \def\SEQLW{\prftree[by]{$\scriptstyle\textup{LW}$}}
- \def\SEQRW{\prftree[by]{$\scriptstyle\textup{RW}$}}
- \def\SEQLC{\prftree[by]{$\scriptstyle\textup{LC}$}}
- \def\SEQRC{\prftree[by]{$\scriptstyle\textup{RC}$}}
- \def\SEQLAND{\prftree[by]{$\scriptstyle\textup{L}%
- \mathord{\wedge}$}}
- \def\SEQRAND{\prftree[by]{$\scriptstyle\textup{R}%
- \mathord{\wedge}$}}
- \def\SEQLOR{\prftree[by]{$\scriptstyle\textup{L}%
- \mathord{\vee}$}}
- \def\SEQROR{\prftree[by]{$\scriptstyle\textup{R}%
- \mathord{\vee}$}}
+ \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
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
- \mathord{\supset}$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
- \mathord{\supset}$}}
+ \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\supset}}
+ \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\supset}}
\else
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
- \mathord{\rightarrow}$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
- \mathord{\rightarrow}$}}
+ \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\rightarrow}}
+ \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\rightarrow}}
\fi
- \def\SEQLALL{\prftree[by]{$\scriptstyle\textup{L}%
- \mathord{\forall}$}}
- \def\SEQRALL{\prftree[by]{$\scriptstyle\textup{R}%
- \mathord{\forall}$}}
- \def\SEQLEX{\prftree[by]{$\scriptstyle\textup{L}%
- \mathord{\exists}$}}
- \def\SEQREX{\prftree[by]{$\scriptstyle\textup{R}%
- \mathord{\exists}$}}
- \def\SEQCUT{\prftree[by]{$\scriptstyle\textup{Cut}$}}
+ \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
+% -------------------------------------------------------------------