From 74f351825595cef97c9d4a62e3c1a7d827fdc06c Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Fri, 12 Jan 2024 18:29:40 +0100 Subject: Be more consistent about abbreviating logical rules. --- transp-inf110-03-quantif.tex | 4 ++-- 1 file 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} -- cgit v1.2.3