From 33062cbd72496b8d50858973ef8e64c3d8856554 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 23 Jun 2021 14:42:11 -0300
Subject: [PATCH] fixing sko_ex (bad formatting though)
---
spec/doc.tex | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index 84e9119..30f3167 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -1718,15 +1718,17 @@ The \currule{} rule skolemizes existential quantifiers.
\begin{plContainer}
\begin{plSubList}
\plLine\\
-\Gamma, x_1 \mapsto (\varepsilon x_1.\varphi), \dots , x_n \mapsto (\varepsilon x_n.\varphi)
-\proofsep& j.&
-\varphi \leftrightarrow \psi &(\dots)\\
+\Gamma, x_1 \mapsto (\varepsilon x_1. (\exists x_2, \dots, x_n. \varphi)), \dots , x_n \mapsto (\varepsilon
+x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{n-1}\mapsto \varepsilon_{n-1}])
+\proofsep& j.&\varphi \leftrightarrow \psi &(\dots)\\
\end{plSubList}
\begin{plList}
\Gamma \proofsep& k.&
\exists x_1, \dots, x_n.\varphi \leftrightarrow \psi &(\currule)\\
\end{plList}
\end{plContainer}
+where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
+x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{i-1}\mapsto\varepsilon_{i-1}])$
\end{proof-rule}
\begin{proof-rule}{sko_forall}{veriT}
--
GitLab