From e76ff9b3cd8e1c9e2b189bd740ebf3ff688e6e6a Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 2 Dec 2023 17:19:31 +0100
Subject: Another presentation of natural deduction proofs.

---
 transp-inf110-02-typage.tex | 51 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 49 insertions(+), 2 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index d7483b1..3746973 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1344,7 +1344,7 @@ Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$.
 
 \medskip
 
-Introduction et élimination des connecteurs (style « déduction naturelle ») :
+Introduction et élimination des connecteurs en style « déduction naturelle » :
 
 \smallskip
 
@@ -1375,7 +1375,7 @@ $\bot$
 \end{tabular}
 
 {\footnotesize Les hypothèses en \textcolor{mydarkgreen}{vert} sont
-  « déchargées ».\par}
+  « déchargées », c'est-à-dire qu'elles disparaissent.\par}
 
 \end{frame}
 %
@@ -1418,6 +1418,53 @@ $\bot$
 \]
 \par}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Présentation différente}
+
+On peut aussi n'écrire que les conclusions (partie droite du
+signe $\vdash$), à condition d'indiquer pour chaque hypothèse
+déchargée à quel endroit elle l'a été :
+
+\bigskip
+
+{\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}
+}{B}
+\\
+\inferrule*[right=\rlap{$\land$Élim$_1$}]{
+\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
+}{A}
+}{B\land A}
+}{A\land B \Rightarrow B\land A}
+\]
+\par}
+
+\bigskip
+
+{\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*[right={$\lor$Int$_2$}]{
+\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v$}}]{ }{A}
+}{B\lor A}
+\\
+\inferrule*[right=\rlap{$\lor$Int$_1$}]{
+\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v'$}}]{ }{B}
+}{B\lor A}
+}{B\lor A}
+}{A\lor B \Rightarrow B\lor A}
+\]
+\par}
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3