Give two examples of natural deduction proofs (written in sequent style).

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}