From b620eb841333f53f725cbad829e57142a0c72e73 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 11:09:18 +0100
Subject: A few more important tautologies.

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

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

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 06473c2..3178d29 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1519,9 +1519,12 @@ Quelques tautologies importantes (« $P\Leftrightarrow Q$ » abrège
 
 \begin{tabular}{|c|c|}
 \hline
-$A\Rightarrow B\Rightarrow A$&$(A\Rightarrow B\Rightarrow C)
+$A\Rightarrow A$\quad\quad\quad $A\Rightarrow B\Rightarrow A$&$(A\Rightarrow B\Rightarrow C)
 \Rightarrow (A\Rightarrow B)\Rightarrow A\Rightarrow C$\\
 \hline
+$(A\Rightarrow B\Rightarrow C) \Leftrightarrow (A\land B \Rightarrow C)$
+&$A\land A \mathrel{\color{olive}\Leftrightarrow} A$\quad\quad\quad$A\lor A \mathrel{\color{olive}\Leftrightarrow} A$\\
+\hline
 $A\land B \Rightarrow A$\quad\quad\quad$A\land B \Rightarrow B$&$A\Rightarrow A\lor B$\quad\quad\quad$B \Rightarrow A\lor B$\\
 \hline
 $A\Rightarrow B\Rightarrow A\land B$&$(A\Rightarrow C)\Rightarrow(B\Rightarrow C)\Rightarrow A\lor B\Rightarrow C$\\
@@ -1854,6 +1857,7 @@ juste qu'il « existe » classiquement.
 \end{frame}
 %
 % TODO:
+% - Brouwer-Heyting-Kolmogorov
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences
 % - Curry-Howard
-- 
cgit v1.2.3

