From f85e3343f8b1ecc1b1170448030b547ba199a90f Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 3 Apr 2020 17:49:36 +0200
Subject: [PATCH] PVS-Cert-

---
 encodings/pvs_cert_minus.lp | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 encodings/pvs_cert_minus.lp

diff --git a/encodings/pvs_cert_minus.lp b/encodings/pvs_cert_minus.lp
new file mode 100644
index 0000000..ee16fbe
--- /dev/null
+++ b/encodings/pvs_cert_minus.lp
@@ -0,0 +1,13 @@
+// PVS-Cert-, or ECC with only one universe
+require open personoj.encodings.lhol
+
+set declared "Σ"
+constant symbol Σ (T: Utype): (η T ⇒ Utype) ⇒ Utype
+constant symbol pair {T: Utype} {U: η T ⇒ Utype} (M: η T) (_: η (U M))
+: η (Σ T U)
+
+symbol fst {T: Utype} {U: η T ⇒ Utype}: η (Σ T U) ⇒ η T
+rule fst (pair &M _) → &M
+
+symbol snd {T: Utype} {U: η T ⇒ Utype} (M: η (Σ T U)): η (U (fst M))
+rule snd (pair _ &N) → &N
-- 
GitLab