diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 176 |
1 files changed, 88 insertions, 88 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index ae52265..64f597f 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -923,16 +923,16 @@ de type $\tau$ dans le contexte $\Gamma$ ». Les trois règles de typage du $\lambda$CST : \[ -\inferrule*[left=\llap{Var}]{ }{\Gamma,x:\sigma \vdash x:\sigma} +\inferrule*[Left={Var}]{ }{\Gamma,x:\sigma \vdash x:\sigma} \] \[ -\inferrule*[left=\llap{App},sep=4em]{\Gamma \vdash P:\sigma\to\tau\\ \Gamma +\inferrule*[Left={App},sep=4em]{\Gamma \vdash P:\sigma\to\tau\\ \Gamma \vdash Q:\sigma}{\Gamma \vdash PQ:\tau} \] \[ -\inferrule*[left=\llap{Abs}]{\Gamma, v:\sigma \vdash E:\tau}{\Gamma +\inferrule*[Left={Abs}]{\Gamma, v:\sigma \vdash E:\tau}{\Gamma \vdash \lambda(v:\sigma).E : \sigma\to\tau} \] @@ -957,17 +957,17 @@ est un terme de type $(\beta\to\alpha\to\gamma) \to {\footnotesize \[ -\inferrule*[left=\llap{Abs}]{ -\inferrule*[left=\llap{Abs}]{ -\inferrule*[left=\llap{Abs}]{ -\inferrule*[left=\llap{App}]{ -\inferrule*[left=\llap{App}]{ -\inferrule*[left=\llap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash f : \beta\to\alpha\to\gamma} +\inferrule*[Left={Abs}]{ +\inferrule*[Left={Abs}]{ +\inferrule*[Left={Abs}]{ +\inferrule*[Left={App}]{ +\inferrule*[Left={App}]{ +\inferrule*[Left={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash f : \beta\to\alpha\to\gamma} \\ -\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash y : \beta} +\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash y : \beta} }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash fy : \alpha\to\gamma} \\ -\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash x : \alpha} +\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash x : \alpha} }{f:\beta\to\alpha\to\gamma, x:\alpha, y:\beta \vdash fyx : \gamma} }{f:\beta\to\alpha\to\gamma, x:\alpha \vdash \lambda(y:\beta). fyx : \beta\to\gamma} }{f:\beta\to\alpha\to\gamma \vdash \lambda(x:\alpha). \lambda(y:\beta). fyx : \alpha\to\beta\to\gamma} @@ -1121,17 +1121,17 @@ dont on n'a donné que les types et les règles appliquées ? {\footnotesize \[ -\inferrule*[left=\llap{Abs}]{ -\inferrule*[left=\llap{Abs}]{ -\inferrule*[left=\llap{Abs}]{ -\inferrule*[left=\llap{App}]{ -\inferrule*[left=\llap{App}]{ -\inferrule*[left=\llap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta\to\alpha\to\gamma} +\inferrule*[Left={Abs}]{ +\inferrule*[Left={Abs}]{ +\inferrule*[Left={Abs}]{ +\inferrule*[Left={App}]{ +\inferrule*[Left={App}]{ +\inferrule*[Left={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta\to\alpha\to\gamma} \\ -\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta} +\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta} }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha\to\gamma} \\ -\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha} +\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha} }{\textbf{?}:\beta\to\alpha\to\gamma, \textbf{?}:\alpha, \textbf{?}:\beta \vdash \textbf{?} : \gamma} }{\textbf{?}:\beta\to\alpha\to\gamma, \textbf{?}:\alpha \vdash \textbf{?} : \beta\to\gamma} }{\textbf{?}:\beta\to\alpha\to\gamma \vdash \textbf{?} : \alpha\to\beta\to\gamma} @@ -1444,13 +1444,13 @@ de $\land$, etc.) : {\footnotesize \[ \inferrule*[left={$\Rightarrow$Int},right=\hphantom{Int}]{ -\inferrule*[left=\llap{$\land$Int}]{ -\inferrule*[left=\llap{$\land$Élim$_2$}]{ -\inferrule*[left=\llap{Ax}]{ }{A\land B \vdash A\land B} +\inferrule*[Left={$\land$Int}]{ +\inferrule*[Left={$\land$Élim$_2$}]{ +\inferrule*[Left={Ax}]{ }{A\land B \vdash A\land B} }{A\land B \vdash B} \\ -\inferrule*[right=\rlap{$\land$Élim$_1$}]{ -\inferrule*[right=\rlap{Ax}]{ }{A\land B \vdash A\land B} +\inferrule*[Right={$\land$Élim$_1$}]{ +\inferrule*[Right={Ax}]{ }{A\land B \vdash A\land B} }{A\land B \vdash A} }{A\land B \vdash B\land A} }{\vdash A\land B \Rightarrow B\land A} @@ -1462,15 +1462,15 @@ de $\land$, etc.) : {\footnotesize \[ \inferrule*[left={$\Rightarrow$Int},right=\hphantom{Int}]{ -\inferrule*[left=\llap{$\lor$Élim}]{ -\inferrule*[left=\llap{Ax}]{ }{A\lor B \vdash A\lor B} +\inferrule*[Left={$\lor$Élim}]{ +\inferrule*[Left={Ax}]{ }{A\lor B \vdash A\lor B} \\ \inferrule*[right={$\lor$Int$_2$}]{ -\inferrule*[right=\rlap{Ax}]{ }{A\lor B,A \vdash A} +\inferrule*[Right={Ax}]{ }{A\lor B,A \vdash A} }{A\lor B,A \vdash B\lor A} \\ -\inferrule*[right=\rlap{$\lor$Int$_1$}]{ -\inferrule*[right=\rlap{Ax}]{ }{A\lor B,B \vdash B} +\inferrule*[Right={$\lor$Int$_1$}]{ +\inferrule*[Right={Ax}]{ }{A\lor B,B \vdash B} }{A\lor B,B \vdash B\lor A} }{A\lor B \vdash B\lor A} }{\vdash A\lor B \Rightarrow B\lor A} @@ -1492,13 +1492,13 @@ pour un gain de place) : {\footnotesize \[ \inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})},right=\hphantom{Int}]{ -\inferrule*[left=\llap{$\land$Int}]{ -\inferrule*[left=\llap{$\land$Élim$_2$}]{ -\inferrule*[left=\llap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B} +\inferrule*[Left={$\land$Int}]{ +\inferrule*[Left={$\land$Élim$_2$}]{ +\inferrule*[Left={\textcolor{mydarkgreen}{$u$}}]{ }{A\land B} }{B} \\ -\inferrule*[right=\rlap{$\land$Élim$_1$}]{ -\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B} +\inferrule*[Right={$\land$Élim$_1$}]{ +\inferrule*[Right={\textcolor{mydarkgreen}{$u$}}]{ }{A\land B} }{A} }{B\land A} }{A\land B \Rightarrow B\land A} @@ -1510,15 +1510,15 @@ pour un gain de place) : {\footnotesize \[ \inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})},right=\hphantom{Int}]{ -\inferrule*[left=\llap{$\lor$Élim(\textcolor{mydarkgreen}{$v$},\textcolor{mydarkgreen}{$v'$})}]{ -\inferrule*[left=\llap{\textcolor{mydarkgreen}{$u$}}]{ }{A\lor B} +\inferrule*[Left={$\lor$Élim(\textcolor{mydarkgreen}{$v$},\textcolor{mydarkgreen}{$v'$})}]{ +\inferrule*[Left={\textcolor{mydarkgreen}{$u$}}]{ }{A\lor B} \\ \inferrule*[right={$\lor$Int$_2$}]{ -\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v$}}]{ }{A} +\inferrule*[Right={\textcolor{mydarkgreen}{$v$}}]{ }{A} }{B\lor A} \\ -\inferrule*[right=\rlap{$\lor$Int$_1$}]{ -\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v'$}}]{ }{B} +\inferrule*[Right={$\lor$Int$_1$}]{ +\inferrule*[Right={\textcolor{mydarkgreen}{$v'$}}]{ }{B} }{B\lor A} }{B\lor A} }{A\lor B \Rightarrow B\lor A} @@ -2009,17 +2009,17 @@ $(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ : {\footnotesize \[ -\inferrule*[left=\llap{$\Rightarrow$Int}]{ -\inferrule*[left=\llap{$\Rightarrow$Int}]{ -\inferrule*[left=\llap{$\Rightarrow$Int}]{ -\inferrule*[left=\llap{$\Rightarrow$Élim}]{ -\inferrule*[left=\llap{$\Rightarrow$Élim}]{ -\inferrule*[left=\llap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C } +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C } \\ -\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B } +\inferrule*[Right={Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B } }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A \Rightarrow C } \\ -\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A } +\inferrule*[Right={Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A } }{B \Rightarrow A \Rightarrow C , A , B \vdash C } }{B \Rightarrow A \Rightarrow C , A \vdash B \Rightarrow C } }{B \Rightarrow A \Rightarrow C \vdash A \Rightarrow B \Rightarrow C } @@ -2076,13 +2076,13 @@ de $A\land B \Rightarrow B\land A$ {\footnotesize \[ \inferrule*[left={Abs},right=\hphantom{Abs}]{ -\inferrule*[left=\llap{Pair}]{ -\inferrule*[left=\llap{Proj$_2$}]{ -\inferrule*[left=\llap{Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta} +\inferrule*[Left={Pair}]{ +\inferrule*[Left={Proj$_2$}]{ +\inferrule*[Left={Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta} }{u:\alpha\times \beta \vdash \pi_2 u:\beta} \\ -\inferrule*[right=\rlap{Proj$_1$}]{ -\inferrule*[right=\rlap{Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta} +\inferrule*[Right={Proj$_1$}]{ +\inferrule*[Right={Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta} }{u:\alpha\times \beta \vdash \pi_1 u:\alpha} }{u:\alpha\times \beta \vdash \langle \pi_2 u, \pi_1 u\rangle:\beta\times \alpha} }{\vdash \lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle : \alpha\times \beta \rightarrow \beta\times \alpha} @@ -2187,15 +2187,15 @@ de $A\lor B \Rightarrow B\lor A$ {\footnotesize \[ \inferrule*[left={Abs},right=\hphantom{Int}]{ -\inferrule*[left=\llap{Match}]{ -\inferrule*[left=\llap{Var}]{ }{u:\alpha+\beta \vdash u:\alpha+\beta} +\inferrule*[Left={Match}]{ +\inferrule*[Left={Var}]{ }{u:\alpha+\beta \vdash u:\alpha+\beta} \\ \inferrule*[right={Inj$_2$}]{ -\inferrule*[right=\rlap{Var}]{ }{\ldots,v:\alpha \vdash v:\alpha} +\inferrule*[Right={Var}]{ }{\ldots,v:\alpha \vdash v:\alpha} }{{\scriptstyle\cdots} \vdash \iota_2^{(\beta,\alpha)} v : \beta+\alpha} \\ -\inferrule*[right=\rlap{Inj$_1$}]{ -\inferrule*[right=\rlap{Var}]{ }{\ldots,v':\beta \vdash v':\beta} +\inferrule*[Right={Inj$_1$}]{ +\inferrule*[Right={Var}]{ }{\ldots,v':\beta \vdash v':\beta} }{{\scriptstyle\cdots} \vdash \iota_1^{(\beta,\alpha)} v' : \beta+\alpha} }{u:\alpha+\beta \vdash (\texttt{match~} u\texttt{~with~}\iota_1 v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') : \beta+\alpha} @@ -2738,20 +2738,20 @@ $\bot$ On reprend les mêmes exemples que dans le transp. \ref{example-propositional-proofs} : -\vskip-5ex\leavevmode +\vskip-2ex\leavevmode \begin{center} \begin{tabular}{c|c} % {\footnotesize $ \inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{ -\inferrule*[left=\llap{$\land$R}]{ -\inferrule*[left=\llap{$\land$L$_2$}]{ -\inferrule*[left=\llap{Ax}]{ }{B \vdash B} +\inferrule*[Left={$\land$R}]{ +\inferrule*[Left={$\land$L$_2$}]{ +\inferrule*[Left={Ax}]{ }{B \vdash B} }{A\land B \vdash B} \\ -\inferrule*[right=\rlap{$\land$L$_1$}]{ -\inferrule*[right=\rlap{Ax}]{ }{A \vdash A} +\inferrule*[Right={$\land$L$_1$}]{ +\inferrule*[Right={Ax}]{ }{A \vdash A} }{A\land B \vdash A} }{A\land B \vdash B\land A} }{\vdash A\land B \Rightarrow B\land A} @@ -2761,13 +2761,13 @@ $ {\footnotesize $ \inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{ -\inferrule*[left=\llap{$\lor$L}]{ -\inferrule*[left=\llap{$\lor$R$_2$}]{ -\inferrule*[left=\llap{Ax}]{ }{A \vdash A} +\inferrule*[Left={$\lor$L}]{ +\inferrule*[Left={$\lor$R$_2$}]{ +\inferrule*[Left={Ax}]{ }{A \vdash A} }{A \vdash B\lor A} \\ -\inferrule*[right=\rlap{$\lor$R$_1$}]{ -\inferrule*[right=\rlap{Ax}]{ }{B \vdash B} +\inferrule*[Right={$\lor$R$_1$}]{ +\inferrule*[Right={Ax}]{ }{B \vdash B} }{B \vdash B\lor A} }{A\lor B \vdash B\lor A} }{\vdash A\lor B \Rightarrow B\lor A} @@ -2783,16 +2783,16 @@ Et que dans le transp. \ref{example-proposition-proof-with-implication} : \vskip-2ex {\footnotesize \[ -\inferrule*[left=\llap{$\Rightarrow$R}]{ -\inferrule*[left=\llap{$\Rightarrow$R}]{ -\inferrule*[left=\llap{$\Rightarrow$R}]{ -\inferrule*[left=\llap{$\Rightarrow$L}]{ -\inferrule*[left=\llap{Ax}]{ }{A, B \vdash B } +\inferrule*[Left={$\Rightarrow$R}]{ +\inferrule*[Left={$\Rightarrow$R}]{ +\inferrule*[Left={$\Rightarrow$R}]{ +\inferrule*[Left={$\Rightarrow$L}]{ +\inferrule*[Left={Ax}]{ }{A, B \vdash B } \\ -\inferrule*[right=\rlap{$\Rightarrow$L}]{ -\inferrule*[left=\llap{Ax}]{ }{A , B \vdash A } +\inferrule*[Right={$\Rightarrow$L}]{ +\inferrule*[Left={Ax}]{ }{A , B \vdash A } \\ -\inferrule*[right=\rlap{Ax}]{ }{C , A , B \vdash C } +\inferrule*[Right={Ax}]{ }{C , A , B \vdash C } }{A \Rightarrow C , A , B \vdash C } }{B \Rightarrow A \Rightarrow C , A , B \vdash C } }{B \Rightarrow A \Rightarrow C , A \vdash B \Rightarrow C } @@ -2881,10 +2881,10 @@ Calcul des séquents&Déduction naturelle\\\hline $\inferrule*[left=$\Rightarrow$L]{\Gamma\vdash M\\\Gamma,P\vdash R}{\Gamma,M\Rightarrow P\vdash R}$ & $\inferrule*[left=$\Rightarrow$Élim]{ -\inferrule*[left=\llap{$\Rightarrow$Intro}]{\Gamma,P\vdash R}{\Gamma\vdash P\Rightarrow R} +\inferrule*[Left={$\Rightarrow$Intro}]{\Gamma,P\vdash R}{\Gamma\vdash P\Rightarrow R} \\ \inferrule*[left=$\Rightarrow$Élim]{ -\inferrule*[left=\llap{Ax}]{ }{\Gamma,M\Rightarrow P\vdash M\Rightarrow P} +\inferrule*[Left={Ax}]{ }{\Gamma,M\Rightarrow P\vdash M\Rightarrow P} \\\Gamma\vdash M}{\Gamma,M\Rightarrow P\vdash P} }{\Gamma,M\Rightarrow P\vdash R}$ \end{tabular} @@ -2946,16 +2946,16 @@ branches de la coupure n'opère pas sur la formule coupée : on fait \begin{center} \scalebox{0.65}{% $\inferrule*[left={\color{purple}Cut}]{ -\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2} +\inferrule*[Left={$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2} \\ -\inferrule*[right=\rlap{?}]{\mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}}{\Gamma,P_1\land P_2\vdash Q} +\inferrule*[Right={?}]{\mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}}{\Gamma,P_1\land P_2\vdash Q} }{\Gamma\vdash Q}$ } ~devient~ \scalebox{0.65}{% -$\inferrule*[right=\rlap{?}]{ -\inferrule*[left=\llap{\color{purple}Cut}]{ -\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2} +$\inferrule*[Right={?}]{ +\inferrule*[Left={\color{purple}Cut}]{ +\inferrule*[Left={$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2} \\ \mpdotsabove{\Gamma',P_1\land P_2\vdash Q'} }{\Gamma,\Gamma'\vdash Q'} @@ -2996,9 +2996,9 @@ de complexité de la formule coupée diminue : \begin{center} \scalebox{0.8}{% $\inferrule*[left={\color{purple}Cut}]{ -\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2} +\inferrule*[Left={$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2} \\ -\inferrule*[right=\rlap{$\land$L$_1$}]{\mpdotsabove{\Gamma,P_1\vdash Q}}{\Gamma,P_1\land P_2\vdash Q} +\inferrule*[Right={$\land$L$_1$}]{\mpdotsabove{\Gamma,P_1\vdash Q}}{\Gamma,P_1\land P_2\vdash Q} }{\Gamma\vdash Q}$ } ~devient~ @@ -3014,9 +3014,9 @@ $\inferrule*[left={\color{purple}Cut}]{ \begin{center} \scalebox{0.7}{% $\inferrule*[left={\color{purple}Cut}]{ -\inferrule*[left=\llap{$\Rightarrow$R}]{\mpdotsabove{\Gamma, M\vdash P}}{\Gamma \vdash M\Rightarrow P} +\inferrule*[Left={$\Rightarrow$R}]{\mpdotsabove{\Gamma, M\vdash P}}{\Gamma \vdash M\Rightarrow P} \\ -\inferrule*[right=\rlap{$\Rightarrow$L}]{\mpdotsabove{\Gamma \vdash M}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\Rightarrow P\vdash Q} +\inferrule*[Right={$\Rightarrow$L}]{\mpdotsabove{\Gamma \vdash M}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\Rightarrow P\vdash Q} }{\Gamma\vdash Q}$ } ~devient~ @@ -3024,7 +3024,7 @@ $\inferrule*[left={\color{purple}Cut}]{ $\inferrule*[left={\color{purple}Cut}]{ \mpdotsabove{\Gamma \vdash M} \\ -\inferrule*[right=\rlap{{\color{purple}Cut}}]{\mpdotsabove{\Gamma,M \vdash P}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\vdash Q} +\inferrule*[Right={{\color{purple}Cut}}]{\mpdotsabove{\Gamma,M \vdash P}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\vdash Q} }{\Gamma\vdash Q}$ } \end{center} |