From 94d58d4ac97a1f3574e70f6e4065cc83e38958cb Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 20 Jan 2024 19:13:36 +0100
Subject: Give another presentation of a proof in an exercise (at a student's
 request).

---
 exercices-inf110.tex | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index d7e258e..a8bf66a 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2384,6 +2384,76 @@ La revoici écrite dans le style « drapeau » :
 \end{footnotesize}
 \egroup
 
+La voici réécrite en forme d'arbre de preuve :
+\begin{tiny}
+\[
+\inferrule*[left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={$\land$Élim$_1$}]{
+\inferrule*[Left={Ax}]{
+}{\neg\neg A \land \neg\neg B \vdash \neg\neg A \land \neg\neg B}
+}{\neg\neg A \land \neg\neg B \vdash \neg\neg A}\\
+\inferrule*[Right={$\Rightarrow$Int}]{
+\inferrule*[Right={$\Rightarrow$Élim}]{
+\inferrule*[Left={$\land$Élim$_2$}]{
+\inferrule*[Left={Ax}]{
+}{\neg\neg A \land \neg\neg B \vdash \neg\neg A \land \neg\neg B}
+}{\neg\neg A \land \neg\neg B \vdash \neg\neg B}\\
+\inferrule*[Right={$\Rightarrow$Int}]{
+\inferrule*[Right={$\Rightarrow$Élim}]{
+\inferrule*[Left={Ax}]{ }{\neg (A\land B) \vdash \neg (A\land B)}\\
+\inferrule*[Right={$\land$Int}]{
+\inferrule*[Left={Ax}]{ }{A\vdash A}\\
+\inferrule*[Right={Ax}]{ }{B\vdash B}
+}{A, B \vdash A\land B}
+}{\neg (A\land B), A, B \vdash \bot}
+}{\neg (A\land B), A \vdash \neg B}
+}{\neg\neg A \land \neg\neg B, \neg (A\land B), A \vdash \bot}
+}{\neg\neg A \land \neg\neg B, \neg (A\land B) \vdash \neg A}
+}{\neg\neg A \land \neg\neg B, \neg (A\land B) \vdash \bot}
+}{\neg\neg A \land \neg\neg B \vdash \neg\neg (A\land B)}
+}{\vdash \neg\neg A \land \neg\neg B \Rightarrow \neg\neg (A\land B)}
+\]
+\end{tiny}
+
+Ou, avec uniquement les conclusions de chaque séquent (mais en
+indiquant, en contrepartie, à chaque décharge d'hypothèse, où cette
+hypothèse est déchargée : les lettres $h,k,h_1,h_2$ sont de tels
+renvois, et on a choisi les mêmes lettres que dans le terme de preuve
+écrit ci-dessous pour aider à la comparaison) :
+\begin{footnotesize}
+\[
+\inferrule*[left={$\Rightarrow$Int($h$)}]{
+\inferrule*[Left={$\Rightarrow$Int($k$)}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={$\land$Élim$_1$}]{
+\inferrule*[Left={$h$}]{
+}{\neg\neg A \land \neg\neg B}
+}{\neg\neg A}\\
+\inferrule*[Right={$\Rightarrow$Int($h_1$)}]{
+\inferrule*[Right={$\Rightarrow$Élim}]{
+\inferrule*[Left={$\land$Élim$_2$}]{
+\inferrule*[Left={$h$}]{
+}{\neg\neg A \land \neg\neg B}
+}{\neg\neg B}\\
+\inferrule*[Right={$\Rightarrow$Int($h_2$)}]{
+\inferrule*[Right={$\Rightarrow$Élim}]{
+\inferrule*[Left={$k$}]{ }{\neg (A\land B)}\\
+\inferrule*[Right={$\land$Int}]{
+\inferrule*[Left={$h_1$}]{ }{A}\\
+\inferrule*[Right={$h_2$}]{ }{B}
+}{A\land B}
+}{\bot}
+}{\neg B}
+}{\bot}
+}{\neg A}
+}{\bot}
+}{\neg\neg (A\land B)}
+}{\neg\neg A \land \neg\neg B \Rightarrow \neg\neg (A\land B)}
+\]
+\end{footnotesize}
+
 En Coq, cette preuve s'écrit :
 
 {\tt\noindent
-- 
cgit v1.2.3