X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems%2Fbugs;h=610b6b8549ff7982ae4d5e444379e53554f78986;hb=7d5ab4339cbbe0c694e6f7376bd92b9a19f5b98d;hp=2cea8d33b028e4de462c21679af1330faf9a0a0d;hpb=42eb14bc4443ce5a9bb893654db97a9c41486f06;p=fireball-separation.git

diff --git a/ocaml/problems/bugs b/ocaml/problems/bugs
index 2cea8d3..610b6b8 100644
--- a/ocaml/problems/bugs
+++ b/ocaml/problems/bugs
@@ -1,12 +1,10 @@
-$! randomly generated test
-D ((((z b) (w v)) (v. (v z))) (a. (v y)))
-C (((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b))))) ((y (y. (c v))) w))
-C ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((z b) (w v)) y))
-C ((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b)))))
-C ((((((y v) v) ((z b) (w v))) c) c) (((((z b) (w v)) (v. (v z))) (a. (v x))) v))
-C (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a))
-N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((c (w v)) ((w v) z)) (c w))) Z
-N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (c. (((c v) ((c w) (b. a))) (v. (c. (w. b)))))) Z
-N ((((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v)))) (y. (c. ((((y v) v) (z. (y. (w. (b b))))) (((z b) (w v)) (v. (v z))))))) (z. (y. (b. a)))) Z
-N (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (((y v) v) ((z b) (w v)))) Z
-N (((((b b) (a. (y v))) (a. (b. (b b)))) (((w v) z) (y. (c v)))) (y. (c. c))) Z
+$! bugs 1
+# bug with eating firing reduction of matches
+D z (_. (v y))
+C u (z (_. (v x)))
+
+$! bugs 2
+# algorithm tries to eat z, but should first step on x, w
+D z PAC
+C x y PAC PAC
+N x (w z) Z