From: acondolu Date: Fri, 14 Jul 2017 17:28:29 +0000 (+0200) Subject: Parser.from_file, and p* problems moved to problems/p X-Git-Tag: weak-reduction-separation~35 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0b5ad58b1454d58219dca88bd1d3e94f14ac50fc;p=fireball-separation.git Parser.from_file, and p* problems moved to problems/p (cherry picked from commit 032edbca0cd6654adae5b5f06620723e74847435) --- diff --git a/ocaml/parser.ml b/ocaml/parser.ml index 9e0e809..a1a9d95 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -188,25 +188,16 @@ prerr_endline (s); aux' chr line in let _, name, div, conv, ps = List.fold_left aux ("#", "?", "", [], []) lines in let div_provided = div <> "" in - let div = if div_provided then div else "BOT" in + let div = if div_provided then div else "xxxxxx" in let strs = [div] @ ps @ conv in (* parse' *) let (tms, free) = parse_many strs in - (* Replace pacmans and bottoms *) - let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in - let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in - let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in - let fix lev v = - if v = lev + n_bot then assert false - else if v = lev + n_pac then assert false - else if v = lev + n_bomb then assert false - else `Var(v,1) in (* 1 by default when variable not applied *) (* Fix arity *) let open Num in let rec aux lev : nf -> nf = function | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> aux lev t) args) - | `Var(n,_) -> fix lev n + | `Var(n,_) -> `Var(n,1) | `Lam(_,t) -> `Lam (true, aux (lev+1) t) | `Match _ | `N _ -> assert false in let all_tms = List.map (aux 0) (tms :> Num.nf list) in @@ -232,3 +223,18 @@ let ps = List.map ( ) ps in name, div, conv, ps, free ;; + + +let from_file path = + let lines = ref [] in + let chan = open_in path in + let _ = try + while true; do + lines := input_line chan :: !lines + done + with End_of_file -> + close_in chan in + let txt = String.concat "\n" (List.rev !lines) in + let problems = Str.split (Str.regexp "\r?\n\r?\n\\#") txt in + List.map problem_of_string problems +;; diff --git a/ocaml/parser.mli b/ocaml/parser.mli index 9275067..47cfb28 100644 --- a/ocaml/parser.mli +++ b/ocaml/parser.mli @@ -8,3 +8,9 @@ val problem_of_string: * Num.i_n_var list (* conv *) * Num.i_n_var list (* ps *) * string list (* names of free variables *) +val from_file : string -> + (string (* problem label *) + * Num.i_var option (* div *) + * Num.i_n_var list (* conv *) + * Num.i_n_var list (* ps *) + * string list (* names of free variables *)) list diff --git a/ocaml/problems.ml b/ocaml/problems.ml index e01a741..3995496 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -21,107 +21,7 @@ let solve_many = List.iter assert_separable;; (* div under a lambda in conv *) (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *) -assert_unseparable (problem_of None [] (* 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)))))))" - ]);; - -(* p-series problems *) -let f x = assert_separable (problem_of None [] x) in -List.iter f [ - (* 2 *) [ "x y"; "x z" ; "x (y z)"]; - (* 4 *) [ "x y"; "x (a. a x)" ; "y (y z)" ]; - (* 5 *) ["a (x. x a) b"; "b (x. x b) a"]; - (* 6 *) ["a (x. x a) b"; "b (x. x b) (c a)"]; - (* 7 *) ["a (x. (x a) (a x x a) (x x) )"]; - (* 8 *) ["x x (x x)"]; - (* 9 *) ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]; - (* 10 *) ["x (y (x a b c))"]; - (* 11 *) ["x x"; "x (y.y)"]; - (* 12 *) ["x x (x x)"; "x x (x (y.y))"]; - (* 13 *) ["x x (x x (x x x x x (x x)))"]; - (* 14 *) ["a (a a (a (a a)) (a (a a)))"]; - (* 15 *) ["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)))"]; - (* 16 *) ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]; - (* 17 *) ["b a"; "b (c.a)"]; - (* 18 *) ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]; - (* 19 *) ["a (a a) (a a a (a (a (a a) a)) a)"]; - (* 20 *) ["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)))))"]; - (* 21 *) - ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))"; - "(((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))"]; - (* 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"]; -];; +List.iter (assert_separable ++ Lambda4.tmp) (Parser.from_file "problems/p");; (* q-series problems *) diff --git a/ocaml/problems/p b/ocaml/problems/p new file mode 100644 index 0000000..5e7283c --- /dev/null +++ b/ocaml/problems/p @@ -0,0 +1,170 @@ +# p2 +N x y + x z + x (y z) + +# p4 +N x y + x (a. a x) + y (y z) + +# p5 +N a (x. x a) b + b (x. x b) a + +# p6 +N a (x. x a) b + b (x. x b) (c a) + +# p7 +N a (x. (x a) (a x x a) (x x) ) + +# p8 +N x x (x x) + +# p9 +N x x (x x x) (x x (x x)) (x x (x x x)) x x + +# p10 +N x (y (x a b c)) + +# p11 +N x x + x (y.y) + +# p12 +N x x (x x) + x x (x (y.y)) + +# p13 +N x x (x x (x x x x x (x x))) + +# p14 +N a (a a (a (a a)) (a (a a))) + +# p15 +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))) + +# p16: +N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) + +# p17 +N b a + b (c.a) + +# p18 +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) + +# p19 +N a (a a) (a a a (a (a (a a) a)) a) + +# p20 +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))))) + +# p21 +N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) + (((z z) x) (y z)) + ((z (y z)) ((y z) (z z))) + +# p22 +N ((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)))) + +# p23 + (* diverging tests *) (* test p23 leads to test p24 *) +N z z z + z (z z) (x. x) + +# p24 + (* 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 *) +N b b + b f + f b + a (x.x) + +# p25 + (* 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 *) +N b b + b f + f b + f (x.x) + +# p26 + (* BUG: + 0 (n (d (o.n) ...))) + After instantiating n, the magic number (for d) should be 2, not 1! *) +N (((x y) (z. (y. (y. z)))) (z. y)) + (((x y) x) (y y)) + +# p27 +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 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)) + +# p28 +N ((((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))))) + +# p29 +N ((((((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) + +# p30 +N ((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))) + +# p31 +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))) + ((((((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)) + +# p32 +N (((((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))))))) + +# p33 + (* Shows an error when the strategy that minimizes special_k is NOT used *) +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))))))) + ((((((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))))))" *) + +# p34 +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 + 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 + +# p35 +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))))))) + ((((((((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))) + +# p36 +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 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)) + + +# p37 + issue with eta-equality of terms in ps +N x (a y) z + x (a z. y z) w + a c