]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems/o
Important: added special variable "Z" for zero.
[fireball-separation.git] / ocaml / problems / o
diff --git a/ocaml/problems/o b/ocaml/problems/o
new file mode 100644 (file)
index 0000000..95c3c3d
--- /dev/null
@@ -0,0 +1,21 @@
+$! o1\r
+N x a b Z\r
+  x (_. BOT) c Z\r
+\r
+$! o2\r
+N x (y (_. BOT) a) c Z\r
+  x (y a PAC) d Z\r
+\r
+$! o3\r
+D y (x a1 BOMB c) (x BOMB b1 d)\r
+C y (x a2 BOMB c) (x BOMB b1 d)\r
+  y (x a1 BOMB c) (x BOMB b2 d)\r
+\r
+\r
+$! o4\r
+D x BOMB a1 c\r
+  x y BOMB d\r
+\r
+$! o6\r
+D x BOMB\r
+C x y\r