diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 5c69859..e0e44b9 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -344,7 +344,7 @@ $\bot$ \\\hline $\forall$ &$\inferrule{\Gamma, {\color{mydarkgreen}v:I}\vdash Q}{\Gamma\vdash \forall (v:I).\, Q}$ ($v$ \alert{frais}) -&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall (v:I).\, Q}{\Gamma\vdash Q[v\backslash t]}$ +&$\inferrule{\Gamma\vdash \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash Q[v\backslash t]}$ \\\hline $\exists$ &$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$ @@ -401,7 +401,7 @@ type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize {\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme d'individu » $t$ est formé.)} \[ -\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]} +\inferrule{\Gamma\vdash f \;:\; \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash ft \;:\; Q[v\backslash t]} \] \medskip @@ -481,7 +481,7 @@ $\bot$ \\\hline $\forall$ &\scalebox{0.80}{$\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}$} -&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$} +&\scalebox{0.80}{$\inferrule{\Gamma\vdash f \;:\; \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$} \\\hline $\exists$ &\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$} @@ -855,7 +855,7 @@ $\bot$ \\\hline $\forall$ &$\inferrule{\Gamma, {\color{mydarkgreen}x:I}\vdash Q}{\Gamma\vdash \forall x.\, Q}$ ($x$ \alert{frais}) -&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall x.\, Q}{\Gamma\vdash Q[x\backslash t]}$ +&$\inferrule{\Gamma\vdash \forall x.\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash Q[x\backslash t]}$ \\\hline $\exists$ &$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x.\, Q}$ @@ -1420,7 +1420,7 @@ différent : $A_0 \rightarrow (\prod_n\,(A_n\rightarrow A_{n+1})) On peut souvent s'en faire une idée d'après son type, p.ex. : \begin{itemize} \item La commutativité de la multiplication $\forall m.\forall - m.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un + n.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un témoignage d'égalité de $m\times n$ et $n\times m$ (c'est-à-dire en fait $m\times n$ calculé de deux manières différentes). \item La preuve de $\forall n. (n=0 \lor \neg n=0)$ donnée |