]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems/q
Important: added special variable "Z" for zero.
[fireball-separation.git] / ocaml / problems / q
index 9f432359bc657bf8dacd280f02cefed96d7aac07..01ec75481a6b387f681f19b2d49f1a56cb82480a 100644 (file)
@@ -1,20 +1,20 @@
 $! q1\r
 C a d e\r
-N a b\r
-  a c\r
+N a b Z\r
+  a c Z\r
 \r
 $! q2\r
 C a d e\r
-N a b\r
+N a b Z\r
 \r
 $! q3\r
 D x y\r
 C a d e f\r
-N a b\r
+N a b Z\r
 \r
 $! q4\r
 C f (x.a b c d)\r
-N a b\r
+N a b Z\r
 \r
 $! q5\r
 D x y\r
@@ -24,28 +24,28 @@ N x
 $! q6\r
 D x w\r
 C (y. x z)\r
-N y\r
+N y Z\r
 \r
 $! q7\r
 D (b (c d (e f f k.(g e))) f)\r
 C (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (f d k.g (b (g (e f)) (b (g (e f)) (e f)) (g (e f) (g e h)))) k.l.(h f (b i)))\r
   (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (b (g (e f))) k.l.(g f (k f f (k f f m.(g k)))))\r
   (b (g (e f)) f k.e k.l.(f d (e f)) (c d (e f f k.(g e)) (g k.(e f f))) (h f (i (h k.(i b l.m.n.e)))))\r
-N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)\r
-  (f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a)\r
-  (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a)\r
+N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a) Z\r
+  (f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a) Z\r
+  (g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a) Z\r
 \r
 ################################################################################\r
 \r
 $! q8\r
 D x a\r
 C y (x b c)\r
-N j\r
+N j Z\r
 \r
 $! q9\r
 D x a\r
 C y x\r
-N a (y a b b b)\r
+N a (y a b b b) Z\r
 \r
 $! q11\r
 D x y\r
@@ -59,8 +59,8 @@ C e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c))) (c f (k. b (l. c)) (k.
   b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (b (k. c) (k. e) (k. l. m. b (n. c))) (e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k)))\r
   b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f) (k. e (f g)))\r
 \r
-N b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))\r
-  b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h))\r
-  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f)\r
-  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)\r
-  e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))\r
+N b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e))) Z\r
+  b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h)) Z\r
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f) Z\r
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b) Z\r
+  e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e))) Z\r