diff options
Diffstat (limited to 'transp-inf110-03-quantif.tex')
| -rw-r--r-- | transp-inf110-03-quantif.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index e0e44b9..08001c0 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -928,8 +928,8 @@ Présentation avec les seules conclusions : \step{bare}{B(x,y')}{$\forall$Élim sur \ref{exhyp} et $y$} \step{exbare}{\exists x'.B(x',y')}{$\exists$Int sur $x$ et \ref{bare}} \conclude{extrude}{\exists x'.B(x',y')}{$\exists$Elim sur \ref{mainhyp} de \ref{exhyp} dans \ref{exbare}} -\conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Intro de \ref{vary} dans \ref{extrude}} -\conclude{}{(\exists x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists x'.B(x',y'))}{$\Rightarrow$Intro de \ref{mainhyp} dans \ref{mainconc}} +\conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Int de \ref{vary} dans \ref{extrude}} +\conclude{}{(\exists x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists x'.B(x',y'))}{$\Rightarrow$Int de \ref{mainhyp} dans \ref{mainconc}} \end{flagderiv} \par} |