diff options
Diffstat (limited to 'Master/texmf-dist/tex/latex')
-rw-r--r-- | Master/texmf-dist/tex/latex/prftree/prftree.sty | 532 |
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 +% ------------------------------------------------------------------- |