pcp in lc in haskell

pcp/lambda.hs

@@ -195,6 +195,8 @@ empty = Abs "a" (Abs "b" (Abs "x" (Var "x")))
 a = Abs "a" (Abs "b" (Abs "x" (App (Var "a") (Var "x"))))
 b = Abs "a" (Abs "b" (Abs "x" (App (Var "b") (Var "x"))))
 ab = Abs "a" (Abs "b" (Abs "x" (App (Var "a") (App (Var "b") (Var "x")))))
+bb = Abs "a" (Abs "b" (Abs "x" (App (Var "b") (App (Var "b") (Var "x")))))
+abb = Abs "a" (Abs "b" (Abs "x" (App (Var "a") (App (Var "b") (App (Var "b") (Var "x"))))))
 bba = Abs "a" (Abs "b" (Abs "x" (App (Var "b") (App (Var "b") (App (Var "a") (Var "x"))))))
 isempty = Abs "s" (App (App (App (Var "s") af) af) true)
 conc = Abs "y" (Abs "z" (Abs "a" (Abs "b" (Abs "x" (App (App (App (Var "y") (Var "a")) (Var "b")) (App (App (App (Var "z") (Var "a")) (Var "b")) (Var "x")))))))
@@ -233,8 +235,21 @@ p2 = App (App pair b) ab
 p3 = App (App pair a) bba
 pairs = App (App cons p1) (App (App cons p2) (App (App cons p3) nil))
 
+p12 = App (App pair abb) a
+p22 = App (App pair b) bb
+p32 = App (App pair a) b
+pairs2 = App (App cons p12) (App (App cons p22) (App (App cons p32) nil))
+
 simp = Abs "p" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App  (App (App ite (App (App lor (App isempty (Var "x"))) (App isempty (Var "y")))) (App (App pair (Var "x")) (Var "y"))) (App (App (Var "f") (App tl_str (Var "x"))) (App tl_str (Var "y")))))))) (App first (Var "p"))) (App second (Var "p")))
 
 pvalid = Abs "p" (App (App lor (App (App prefix (App first (Var "p"))) (App second (Var "p")))) (App (App prefix (App second (Var "p"))) (App first (Var "p"))))
 
-find_eq = App ycomb ()
+find_eq = App ycomb (Abs "f" (Abs "x" (App (App (App ite (App is_nil (Var "x"))) false) (App (App lor (App (App eq (App first (App hd_l (Var "x")))) (App second (App hd_l (Var "x"))))) (App (Var "f") (App tl_l (Var "y")))))))
+
+cmb = Abs "p" (Abs "q" (App (App pair (App (App conc (App second (Var "p"))) (App second (Var "q")))) (App (App conc (App second (Var "p"))) (App second (Var "q")))))
+
+map_cmb = App ycomb (Abs "f" (Abs "x" (Abs "y" ( App (App (App ite (App is_nil (Var "y"))) false) ( App (App (App ite (App pvalid (App (App cmb (Var "x")) (App hd_l (Var "y"))))) (App (App cons (App simp (App (App cmb (Var "x")) (App hd_l (Var "x"))))) (App (App (Var "f") (Var "x")) (App tl_l (Var "y"))))) (App (App (Var "f") (Var "x")) (App tl_l (Var "y"))) ) ))))
+
+cross_cmb = App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App is_nil (Var "y"))) nil) (App (App append (App (App map_cmb (App hd_l (Var "x"))) (Var "y"))) (App (App (Var "f") (App tl_l (Var "x"))) (Var "y")))))))
+
+pcp = Abs "x" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App is_nil (Var "x"))) false) (App (App (App ite (App find_eq (Var "x"))) true) (App (App (Var "f") (App (App cross_cmb (Var "x")) (Var "y"))) (Var "y")))))))) (Var "x")) (Var "x"))