diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 8ee4ae4..d7483b1 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1379,4 +1379,45 @@ $\bot$ \end{frame} % +\begin{frame} +\frametitle{Exemples de démonstration} + +{\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} +}{A\land B \vdash B} +\\ +\inferrule*[right=\rlap{$\land$Élim$_1$}]{ +\inferrule*[right=\rlap{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} +\] +\par} + +\bigskip + +{\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*[right={$\lor$Int$_2$}]{ +\inferrule*[right=\rlap{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} +}{A\lor B,B \vdash B\lor A} +}{A\lor B \vdash B\lor A} +}{\vdash A\lor B \Rightarrow B\lor A} +\] +\par} + +\end{frame} +% \end{document} |