why3

plceopen.mlw

+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