\r
$! p2\r
-N x y\r
- x z\r
- x (y z)\r
+N x y Z\r
+ x z Z\r
+ x (y z) Z\r
\r
$! p4\r
-N x y\r
- x (a. a x)\r
- y (y z)\r
+N x y Z\r
+ x (a. a x) Z\r
+ y (y z) Z\r
\r
$! p5\r
-N a (x. x a) b\r
- b (x. x b) a\r
+N a (x. x a) b Z\r
+ b (x. x b) a Z\r
\r
$! p6\r
-N a (x. x a) b\r
- b (x. x b) (c a)\r
+N a (x. x a) b Z\r
+ b (x. x b) (c a) Z\r
\r
$! p7\r
-N a (x. (x a) (a x x a) (x x) )\r
+N a (x. (x a) (a x x a) (x x) ) Z\r
\r
$! p8\r
-N x x (x x)\r
+N x x (x x) Z\r
\r
$! p9\r
-N x x (x x x) (x x (x x)) (x x (x x x)) x x\r
+N x x (x x x) (x x (x x)) (x x (x x x)) x x Z\r
\r
$! p10\r
-N x (y (x a b c))\r
+N x (y (x a b c)) Z\r
\r
$! p11\r
-N x x\r
- x (y.y)\r
+N x x Z\r
+ x (y.y) Z\r
\r
$! p12\r
-N x x (x x)\r
- x x (x (y.y))\r
+N x x (x x) Z\r
+ x x (x (y.y)) Z\r
\r
$! p13\r
-N x x (x x (x x x x x (x x)))\r
+N x x (x x (x x x x x (x x))) Z\r
\r
$! p14\r
-N a (a a (a (a a)) (a (a a)))\r
+N a (a a (a (a a)) (a (a a))) Z\r
\r
$! p15\r
-N a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))\r
+N a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a))) Z\r
\r
$! p16:\r
-N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))\r
+N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) Z\r
\r
$! p17\r
-N b a\r
- b (c.a)\r
+N b a Z\r
+ b (c.a) Z\r
\r
$! p18\r
-N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))\r
- a a\r
- a (a a)\r
+N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) Z\r
+ a a Z\r
+ a (a a) Z\r
\r
$! p19\r
-N a (a a) (a a a (a (a (a a) a)) a)\r
+N a (a a) (a a a (a (a (a a) a)) a) Z\r
\r
$! p20\r
-N a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))\r
+N a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b))))) Z\r
\r
$! p21\r
-N (((y z) (y z)) ((z (y z)) ((y z) (z z))))\r
- (((z z) x) (y z))\r
- ((z (y z)) ((y z) (z z)))\r
+N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) Z\r
+ (((z z) x) (y z)) Z\r
+ ((z (y z)) ((y z) (z z))) Z\r
\r
$! p22\r
-N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))\r
- ((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))\r
- (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))\r
+N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z\r
+ ((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z))))) Z\r
+ (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z\r
\r
$! p23\r
# (* diverging tests *) (* test p23 leads to test p24 *)\r
-N z z z\r
- z (z z) (x. x)\r
+N z z z Z\r
+ z (z z) (x. x) Z\r
\r
$! p24\r
# (* because of the last term, the magic number is 1 and we diverge\r
but setting the magic number to 0 allows to solve the problem\r
thus our strategy is incomplete *)\r
-N b b\r
- b f\r
- f b\r
- a (x.x)\r
+N b b Z\r
+ b f Z\r
+ f b Z\r
+ a (x.x) Z\r
\r
$! p25\r
# (* because of the last term, the magic number is 1 and we diverge\r
but setting the magic number to 0 allows to solve the problem\r
thus our strategy is incomplete *)\r
-N b b\r
- b f\r
- f b\r
- f (x.x)\r
+N b b Z\r
+ b f Z\r
+ f b Z\r
+ f (x.x) Z\r
\r
$! p26\r
(* BUG:\r
0 (n (d (o.n) ...)))\r
After instantiating n, the magic number (for d) should be 2, not 1! *)\r
-N (((x y) (z. (y. (y. z)))) (z. y))\r
- (((x y) x) (y y))\r
+N (((x y) (z. (y. (y. z)))) (z. y)) Z\r
+ (((x y) x) (y y)) Z\r
\r
$! p27\r
-N (((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))\r
- ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))\r
- (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))\r
+N (((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))) Z\r
+ ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) Z\r
+ (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) Z\r
\r
$! p28\r
-N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))\r
- (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))\r
+N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z\r
+ (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z\r
\r
$! p29\r
-N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))\r
- (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)\r
+N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z\r
+ (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z\r
\r
$! p30\r
-N ((b c) (b. (z a)))\r
- ((v (a. (z v))) ((y (b c)) ((z a) (v y))))\r
- ((v (v. c)) z)\r
- ((v y) (v (a. (z v))))\r
- ((y (b c)) ((z a) (v y)))\r
+N ((b c) (b. (z a))) Z\r
+ ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z\r
+ ((v (v. c)) z) Z\r
+ ((v y) (v (a. (z v)))) Z\r
+ ((y (b c)) ((z a) (v y))) Z\r
\r
$! p31\r
-N (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))\r
- ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))\r
- (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))\r
- (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))\r
- ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))\r
-\r
-$! p32\r
-N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))\r
- (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)\r
- (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))\r
- ((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))\r
- ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))\r
+N (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c))) Z\r
+ ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z\r
+ (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z\r
+ (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z\r
+ ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z\r
+\r
+$? p32\r
+# should fail because the first and second terms are eta-eq\r
+N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z\r
+ (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z\r
+ (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z\r
+ ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z\r
+ ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a))))))) Z\r
\r
$! p33\r
(* Shows an error when the strategy that minimizes special_k is NOT used *)\r
-N ((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))\r
- ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))\r
- (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))\r
- (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))\r
+N ((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y))))))) Z\r
+ ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) Z\r
+ (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) Z\r
+ (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w)))) Z\r
# (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)\r
\r
$! p34\r
-N b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a\r
- d (j. e) e (j. c f) (j. c j) b a\r
- d (j. e) e (j. c f) b (b c (b c) (j. c f)) a\r
- d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a\r
- d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a\r
+N b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a Z\r
+ d (j. e) e (j. c f) (j. c j) b a Z\r
+ d (j. e) e (j. c f) b (b c (b c) (j. c f)) a Z\r
+ d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a Z\r
+ d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a Z\r
\r
$! p35\r
-N (((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))\r
- ((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))\r
- ((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))\r
+N (((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y))))))) Z\r
+ ((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) Z (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))))))) Z\r
+ ((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y))) Z\r
\r
$! p36\r
-N (((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))))))))\r
- (((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))\r
- (((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))\r
+N (((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))))) Z\r
+ (((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v))) Z\r
+ (((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x)) Z\r
\r
\r
$! p37\r
issue with eta-equality of terms in ps\r
-N x (a y) z\r
- x (a z. y z) w\r
- a c\r
+N x (a y) z Z\r
+ x (a z. y z) w Z\r
+ a c Z\r
projects / fireball-separation.git / blobdiff