- "(((z z) x) (y z))";
- "((z (y z)) ((y z) (z z)))"
-] ;;
-
-let p22 = magic
-["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
-"((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)))))";
-"(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ;;
-
-(* diverging tests *)
-(* test p23 leads to test p24 *)
-let p23 = magic
-["z z z"; "z (z z) (x. x)"] ;;
-
-(* because of the last term, the magic number is 1 and we diverge;
- but setting the magic number to 0 allows to solve the problem;
- thus our strategy is incomplete *)
-let p24 = magic
-["b b"; "b f"; "f b"; "a (x.x)"] ;;
-
-(* because of the last term, the magic number is 1 and we diverge;
- but setting the magic number to 0 allows to solve the problem;
- thus our strategy is incomplete *)
-let p25 = magic
-["b b"; "b f"; "f b"; "f (x.x)"] ;;
-
-(* BUG:
- 0 (n (d (o.n) ...)))
- After instantiating n, the magic number (for d) should be 2, not 1! *)
-let p26 = magic
-["(((x y) (z. (y. (y. z)))) (z. y))";
-"(((x y) x) (y y))"] ;;
-
-let p27 = magic
-["(((((((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 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))"] ;;
-
-let p28 = magic
-["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
- "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ;;
-
-let p29 = magic
-["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
-"(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ;;
-
-let p30 = magic
-["((b c) (b. (z a)))";
-"((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
-"((v (v. c)) z)";
-"((v y) (v (a. (z v))))";
-"((y (b c)) ((z a) (v y)))"] ;;
-
-let p31 = magic
-[" (((((((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)))";
-"((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
-"(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
-"(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
-"((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ;;
-
-let p32 = magic
-["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
-"(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
-"(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
-"((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
-"((((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)))))))"
-] ;;
-
-(* Shows an error when the strategy that minimizes special_k is NOT used *)
-let p33 = magic
-[
-"((((((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)))))))";
-"((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))";
-"(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
-"(((((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))))";
-(* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
-] ;;
-
-let p34 = magic [
-"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";
-"d (j. e) e (j. c f) (j. c j) b a";
-"d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
-"d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
-"d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";
-] ;;
-(* 0: (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)
-1: (d j.e e j.(c f) j.(c j) b a)
-2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a)
-3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a)
-4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *)
-
-let p35 = magic [
-"(((((((((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)))))))";
-"((((((((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))))))))))";
-"((((((((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)))"
-] ;;
-
-let p36 = magic
-[
-"(((((((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 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 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))"
-] ;;
-
-(* issue with eta-equality of terms in ps *)
-let p37 = magic
- ["x (a y) z"; "x (a z. y z) w"; "a c"]
- ;;
-
-(**********************)
+ "(((z z) x) (y z))";
+ "((z (y z)) ((y z) (z z)))"];
+ (* 22 *)
+ ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
+ "((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)))))";
+ "(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"];
+ (* 23 *) (* diverging tests *) (* test p23 leads to test p24 *)
+ ["z z z"; "z (z z) (x. x)"];
+ (* 24 *)
+ (* because of the last term, the magic number is 1 and we diverge;
+ but setting the magic number to 0 allows to solve the problem;
+ thus our strategy is incomplete *)
+ ["b b"; "b f"; "f b"; "a (x.x)"];
+ (* 25 *)
+ (* because of the last term, the magic number is 1 and we diverge;
+ but setting the magic number to 0 allows to solve the problem;
+ thus our strategy is incomplete *)
+ ["b b"; "b f"; "f b"; "f (x.x)"];
+ (* 26 *)
+ (* BUG:
+ 0 (n (d (o.n) ...)))
+ After instantiating n, the magic number (for d) should be 2, not 1! *)
+ ["(((x y) (z. (y. (y. z)))) (z. y))";
+ "(((x y) x) (y y))"];
+ (* 27 *)
+ ["(((((((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 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))"];
+ (* 28 *)
+ ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
+ "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ];
+ (* 29 *)
+ ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
+ "(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"];
+ (* 30 *)
+ ["((b c) (b. (z a)))";
+ "((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
+ "((v (v. c)) z)";
+ "((v y) (v (a. (z v))))";
+ "((y (b c)) ((z a) (v y)))"];
+ (* 31 *)
+ [" (((((((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)))";
+ "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
+ "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
+ "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
+ "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"];
+ (* 32 *)
+ ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
+ "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
+ "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
+ "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
+ "((((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)))))))"
+ ];
+ (* 33 *)
+ (* Shows an error when the strategy that minimizes special_k is NOT used *)
+ [ "((((((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)))))))";
+ "((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))";
+ "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
+ "(((((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))))";
+ (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *) ];
+ (* 34 *)
+ [ "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";
+ "d (j. e) e (j. c f) (j. c j) b a";
+ "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
+ "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
+ "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";];
+ (* 35 *)
+ [ "(((((((((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)))))))";
+ "((((((((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))))))))))";
+ "((((((((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)))"];
+ (* 36 *)
+ [ "(((((((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 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 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))"];
+ (* 37 *) (* issue with eta-equality of terms in ps *)
+ ["x (a y) z"; "x (a z. y z) w"; "a c"];
+
+]);;
+
+(* q-series problems *)