diff options
| author | David A. Madore <david+git@madore.org> | 2024-01-12 18:29:40 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2024-01-12 18:29:40 +0100 |
| commit | 74f351825595cef97c9d4a62e3c1a7d827fdc06c (patch) | |
| tree | d12c8cacd7f11279262e94ee3944530f677fd0ff | |
| parent | d2c6749c7a37fc1f240613d3d618908ecabcd558 (diff) | |
| download | inf110-lfi-74f351825595cef97c9d4a62e3c1a7d827fdc06c.tar.gz inf110-lfi-74f351825595cef97c9d4a62e3c1a7d827fdc06c.tar.bz2 inf110-lfi-74f351825595cef97c9d4a62e3c1a7d827fdc06c.zip | |
Be more consistent about abbreviating logical rules.
| -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} |