Commit 6ba3bce5 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

pcp using lists

parent 918f77e5
......@@ -841,7 +841,14 @@ let rec sn_reduce_with_paths_to_nf term max_depth sim =
if newterm = term then []
else term :: sn_reduce_with_paths_to_nf newterm max_depth sim
let rec size term =
match term with
| AVar (s, t) -> 0
| ALam ((xs, e), t) -> 1 + size e
| AApp (e1, e2, t) -> 1 + size e1 + size e2
let rec nf subst term =
(* Printf.printf "%d\n" (size term); *)
let new_term = reduce_lo subst term in
if new_term = term then term else nf subst new_term
......
......@@ -4,53 +4,176 @@ This terms can be used to test and experiment. *)
open Alpha
let tree_of_string s = Grammar.input Lexer.token (Lexing.from_string (s^"\n"))
let t_ite = tree_of_string "/c a b.c a b"
let t_true = tree_of_string "/x y.x"
let t_false = tree_of_string "/x y.y"
let t_pair = tree_of_string "/a b c.c a b"
let t_first = tree_of_string "/p.p (/x y.x)"
let t_second = tree_of_string "/p.p (/x y.y)"
let t_empty = tree_of_string "/x a b.x"
let t_at = tree_of_string "/x./x y.x"
let t_af = tree_of_string "/x./x y.y"
let t_concat = tree_of_string "/y z x a b.y (z x a b) a b"
let t_isempty = tree_of_string "/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)"
let t_prepa = tree_of_string "/s x a b.a (s x a b)"
let t_prepb = tree_of_string "/s x a b.b (s x a b)"
let t_nexta = tree_of_string "/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)"
let t_nextb = tree_of_string "/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)"
let t_tl = tree_of_string "/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))"
let t_hd = tree_of_string "/s x a b.s x (/y.a x) (/y.b x)"
let t_hd_a = tree_of_string "/s.s (/x y.y) (/x./x y.x) (/x./x y.y)"
let t_hd_b = tree_of_string "/s.s (/x y.y) (/x./x y.x) (/x./x y.x)"
let t_is_e = tree_of_string "/s.s (/x y.x) (/x./x y.y) (/x./x y.y)"
let t_and = tree_of_string "/x y.x y x"
let t_or = tree_of_string "/x y.x x y"
let t_hd_eq = tree_of_string "/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))"
let t_ycomb = tree_of_string "/f.(/x.f (x x)) (/x.f (x x))"
let t_zcomb = tree_of_string "/f.(/x.f (/y.x x y)) (/x.f (/y.x x y))"
let s_e = tree_of_string "/x a b.x"
let s_a = tree_of_string "/x a b.a x"
let s_b = tree_of_string "/x a b.b x"
let s_ab = tree_of_string "/x a b.a (b x)"
let s_aa = tree_of_string "/x a b.a (a x)"
let s_ba = tree_of_string "/x a b.b (a x)"
let s_baba = tree_of_string "/x a b.b (a (b (a x)))"
(* let _all_a = tree_of_string "/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x)))"
let all_a = tree_of_string "/a.(/f.(/x.f (/y.x x y)) (/x.f (/y.x x y))) (/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x)))) a" *)
let _eq_str = tree_of_string "/rec x y.(/c a b.c a b) ((/x y.x x y) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))) x y) (rec ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x) ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) y)))";;
let eq_str = tree_of_string "/a b.(/f.(/x.f (x x)) (/x.f (x x))) (/rec x y.(/c a b.c a b) ((/x y.x x y) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))) x y) (rec ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x) ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) y)))) a b";;
let s_ite = "(/c a b.c a b)"
let t_ite = tree_of_string s_ite
let s_true = "(/x y.x)"
let t_true = tree_of_string s_true
let s_false = "(/x y.y)"
let t_false = tree_of_string s_false
let s_pair = "(/a b c.c a b)"
let t_pair = tree_of_string s_pair
let s_first = "(/p.p (/x y.x))"
let t_first = tree_of_string s_first
let s_second = "(/p.p (/x y.y))"
let t_second = tree_of_string s_second
let s_empty = "(/x a b.x)"
let t_empty = tree_of_string s_empty
let t_at = tree_of_string "(/x./x y.x)"
let t_af = tree_of_string "(/x./x y.y)"
let s_concat = "(/y z x a b.y (z x a b) a b)"
let t_concat = tree_of_string s_concat
let t_isempty = tree_of_string "(/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y))"
let t_prepa = tree_of_string "(/s x a b.a (s x a b))"
let t_prepb = tree_of_string "(/s x a b.b (s x a b))"
let t_nexta = tree_of_string "(/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))"
let t_nextb = tree_of_string "(/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))"
let t_tl = tree_of_string "(/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))))"
let t_hd = tree_of_string "(/s x a b.s x (/y.a x) (/y.b x))"
let t_hd_a = tree_of_string "(/s.s (/x y.y) (/x./x y.x) (/x./x y.y))"
let t_hd_b = tree_of_string "(/s.s (/x y.y) (/x./x y.x) (/x./x y.x))"
let t_is_e = tree_of_string "(/s.s (/x y.x) (/x./x y.y) (/x./x y.y))"
let t_and = tree_of_string "(/x y.x y x)"
let s_or = "(/x y.x x y)"
let t_or = tree_of_string s_or
let t_hd_eq = tree_of_string "(/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y)))"
let s_ycomb = "(/f.(/x.f (x x)) (/x.f (x x)))"
let t_ycomb = tree_of_string s_ycomb
let s_zcomb = "(/f.(/x.f (/y.x x y)) (/x.f (/y.x x y)))"
let t_zcomb = tree_of_string s_zcomb
let _eq_str = "(/rec x y.(/c a b.c a b) ((/x y.x x y) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))) x y) (rec ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x) ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) y))))";;
let s_eq_str = ("(/a b.(/f.(/x.f (x x)) (/x.f (x x))) " ^_eq_str ^ " a b)");;
let eq_str = tree_of_string s_eq_str;;
(* LISTS *)
let s_cons = "(/x y.(/a b c.c a b) (/x y.y) ((/a b c.c a b) x y))"
let t_cons = tree_of_string s_cons
let s_lhd = "(/z.(/p.p (/x y.x)) ((/p.p (/x y.y)) z))"
let t_lhd = tree_of_string s_lhd
let s_ltl = "(/z.(/p.p (/x y.y)) ((/p.p (/x y.y)) z))"
let t_ltl = tree_of_string s_ltl
let s_nil = "(/x.x)"
let t_nil = tree_of_string s_nil
let s_isnil = "(/p.p (/x y.x))"
let t_isnil = tree_of_string s_isnil
(* LIST with TUPLE (e,e) *)
let s_mktuple = "(/x y." ^ s_pair ^ " x y)"
let s_tuple_ee = "(" ^ s_mktuple ^ " " ^ s_empty ^ " " ^ s_empty ^ ")"
let s_listtuple_ee = "(" ^ s_cons ^ " " ^ s_tuple_ee ^ " " ^ s_nil ^ ")"
let t_listtuple_ee = tree_of_string s_listtuple_ee
(* LIST OF TILES *)
let s_t1_2 = "(/x a b.a x)"
let s_b1_2 = "(/x a b.a (b (b x)))"
let s_tile1 = "(" ^ s_mktuple ^ " " ^ s_t1_2 ^ " " ^ s_b1_2 ^ ")"
let s_t2_2 = "(/x a b.b x)"
let s_b2_2 = "(/x a b.x)"
let s_tile2 = "(" ^ s_mktuple ^ " " ^ s_t2_2 ^ " " ^ s_b2_2 ^ ")"
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ "))"
let t_tiles = tree_of_string s_tiles
(* find if for (t1,t2), t1 = t2 in list of tuples *)
(* "/r x.ite (isnil x) (false) (or (eq_str (fst (lhd x)) (snd (lhd x))) (r (tl x)))" *)
let s__find_eq = "(/r x."^s_ite^" ("^s_isnil^" x) "^s_false^" ("^s_or^" ("^s_eq_str^" ("^s_first^" ("^s_lhd^" x)) ("^s_second^" ("^s_lhd^" x))) (r ("^s_ltl^" x))))"
let s_find_eq = "(/x."^s_ycomb^" "^s__find_eq^" x)"
let t_find_eq = tree_of_string s_find_eq
(* let tmp = Core.AApp(t_find_eq, t_tiles, UnT) *)
let s_concat_pairs = "(/p s."^s_mktuple^" ("^s_concat^" ("^s_first^" p) ("^s_first^" s)) ("^s_concat^" ("^s_second^" p) ("^s_second^" s)))"
let s__combine = "(/r x ys."^s_ite^" ("^s_isnil^" ys) ("^s_nil^") ("^s_cons^" ("^s_concat_pairs^" x ("^s_lhd^" ys)) (r x ("^s_ltl^" ys))))"
let s_combine = "(/x y."^s_ycomb^" "^s__combine^" x y)"
let s__cross_append = "(/r xs ys."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_cons^" ("^s_combine^" ("^s_lhd^" xs) ys) (r ("^s_ltl^" xs) ys)))"
let s_cross_append = "(/xs ys."^s_ycomb^" "^s__cross_append^" xs ys)"
let t_cross_append = tree_of_string s_cross_append
(* let tmp = Core.AApp(Core.AApp(t_cross_append, t_listtuple_ee, UnT), t_tiles, UnT) *)
(* let tmp = t_tiles *)
let s__pcp = "(/r xs tiles."^s_ite^" ("^s_find_eq^" ("^s__cross_append^" xs tiles)) "^s_true^" (r ("^s__cross_append^" xs tiles) tiles))"
let s_pcp = "(/tiles."^s_ycomb^" "^s__pcp^" "^s_listtuple_ee^" tiles)"
let t_pcp = tree_of_string s_pcp
let tmp = Core.AApp(t_pcp, t_tiles, UnT)
(* STRINGS *)
let s_e = tree_of_string "(/x a b.x)"
let s_a = tree_of_string "(/x a b.a x)"
let s_b = tree_of_string "(/x a b.b x)"
let s_ab = tree_of_string "(/x a b.a (b x))"
let s_aa = tree_of_string "(/x a b.a (a x))"
let s_ba = tree_of_string "(/x a b.b (a x))"
let s_baba = tree_of_string "(/x a b.b (a (b (a x))))"
(* let _all_a = tree_of_string "(/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x))))"
let all_a = tree_of_string "(/a.(/f.(/x.f (x x)) (/x.f (x x))) (/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x)))) a)"
let tmp = Core.AApp(all_a, s_baba, UnT)
let res_all_a = Core.nf (Core.casubst) tmp
let tmp = Core.AApp(Core.AApp(eq_str, s_baba, UnT), s_baba, UnT)
let res = Core.nf (Core.casubst) tmp
let res_eq_str = Core.nf (Core.casubst) tmp *)
(* PCP2 *)
(* let s_t1_2 = "(/x a b.a x)"
let s_b1_2 = "(/x a b.a (b (b x)))"
let s_t2_2 = "(/x a b.b x)"
let s_b2_2 = "(/x a b.x)" *)
(* let s_t1_2 = "(/x a b.a x)"
let s_b1_2 = "(/x a b.a (b x))"
let s_t2_2 = "(/x a b.b x)"
let s_b2_2 = "(/x a b.x)"
let _pcp2 = "(/f a b." ^ s_ite ^ " (" ^ s_or ^ " (" ^ s_eq_str ^ " (" ^ s_concat ^ " a " ^ s_t1_2 ^ ") (" ^ s_concat ^ " b " ^ s_b1_2 ^ ")) (" ^ s_eq_str ^ " (" ^ s_concat ^ " a " ^ s_t2_2 ^ ") (" ^ s_concat ^ " b " ^ s_b2_2 ^ "))) " ^ s_true ^ " (" ^ s_or ^ " (f (" ^ s_concat ^ " a " ^ s_t1_2 ^ ") (" ^ s_concat ^ " b " ^ s_b1_2 ^ ")) (f (" ^ s_concat ^ " a " ^ s_t2_2 ^ ") (" ^ s_concat ^ " b " ^ s_b2_2 ^ "))))"
let s_pcp2 = s_ycomb ^ " " ^ _pcp2 ^ " " ^ s_empty ^ " " ^ s_empty
let pcp2 = tree_of_string s_pcp2
let res_pcp2 = Core.nf (Core.casubst) pcp2 *)
(* PCP3 *)
(* let s_t1 = "(/x a b.b x)"
let s_b1 = "(/x a b.b (b (b x)))"
let s_t2 = "(/x a b.b (a (b (b (b x)))))"
let s_b2 = "(/x a b.b (a x))"
let s_t3 = "(/x a b.b (a x))"
let s_b3 = "(/x a b.a x)"
let _pcp3 = "/f a b." ^ s_ite ^ " (" ^ s_or ^ " (" ^ s_or ^ " (" ^ s_eq_str ^ " (" ^ s_concat ^ " a " ^ s_t1 ^ ") (" ^ s_concat ^ " b " ^ s_b1 ^ ")) (" ^ s_eq_str ^ " (" ^ s_concat ^ " a " ^ s_t2 ^ ") (" ^ s_concat ^ " b " ^ s_b2 ^ ")))) (" ^ s_eq_str ^ " (" ^ s_concat ^ " a " ^ s_t3 ^ ") (" ^ s_concat ^ " b " ^ s_b3 ^ ")) " ^ s_true ^ " (" ^ s_or ^ " (" ^ s_or ^ " (f (" ^ s_concat ^ " a " ^ s_t1 ^ ") (" ^ s_concat ^ " b " ^ s_b1 ^ ")) (f (" ^ s_concat ^ " a " ^ s_t2 ^ ") (" ^ s_concat ^ " b " ^ s_b2 ^ "))) (f (" ^ s_concat ^ " a " ^ s_t3 ^ ") (" ^ s_concat ^ " b " ^ s_b3 ^ ")))"
(* let tmp = Core.AApp(Core.AApp(t_and, t_true, UnT), t_true, UnT)
let res = Core.nf (Core.casubst) tmp *)
let s_pcp3 = s_ycomb ^ " " ^ _pcp3 ^ " " ^ s_empty ^ " " ^ s_empty
let pcp3 = tree_of_string s_pcp3
(* let tmp = Core.AApp(t_tl, s_baba, UnT)
let res = Core.nf (Core.casubst) tmp *)
let res_pcp3 = Core.nf (Core.casubst) pcp3 *)
let () = Printf.printf "res: %s" (Core.a_term_to_string res)
let () =
Printf.printf "PCP file.\n";
(* Printf.printf "%s\n\n" s_pcp; *)
Printf.printf "res_tmp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst tmp));
(* Printf.printf "res_all_a: %s\n" (Core.a_term_to_string res_all_a);
Printf.printf "res_eq_str: %s\n" (Core.a_term_to_string res_eq_str);
(* Printf.printf "pcp2: %s\n" (s_pcp2); *)
Printf.printf "res_pcp2: %s\n" (Core.a_term_to_string res_pcp2); *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment