From: acondolu <andrea.condoluci@unibo.it>
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