From 8d989df63fbfdfa08bbcba4e982387075c8fd4d6 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 30 Nov 2023 19:00:58 +0100
Subject: Give two examples of natural deduction proofs (written in sequent
 style).

---
 transp-inf110-02-typage.tex | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

(limited to 'transp-inf110-02-typage.tex')

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
@@ -1377,6 +1377,47 @@ $\bot$
 {\footnotesize Les hypothèses en \textcolor{mydarkgreen}{vert} sont
   « déchargées ».\par}
 
+\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}
-- 
cgit v1.2.3