summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2024-01-20 19:18:21 +0100
committerDavid A. Madore <david+git@madore.org>2024-01-20 19:18:21 +0100
commit7581f4907dd6af33345dc7b85fb8447e0f8c10e5 (patch)
tree40fed93de3e1a5b3bd2312e780756fe9295350d4
parent94d58d4ac97a1f3574e70f6e4065cc83e38958cb (diff)
downloadinf110-lfi-7581f4907dd6af33345dc7b85fb8447e0f8c10e5.tar.gz
inf110-lfi-7581f4907dd6af33345dc7b85fb8447e0f8c10e5.tar.bz2
inf110-lfi-7581f4907dd6af33345dc7b85fb8447e0f8c10e5.zip
Clarification over previous addition.
-rw-r--r--exercices-inf110.tex5
1 files changed, 4 insertions, 1 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index a8bf66a..2f00df0 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2384,7 +2384,10 @@ La revoici écrite dans le style « drapeau » :
\end{footnotesize}
\egroup
-La voici réécrite en forme d'arbre de preuve :
+La voici réécrite en forme d'arbre de preuve (en omettant certaines
+hypothèses superflues à gauche du symbole ‘$\vdash$’, ou, ce qui
+revient au même, en faisant un usage tacite de la règle
+d'affaiblissement) :
\begin{tiny}
\[
\inferrule*[left={$\Rightarrow$Int}]{