diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index f3e8b1d..35425f0 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2675,22 +2675,19 @@ droite \alert{ou à gauche} du symbole « $\vdash$ ». \medskip \itempoint On garde la règle $\inferrule*[left=Ax]{ }{\Gamma,Q \vdash - Q}$, qu'on peut choisir de séparer en : + Q}$, ou on peut en séparer une règle d'qffaibilissement ; et on va +reparler des règles de « contraction » et « coupure » : + \begin{center} -\begin{tabular}{c|c|c} +\begin{tabular}{c|c} $\inferrule*[left=Ax]{ }{Q \vdash Q}$ &$\inferrule*[left=Weak]{\Gamma \vdash Q}{\Gamma,P\vdash Q}$ -&$\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$ +\\\hline +$\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$ +&$\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}$ \end{tabular} \end{center} -\medskip - -\itempoint On va reparler de la règle de « coupure » : -\[ -\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q} -\] - \end{frame} % \begin{frame} |