diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 6 |
1 files changed, 5 insertions, 1 deletions
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 |