From dc75f85146291c3b92d68884fc72b61dc3ec714c Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Thu, 7 Feb 2019 16:11:50 +0100
Subject: [PATCH] why3

---
 plceopen.mlw | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 plceopen.mlw

diff --git a/plceopen.mlw b/plceopen.mlw
new file mode 100644
index 0000000..e1b6cd0
--- /dev/null
+++ b/plceopen.mlw
@@ -0,0 +1,14 @@
+module PLCopen
+
+  predicate s8000
+  predicate a
+  predicate b
+  
+  axiom a: s8000 -> a /\ b 
+  
+  lemma la: not a -> not s8000
+  lemma lb: not b -> not s8000
+  
+  lemma lab: not a \/ not b -> not s8000
+  
+end
\ No newline at end of file
-- 
GitLab