From 3818b12ffc9382f6d273b8b9e9eb2d0384d1b19e Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 21 Apr 2020 14:30:45 +0200
Subject: [PATCH] prenex notations (adapted to lambdapi issue)

---
 encodings/prenex.lp | 16 +++++++++-------
 paper/equal.lp      |  4 ++--
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index b6222b0..1c798ad 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -3,14 +3,16 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
 set declared "χ"
-set declared "∇"
+set declared "∀S"
+set declared "∀B"
+
 symbol Scheme: TYPE
 symbol χ: Scheme → TYPE
-symbol ∇: Set → Scheme
-rule χ (∇ $X) ↪ η $X
+symbol scheme: Set → Scheme
+rule χ (scheme $X) ↪ η $X
 
-constant symbol forallS: (Set → Scheme) → Scheme
-rule χ (forallS $p) ↪ ΠT: Set, χ ($p T)
+constant symbol ∀S: (Set → Scheme) → Scheme
+rule χ (∀S $p) ↪ ΠT: Set, χ ($p T)
 
-constant symbol forallB: (Set → Bool) → Bool
-rule ε (forallB $P) ↪ Πx: Set, ε ($P x)
+constant symbol ∀B: (Set → Bool) → Bool
+rule ε (∀B $P) ↪ Πx: Set, ε ($P x)
diff --git a/paper/equal.lp b/paper/equal.lp
index d65d092..7bd1476 100644
--- a/paper/equal.lp
+++ b/paper/equal.lp
@@ -1,5 +1,5 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require personoj.encodings.prenex as P
+require open personoj.encodings.prenex
 
-symbol eq: P.χ (P.forallS (λT: ϕ {|set|}, P.∇ (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: ϕ {|set|}, scheme (T ~> T ~> bool)))
-- 
GitLab