(set-logic UFDT)
(set-info :source |
Generated by: Andrew Reynolds
Generated on: 2017-04-28
Generator: Sledgehammer, converted to v2.6 by CVC4
Application: Verfication goals in Isabelle
Target solver: CVC4, Z3
Publications: "A Decision Procedure for (Co)Datatypes" by Andrew Reynolds and Jasmin Blanchette, CADE 2015.
|)
(set-info :status unsat)
(declare-sort A$ 0)
(declare-sort B$ 0)
(declare-sort A_a_fun$ 0)
(declare-sort A_b_fun$ 0)
(declare-sort B_a_fun$ 0)
(declare-sort B_b_fun$ 0)
(declare-sort A_bool_fun$ 0)
(declare-sort B_bool_fun$ 0)
(declare-sort A_a_tree_fun$ 0)
(declare-sort A_b_tree_fun$ 0)
(declare-sort A_tree_b_fun$ 0)
(declare-sort B_a_tree_fun$ 0)
(declare-sort B_b_tree_fun$ 0)
(declare-sort B_tree_b_fun$ 0)
(declare-sort A_a_sum_a_fun$ 0)
(declare-sort A_a_sum_b_fun$ 0)
(declare-sort A_b_fun_b_fun$ 0)
(declare-sort B_b_fun_b_fun$ 0)
(declare-sort B_b_sum_b_fun$ 0)
(declare-sort A_a_a_prod_fun$ 0)
(declare-sort A_b_b_prod_fun$ 0)
(declare-sort B_b_b_prod_fun$ 0)
(declare-sort B_b_prod_b_fun$ 0)
(declare-sort B_tree_bool_fun$ 0)
(declare-sort A_b_fun_bool_fun$ 0)
(declare-sort B_b_bool_fun_fun$ 0)
(declare-sort A_tree_a_tree_fun$ 0)
(declare-sort A_tree_b_tree_fun$ 0)
(declare-sort B_tree_a_tree_fun$ 0)
(declare-sort B_tree_b_tree_fun$ 0)
(declare-sort A_b_fun_b_tree_fun$ 0)
(declare-sort B_b_tree_sum_b_fun$ 0)
(declare-sort A_a_fun_a_a_fun_fun$ 0)
(declare-sort A_a_fun_a_b_fun_fun$ 0)
(declare-sort A_a_sum_a_a_sum_fun$ 0)
(declare-sort A_a_sum_b_b_sum_fun$ 0)
(declare-sort A_b_fun_a_a_fun_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun$ 0)
(declare-sort A_b_sum_b_b_sum_fun$ 0)
(declare-sort B_a_fun_b_a_fun_fun$ 0)
(declare-sort B_a_fun_b_b_fun_fun$ 0)
(declare-sort B_b_b_tree_prod_fun$ 0)
(declare-sort B_b_fun_b_a_fun_fun$ 0)
(declare-sort B_b_fun_b_b_fun_fun$ 0)
(declare-sort B_b_sum_b_b_sum_fun$ 0)
(declare-sort A_a_prod_a_a_prod_fun$ 0)
(declare-sort A_a_prod_b_b_prod_fun$ 0)
(declare-sort B_a_b_b_prod_prod_fun$ 0)
(declare-sort B_b_b_b_prod_prod_fun$ 0)
(declare-sort B_b_prod_b_b_prod_fun$ 0)
(declare-sort A_a_sum_tree_a_tree_fun$ 0)
(declare-sort A_a_sum_tree_b_tree_fun$ 0)
(declare-sort B_tree_b_sum_b_tree_fun$ 0)
(declare-sort A_a_fun_a_a_tree_fun_fun$ 0)
(declare-sort A_tree_b_b_prod_tree_fun$ 0)
(declare-sort B_b_fun_b_b_tree_fun_fun$ 0)
(declare-sort B_b_sum_b_tree_b_sum_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_fun$ 0)
(declare-sort B_tree_b_sum_b_b_sum_fun$ 0)
(declare-sort B_tree_b_tree_b_prod_fun$ 0)
(declare-sort A_a_fun_a_a_sum_a_fun_fun$ 0)
(declare-sort A_a_fun_a_b_b_prod_fun_fun$ 0)
(declare-sort A_b_fun_a_b_b_prod_fun_fun$ 0)
(declare-sort B_b_b_prod_fun_b_b_fun_fun$ 0)
(declare-sort B_b_prod_b_tree_b_prod_fun$ 0)
(declare-sort B_tree_b_prod_b_b_prod_fun$ 0)
(declare-sort B_tree_b_tree_bool_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_bool_fun$ 0)
(declare-sort B_tree_tree_b_tree_tree_fun$ 0)
(declare-sort B_b_fun_b_b_bool_fun_fun_fun$ 0)
(declare-sort B_tree_b_tree_fun_b_tree_fun$ 0)
(declare-sort B_tree_b_tree_sum_b_tree_fun$ 0)
(declare-sort A_b_fun_tree_a_b_fun_tree_fun$ 0)
(declare-sort A_b_tree_sum_b_b_tree_sum_fun$ 0)
(declare-sort A_tree_b_sum_a_tree_b_sum_fun$ 0)
(declare-sort A_tree_b_sum_b_tree_b_sum_fun$ 0)
(declare-sort B_a_tree_fun_b_b_tree_fun_fun$ 0)
(declare-sort B_b_fun_tree_b_b_fun_tree_fun$ 0)
(declare-sort B_b_sum_tree_b_b_sum_tree_fun$ 0)
(declare-sort B_b_tree_fun_b_b_tree_fun_fun$ 0)
(declare-sort B_b_tree_sum_b_b_tree_sum_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_fun$ 0)
(declare-sort B_tree_b_fun_b_tree_b_fun_fun$ 0)
(declare-sort B_tree_b_sum_b_tree_b_sum_fun$ 0)
(declare-sort B_tree_b_tree_a_b_fun_sum_fun$ 0)
(declare-sort B_tree_b_tree_b_tree_prod_fun$ 0)
(declare-sort B_tree_b_tree_prod_b_tree_fun$ 0)
(declare-sort A_b_fun_b_tree_a_b_fun_sum_fun$ 0)
(declare-sort B_b_tree_b_tree_prod_prod_b_fun$ 0)
(declare-sort B_b_tree_prod_b_b_tree_prod_fun$ 0)
(declare-sort B_tree_b_prod_b_tree_b_prod_fun$ 0)
(declare-sort A_a_a_prod_fun_a_b_b_prod_fun_fun$ 0)
(declare-sort B_b_b_fun_b_b_bool_fun_fun_fun_fun$ 0)
(declare-sort B_b_tree_sum_b_tree_b_tree_sum_fun$ 0)
(declare-sort B_tree_b_tree_fun_b_tree_b_fun_fun$ 0)
(declare-sort B_tree_b_tree_sum_b_b_tree_sum_fun$ 0)
(declare-sort A_a_a_prod_prod_a_a_a_prod_prod_fun$ 0)
(declare-sort A_a_a_prod_prod_b_b_b_prod_prod_fun$ 0)
(declare-sort A_b_b_prod_prod_a_b_b_prod_prod_fun$ 0)
(declare-sort A_b_b_prod_prod_b_b_b_prod_prod_fun$ 0)
(declare-sort B_b_b_prod_prod_b_b_b_prod_prod_fun$ 0)
(declare-sort A_a_fun_a_a_fun_a_a_tree_fun_fun_fun$ 0)
(declare-sort A_tree_a_a_tree_a_tree_prod_prod_fun$ 0)
(declare-sort A_tree_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort B_b_tree_prod_b_tree_b_tree_prod_fun$ 0)
(declare-sort B_tree_a_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort B_tree_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort B_tree_b_tree_prod_b_b_tree_prod_fun$ 0)
(declare-sort A_b_fun_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort A_tree_a_tree_fun_a_tree_a_tree_fun_fun$ 0)
(declare-sort A_tree_a_tree_fun_a_tree_b_tree_fun_fun$ 0)
(declare-sort A_tree_b_tree_fun_a_tree_a_tree_fun_fun$ 0)
(declare-sort A_tree_b_tree_fun_a_tree_b_tree_fun_fun$ 0)
(declare-sort A_tree_b_tree_sum_a_tree_b_tree_sum_fun$ 0)
(declare-sort A_tree_b_tree_sum_b_tree_b_tree_sum_fun$ 0)
(declare-sort B_tree_a_tree_fun_b_tree_b_tree_fun_fun$ 0)
(declare-sort B_tree_b_tree_fun_b_tree_b_tree_fun_fun$ 0)
(declare-sort B_tree_b_tree_sum_b_tree_b_tree_sum_fun$ 0)
(declare-sort A_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun$ 0)
(declare-sort A_b_fun_b_tree_fun_a_b_fun_b_tree_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_b_tree_prod_fun$ 0)
(declare-sort B_tree_b_tree_prod_b_tree_b_tree_prod_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun$ 0)
(declare-sort B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$ 0)
(declare-sort B_b_b_tree_b_sum_b_tree_b_sum_prod_prod_fun$ 0)
(declare-sort B_tree_b_b_prod_prod_b_tree_b_b_prod_prod_fun$ 0)
(declare-sort B_b_fun_b_b_b_fun_b_b_bool_fun_fun_fun_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$ 0)
(declare-sort B_a_b_b_prod_prod_fun_b_a_b_b_prod_prod_fun_fun$ 0)
(declare-sort A_b_fun_bool_fun_b_tree_a_b_fun_sum_bool_fun_fun$ 0)
(declare-sort B_b_tree_b_tree_prod_prod_b_tree_b_tree_prod_fun$ 0)
(declare-sort B_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun$ 0)
(declare-sort B_tree_b_tree_fun_tree_b_tree_b_tree_fun_tree_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_bool_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun$ 0)
(declare-sort B_tree_b_tree_a_b_fun_sum_fun_b_tree_b_tree_fun_fun$ 0)
(declare-sort B_tree_b_tree_b_tree_prod_fun_b_tree_b_tree_fun_fun$ 0)
(declare-sort A_b_fun_b_tree_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$ 0)
(declare-sort A_b_fun_b_tree_a_b_fun_sum_fun_a_b_fun_b_tree_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_fun$ 0)
(declare-sort A_a_tree_a_tree_prod_prod_a_a_tree_a_tree_prod_prod_fun$ 0)
(declare-sort A_a_tree_a_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort A_b_tree_b_tree_prod_prod_a_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort A_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort B_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$ 0)
(declare-sort B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort A_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_bool_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_bool_fun$ 0)
(declare-sort B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$ 0)
(declare-sort B_tree_b_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod_fun$ 0)
(declare-sort B_tree_b_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun_fun$ 0)
(declare-sort A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$ 0)
(declare-sort B_tree_b_tree_fun_b_tree_b_tree_prod_b_tree_b_tree_prod_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_b_tree_prod_fun_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_fun$ 0)
(declare-sort A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$ 0)
(declare-sort B_tree_b_tree_b_tree_prod_prod_b_tree_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun$ 0)
(declare-sort A_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_b_tree_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$ 0)
(declare-sort B_tree_a_b_tree_b_tree_prod_prod_fun_b_tree_a_b_tree_b_tree_prod_prod_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun_fun$ 0)
(declare-sort A_a_tree_b_sum_a_tree_b_sum_prod_prod_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$ 0)
(declare-sort A_a_tree_b_sum_a_tree_b_sum_prod_prod_b_b_tree_b_sum_b_tree_b_sum_prod_prod_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$ 0)
(declare-sort B_tree_b_tree_fun_b_tree_b_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun_fun_fun$ 0)
(declare-sort A_a_tree_fun_a_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$ 0)
(declare-sort A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ 0)
(declare-sort B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun_b_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ 0)
(declare-sort A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$ 0)
(declare-sort A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_b_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$ 0)
(declare-sort A_bool_fun_a_a_tree_fun_a_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$ 0)
(declare-sort B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ 0)
(declare-sort A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_fun$ 0)
(declare-sort B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun_b_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun_fun$ 0)
(declare-sort A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun$ 0)
(declare-sort A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$ 0)
(declare-sort A_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun$ 0)
(declare-sort A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun_fun$ 0)
(declare-sort B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$ 0)
(declare-sort A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun_fun$ 0)
(declare-sort A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun_fun_fun$ 0)
(declare-sort B_tree$ 0)
(declare-fun root$ (B_tree$) B$)
(declare-fun left$ (B_tree$) B_tree$)
(declare-fun right$ (B_tree$) B_tree$)
(declare-fun node$ (B$ B_tree$ B_tree$) B_tree$)
(declare-datatypes ((B_tree_b_tree_prod$ 0)(B_b_tree_b_tree_prod_prod$ 0)(B_tree_a_b_fun_sum$ 0)(B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$ 0)(B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$ 0)) (((pair$ (fst$ B_tree$) (snd$ B_tree$)))
((pair$a (fst$a B$) (snd$a B_tree_b_tree_prod$)))
((inl$ (select$ B_tree$)) (inr$ (selecta$ A_b_fun$)))
((pair$b (fst$b B_tree_a_b_fun_sum$) (snd$b B_tree_a_b_fun_sum$)))
((pair$c (fst$c B$) (snd$c B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)))
))
(declare-sort A_tree$ 0)
(declare-fun root$a (A_tree$) A$)
(declare-fun left$a (A_tree$) A_tree$)
(declare-fun right$a (A_tree$) A_tree$)
(declare-fun node$a (A$ A_tree$ A_tree$) A_tree$)
(declare-datatypes ((A_tree_a_tree_prod$ 0)(A_a_tree_a_tree_prod_prod$ 0)(B_b_prod$ 0)) (((pair$d (fst$d A_tree$) (snd$d A_tree$)))
((pair$e (fst$e A$) (snd$e A_tree_a_tree_prod$)))
((pair$f (fst$f B$) (snd$f B$)))
))
(declare-sort B_b_prod_tree$ 0)
(declare-fun root$b (B_b_prod_tree$) B_b_prod$)
(declare-fun left$b (B_b_prod_tree$) B_b_prod_tree$)
(declare-fun right$b (B_b_prod_tree$) B_b_prod_tree$)
(declare-fun node$b (B_b_prod$ B_b_prod_tree$ B_b_prod_tree$) B_b_prod_tree$)
(declare-datatypes ((A_a_sum$ 0)) (((inl$a (projl$ A$)) (inr$a (projr$ A$)))
))
(declare-sort A_a_sum_tree$ 0)
(declare-sort B_tree_tree$ 0)
(declare-fun root$c (A_a_sum_tree$) A_a_sum$)
(declare-fun left$c (A_a_sum_tree$) A_a_sum_tree$)
(declare-fun right$c (A_a_sum_tree$) A_a_sum_tree$)
(declare-fun node$c (A_a_sum$ A_a_sum_tree$ A_a_sum_tree$) A_a_sum_tree$)
(declare-fun root$d (B_tree_tree$) B_tree$)
(declare-fun left$d (B_tree_tree$) B_tree_tree$)
(declare-fun right$d (B_tree_tree$) B_tree_tree$)
(declare-fun node$d (B_tree$ B_tree_tree$ B_tree_tree$) B_tree_tree$)
(declare-datatypes ((B_b_sum$ 0)) (((inl$b (projl$a B$)) (inr$b (projr$a B$)))
))
(declare-sort B_b_sum_tree$ 0)
(declare-sort B_tree_b_tree_fun_tree$ 0)
(declare-sort B_b_fun_tree$ 0)
(declare-sort A_b_fun_tree$ 0)
(declare-fun root$e (B_b_sum_tree$) B_b_sum$)
(declare-fun left$e (B_b_sum_tree$) B_b_sum_tree$)
(declare-fun right$e (B_b_sum_tree$) B_b_sum_tree$)
(declare-fun node$e (B_b_sum$ B_b_sum_tree$ B_b_sum_tree$) B_b_sum_tree$)
(declare-fun selectb$ (B_tree_b_tree_fun_tree$) B_tree_b_tree_fun$)
(declare-fun selectc$ (B_tree_b_tree_fun_tree$) B_tree_b_tree_fun_tree$)
(declare-fun selectd$ (B_tree_b_tree_fun_tree$) B_tree_b_tree_fun_tree$)
(declare-fun node$f (B_tree_b_tree_fun$ B_tree_b_tree_fun_tree$ B_tree_b_tree_fun_tree$) B_tree_b_tree_fun_tree$)
(declare-fun selecte$ (B_b_fun_tree$) B_b_fun$)
(declare-fun selectf$ (B_b_fun_tree$) B_b_fun_tree$)
(declare-fun selectg$ (B_b_fun_tree$) B_b_fun_tree$)
(declare-fun node$g (B_b_fun$ B_b_fun_tree$ B_b_fun_tree$) B_b_fun_tree$)
(declare-fun selecth$ (A_b_fun_tree$) A_b_fun$)
(declare-fun selecti$ (A_b_fun_tree$) A_b_fun_tree$)
(declare-fun selectj$ (A_b_fun_tree$) A_b_fun_tree$)
(declare-fun node$h (A_b_fun$ A_b_fun_tree$ A_b_fun_tree$) A_b_fun_tree$)
(declare-datatypes ((A_a_prod$ 0)(A_b_tree_sum$ 0)(A_b_sum$ 0)(B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod$ 0)(B_b_tree_prod$ 0)(B_tree_b_prod$ 0)(B_b_b_prod_prod$ 0)(A_a_a_prod_prod$ 0)(B_tree_b_b_prod_prod$ 0)(B_tree_b_tree_b_tree_prod_prod$ 0)(A_b_b_prod_prod$ 0)(A_b_tree_b_tree_prod_prod$ 0)(A_tree_b_sum$ 0)(A_tree_b_sum_a_tree_b_sum_prod$ 0)(A_a_tree_b_sum_a_tree_b_sum_prod_prod$ 0)(B_tree_b_sum$ 0)(B_tree_b_sum_b_tree_b_sum_prod$ 0)(B_b_tree_b_sum_b_tree_b_sum_prod_prod$ 0)(A_tree_b_tree_sum$ 0)(A_tree_b_tree_sum_a_tree_b_tree_sum_prod$ 0)(A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod$ 0)(B_tree_b_tree_sum$ 0)(B_tree_b_tree_sum_b_tree_b_tree_sum_prod$ 0)(B_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod$ 0)(B_b_tree_sum$ 0)) (((pair$g (fst$g A$) (snd$g A$)))
((inl$c (projl$b A$)) (inr$c (projr$b B_tree$)))
((inl$d (projl$c A$)) (inr$d (projr$c B$)))
((pair$h (fst$h B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (snd$h B$)))
((pair$i (fst$i B$) (snd$i B_tree$)))
((pair$j (fst$j B_tree$) (snd$j B$)))
((pair$k (fst$k B$) (snd$k B_b_prod$)))
((pair$l (fst$l A$) (snd$l A_a_prod$)))
((pair$m (fst$m B_tree$) (snd$m B_b_prod$)))
((pair$n (fst$n B_tree$) (snd$n B_tree_b_tree_prod$)))
((pair$o (fst$o A$) (snd$o B_b_prod$)))
((pair$p (fst$p A$) (snd$p B_tree_b_tree_prod$)))
((inl$e (projl$d A_tree$)) (inr$e (projr$d B$)))
((pair$q (fst$q A_tree_b_sum$) (snd$q A_tree_b_sum$)))
((pair$r (fst$r A$) (snd$r A_tree_b_sum_a_tree_b_sum_prod$)))
((inl$f (projl$e B_tree$)) (inr$f (projr$e B$)))
((pair$s (fst$s B_tree_b_sum$) (snd$s B_tree_b_sum$)))
((pair$t (fst$t B$) (snd$t B_tree_b_sum_b_tree_b_sum_prod$)))
((inl$g (projl$f A_tree$)) (inr$g (projr$f B_tree$)))
((pair$u (fst$u A_tree_b_tree_sum$) (snd$u A_tree_b_tree_sum$)))
((pair$v (fst$v A$) (snd$v A_tree_b_tree_sum_a_tree_b_tree_sum_prod$)))
((inl$h (projl$g B_tree$)) (inr$h (projr$g B_tree$)))
((pair$w (fst$w B_tree_b_tree_sum$) (snd$w B_tree_b_tree_sum$)))
((pair$x (fst$x B$) (snd$x B_tree_b_tree_sum_b_tree_b_tree_sum_prod$)))
((inl$i (projl$h B$)) (inr$i (projr$h B_tree$)))
))
(declare-fun l$ () A_a_fun$)
(declare-fun r$ () A_a_fun$)
(declare-fun t$ () A_tree$)
(declare-fun x$ () A$)
(declare-fun id$ () B_b_fun$)
(declare-fun uu$ () A_b_fun_b_tree_fun$)
(declare-fun id$a () B_tree_b_tree_fun$)
(declare-fun id$b () B_b_sum_b_b_sum_fun$)
(declare-fun id$c () B_tree_b_tree_fun_b_tree_b_tree_fun_fun$)
(declare-fun id$d () B_b_fun_b_b_fun_fun$)
(declare-fun id$e () A_b_fun_a_b_fun_fun$)
(declare-fun id$f () A_a_fun$)
(declare-fun id$g () B_b_sum_tree_b_b_sum_tree_fun$)
(declare-fun id$h () B_tree_b_tree_fun_tree_b_tree_b_tree_fun_tree_fun$)
(declare-fun id$i () B_b_fun_tree_b_b_fun_tree_fun$)
(declare-fun id$j () A_b_fun_tree_a_b_fun_tree_fun$)
(declare-fun id$k () B_tree_tree_b_tree_tree_fun$)
(declare-fun id$l () A_tree_a_tree_fun$)
(declare-fun id$m () B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun id$n () B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun id$o () B_b_prod_b_b_prod_fun$)
(declare-fun id$p () A_a_prod_a_a_prod_fun$)
(declare-fun id$q () B_b_tree_prod_b_b_tree_prod_fun$)
(declare-fun id$r () B_tree_b_prod_b_tree_b_prod_fun$)
(declare-fun id$s () B_tree_b_tree_prod_b_tree_b_tree_prod_fun$)
(declare-fun id$t () B_b_b_prod_prod_b_b_b_prod_prod_fun$)
(declare-fun id$u () B_tree_b_b_prod_prod_b_tree_b_b_prod_prod_fun$)
(declare-fun id$v () B_tree_b_tree_b_tree_prod_prod_b_tree_b_tree_b_tree_prod_prod_fun$)
(declare-fun id$w () B_b_tree_sum_b_b_tree_sum_fun$)
(declare-fun id$x () B_tree_b_sum_b_tree_b_sum_fun$)
(declare-fun id$y () B_tree_b_tree_sum_b_tree_b_tree_sum_fun$)
(declare-fun id$z (B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum$)
(declare-fun uua$ () B_b_fun$)
(declare-fun uub$ () B_tree_b_tree_fun$)
(declare-fun uuc$ () A_a_fun$)
(declare-fun uud$ (B$) B_b_fun$)
(declare-fun uue$ (B$) A_b_fun$)
(declare-fun uuf$ (B$) B_tree_b_fun$)
(declare-fun uug$ (A$) A_a_fun$)
(declare-fun uuh$ (B_tree$) B_tree_b_tree_fun$)
(declare-fun uui$ (B_tree$) A_b_fun_b_tree_fun$)
(declare-fun uuj$ () B_tree_b_tree_prod_b_tree_b_tree_prod_fun$)
(declare-fun uuk$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun uul$ (B_tree_b_tree_fun$) B_tree_b_tree_fun_b_tree_b_tree_fun_fun$)
(declare-fun uum$ (B_tree_b_tree_fun$) A_b_fun_b_tree_fun_a_b_fun_b_tree_fun_fun$)
(declare-fun uun$ () A_b_fun_b_tree_a_b_fun_sum_fun$)
(declare-fun uuo$ (A$) A_b_fun_b_fun$)
(declare-fun uup$ (A_a_fun$) A_b_fun_a_b_fun_fun$)
(declare-fun uuq$ (A_b_fun_b_fun$) A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun_fun_fun$)
(declare-fun uur$ () B_tree_b_tree_a_b_fun_sum_fun$)
(declare-fun uus$ (B_tree_a_b_fun_sum_b_tree_fun$) B_tree_b_tree_fun$)
(declare-fun uut$ (B_tree_a_b_fun_sum_b_tree_fun$) A_b_fun_b_tree_fun$)
(declare-fun uuu$ (B$) B_b_fun_b_fun$)
(declare-fun uuv$ (B_b_fun$) B_b_fun_b_b_fun_fun$)
(declare-fun uuw$ (B_tree$) B_tree_b_tree_fun_b_tree_fun$)
(declare-fun uux$ (B_tree_b_tree_fun$) B_tree_b_tree_fun_b_tree_b_tree_fun_fun$)
(declare-fun uuy$ (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun_fun$)
(declare-fun uuz$ (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_bool_fun_fun$)
(declare-fun uva$ () B_b_tree_b_tree_prod_prod_b_fun$)
(declare-fun uvb$ () B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$)
(declare-fun uvc$ () B_tree_b_tree_prod_b_tree_fun$)
(declare-fun uvd$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$)
(declare-fun uve$ () B_b_tree_b_tree_prod_prod_b_tree_b_tree_prod_fun$)
(declare-fun uvf$ () B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun uvg$ () B_tree_b_tree_prod_b_tree_fun$)
(declare-fun uvh$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$)
(declare-fun uvi$ () B_b_prod_b_fun$)
(declare-fun uvj$ () B_b_b_prod_fun$)
(declare-fun uvk$ () B_tree_b_tree_b_tree_prod_fun$)
(declare-fun uvl$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun uvm$ () B_b_prod_b_fun$)
(declare-fun uvn$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$)
(declare-fun uvo$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$)
(declare-fun uvp$ () B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$)
(declare-fun uvq$ () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$)
(declare-fun uvr$ (B_b_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun_fun$)
(declare-fun uvs$ (B_tree_a_b_fun_sum_b_tree_fun$ B_tree_a_b_fun_sum_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_b_tree_prod_fun_fun$)
(declare-fun comp$ (B_tree_b_tree_fun$) B_tree_b_tree_fun_b_tree_b_tree_fun_fun$)
(declare-fun id$aa () B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun swap$ (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun xtor$ (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun apfst$ (B_b_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun apsnd$ (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun comp$a (B_b_fun$) B_b_fun_b_b_fun_fun$)
(declare-fun comp$b (A_b_fun$) A_a_fun_a_b_fun_fun$)
(declare-fun comp$c (B_b_fun$) A_b_fun_a_b_fun_fun$)
(declare-fun comp$d (B_a_fun$) A_b_fun_a_a_fun_fun$)
(declare-fun comp$e (A_a_fun$) A_a_fun_a_a_fun_fun$)
(declare-fun comp$f (A_b_fun$) B_a_fun_b_b_fun_fun$)
(declare-fun comp$g (A_a_fun$) B_a_fun_b_a_fun_fun$)
(declare-fun comp$h (B_a_fun$) B_b_fun_b_a_fun_fun$)
(declare-fun comp$i (A_b_b_prod_fun$) A_a_fun_a_b_b_prod_fun_fun$)
(declare-fun comp$j (A_b_fun$ A_a_sum_a_fun$) A_a_sum_b_fun$)
(declare-fun comp$k (B_tree_b_tree_fun$) A_tree_b_tree_fun_a_tree_b_tree_fun_fun$)
(declare-fun comp$l (A_tree_b_tree_fun$) A_tree_a_tree_fun_a_tree_b_tree_fun_fun$)
(declare-fun comp$m (B_tree_a_tree_fun$) A_tree_b_tree_fun_a_tree_a_tree_fun_fun$)
(declare-fun comp$n (A_tree_a_tree_fun$) A_tree_a_tree_fun_a_tree_a_tree_fun_fun$)
(declare-fun comp$o (A_tree_a_tree_fun$ B_tree_a_tree_fun$) B_tree_a_tree_fun$)
(declare-fun comp$p (B_tree_a_tree_fun$ B_tree_b_tree_fun$) B_tree_a_tree_fun$)
(declare-fun comp$q (A_tree_b_tree_fun$) B_tree_a_tree_fun_b_tree_b_tree_fun_fun$)
(declare-fun comp$r (A_tree_b_b_prod_tree_fun$ A_tree_a_tree_fun$) A_tree_b_b_prod_tree_fun$)
(declare-fun comp$s (A_tree_b_tree_fun$ A_a_sum_tree_a_tree_fun$) A_a_sum_tree_b_tree_fun$)
(declare-fun comp$t (A_a_prod_b_b_prod_fun$ A_a_prod_a_a_prod_fun$) A_a_prod_b_b_prod_fun$)
(declare-fun comp$u (B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$v (B_tree_b_tree_prod_b_tree_b_tree_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$)
(declare-fun comp$w (B_tree_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$)
(declare-fun comp$x (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$y (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$)
(declare-fun comp$z (B_tree_a_b_fun_sum_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$)
(declare-fun swap$a (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod$)
(declare-fun swap$b (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun xtor$a (B_b_tree_b_tree_prod_prod$) B_b_tree_b_tree_prod_prod$)
(declare-fun xtor$b (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun xtor$c (B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum$)
(declare-fun apfst$a (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun apsnd$a (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun apsnd$b (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$aa (B_tree_a_b_fun_sum_b_tree_fun$) A_b_fun_b_tree_a_b_fun_sum_fun_a_b_fun_b_tree_fun_fun$)
(declare-fun comp$ab (B_tree_b_tree_fun$) A_b_fun_b_tree_fun_a_b_fun_b_tree_fun_fun$)
(declare-fun comp$ac (A_tree_b_tree_fun$ A_a_tree_fun$) A_b_tree_fun$)
(declare-fun comp$ad (B_tree_a_b_fun_sum_b_tree_fun$) B_tree_b_tree_a_b_fun_sum_fun_b_tree_b_tree_fun_fun$)
(declare-fun comp$ae (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$ A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$) A_b_fun_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$af (B_tree_b_b_tree_b_tree_prod_prod_fun$ A_b_fun_b_tree_fun$) A_b_fun_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$ag (A_a_a_prod_prod_b_b_b_prod_prod_fun$ A_a_a_prod_prod_a_a_a_prod_prod_fun$) A_a_a_prod_prod_b_b_b_prod_prod_fun$)
(declare-fun comp$ah (A_tree_b_tree_fun$) B_a_tree_fun_b_b_tree_fun_fun$)
(declare-fun comp$ai (A_b_b_prod_prod_b_b_b_prod_prod_fun$ B_a_b_b_prod_prod_fun$) B_b_b_b_prod_prod_fun$)
(declare-fun comp$aj (A_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ B_tree_a_b_tree_b_tree_prod_prod_fun$) B_tree_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$ak (A_tree_a_tree_fun$ B_a_tree_fun$) B_a_tree_fun$)
(declare-fun comp$al (A_b_b_prod_prod_a_b_b_prod_prod_fun$) B_a_b_b_prod_prod_fun_b_a_b_b_prod_prod_fun_fun$)
(declare-fun comp$am (A_b_tree_b_tree_prod_prod_a_b_tree_b_tree_prod_prod_fun$) B_tree_a_b_tree_b_tree_prod_prod_fun_b_tree_a_b_tree_b_tree_prod_prod_fun_fun$)
(declare-fun comp$an (B_b_prod_b_b_prod_fun$ B_b_b_prod_fun$ B$) B_b_prod$)
(declare-fun comp$ao (B_b_prod_b_tree_b_prod_fun$ B_b_b_prod_fun$ B$) B_tree_b_prod$)
(declare-fun comp$ap (B_tree_b_tree_fun$) B_b_tree_fun_b_b_tree_fun_fun$)
(declare-fun comp$aq (B_tree_b_prod_b_b_prod_fun$ B_tree_b_tree_b_prod_fun$ B_tree$) B_b_prod$)
(declare-fun comp$ar (B_b_fun$) B_tree_b_fun_b_tree_b_fun_fun$)
(declare-fun comp$as (B_tree_b_prod_b_tree_b_prod_fun$ B_tree_b_tree_b_prod_fun$ B_tree$) B_tree_b_prod$)
(declare-fun comp$at (B_b_tree_prod_b_b_tree_prod_fun$ B_b_b_tree_prod_fun$ B$) B_b_tree_prod$)
(declare-fun comp$au (B_b_tree_prod_b_tree_b_tree_prod_fun$ B_b_b_tree_prod_fun$ B$) B_tree_b_tree_prod$)
(declare-fun comp$av (B_tree_b_tree_prod_b_b_tree_prod_fun$ B_tree_b_tree_b_tree_prod_fun$ B_tree$) B_b_tree_prod$)
(declare-fun comp$aw (B_tree_b_tree_prod_b_tree_b_tree_prod_fun$ B_tree_b_tree_b_tree_prod_fun$ B_tree$) B_tree_b_tree_prod$)
(declare-fun comp$ax (A_tree_a_a_tree_a_tree_prod_prod_fun$ A_tree_a_tree_fun$) A_tree_a_a_tree_a_tree_prod_prod_fun$)
(declare-fun comp$ay (A_a_tree_a_tree_prod_prod_a_a_tree_a_tree_prod_prod_fun$ A_tree_a_a_tree_a_tree_prod_prod_fun$) A_tree_a_a_tree_a_tree_prod_prod_fun$)
(declare-fun comp$az (B_tree_b_b_tree_b_tree_prod_prod_fun$ A_tree_b_tree_fun$) A_tree_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$ba (A_a_tree_a_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ A_tree_a_a_tree_a_tree_prod_prod_fun$) A_tree_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$bb (B_tree_b_b_tree_b_tree_prod_prod_fun$ B_tree_b_tree_fun$) B_tree_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$bc (B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ B_tree_b_b_tree_b_tree_prod_prod_fun$) B_tree_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun comp$bd (A_a_prod_b_b_prod_fun$) A_a_a_prod_fun_a_b_b_prod_fun_fun$)
(declare-fun comp$be (A_a_tree_b_sum_a_tree_b_sum_prod_prod_b_b_tree_b_sum_b_tree_b_sum_prod_prod_fun$ B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$) B_b_b_tree_b_sum_b_tree_b_sum_prod_prod_fun$)
(declare-fun comp$bf (A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_b_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod_fun$ B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$) B_tree_b_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod_fun$)
(declare-fun comp$bg (A_a_tree_b_sum_a_tree_b_sum_prod_prod_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$) B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun_b_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun_fun$)
(declare-fun comp$bh (A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$) B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun_b_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun_fun$)
(declare-fun comp$bi (A_a_sum_b_b_sum_fun$ A_a_sum_a_a_sum_fun$) A_a_sum_b_b_sum_fun$)
(declare-fun comp$bj (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$ A_b_fun_b_tree_a_b_fun_sum_fun$) A_b_fun_b_tree_a_b_fun_sum_fun$)
(declare-fun comp$bk (A_b_fun_b_tree_a_b_fun_sum_fun$ A_b_fun_a_b_fun_fun$) A_b_fun_b_tree_a_b_fun_sum_fun$)
(declare-fun comp$bl (A_a_sum_b_fun$ A_a_sum_a_a_sum_fun$) A_a_sum_b_fun$)
(declare-fun comp$bm (A_b_fun_b_tree_fun$) A_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun$)
(declare-fun comp$bn (B_b_sum_b_fun$ B_b_sum_b_b_sum_fun$ B_b_sum$) B$)
(declare-fun comp$bo (B_b_sum_b_fun$ A_b_sum_b_b_sum_fun$ A_b_sum$) B$)
(declare-fun comp$bp (B_b_sum_b_fun$ B_tree_b_sum_b_b_sum_fun$ B_tree_b_sum$) B$)
(declare-fun comp$bq (B_tree_b_fun$) B_tree_b_tree_fun_b_tree_b_fun_fun$)
(declare-fun comp$br (B_b_tree_sum_b_fun$ B_b_tree_sum_b_b_tree_sum_fun$ B_b_tree_sum$) B$)
(declare-fun comp$bs (B_tree_b_sum_b_tree_fun$ B_b_sum_b_tree_b_sum_fun$ B_b_sum$) B_tree$)
(declare-fun comp$bt (B_b_tree_fun$) B_b_fun_b_b_tree_fun_fun$)
(declare-fun comp$bu (B_b_tree_sum_b_fun$ A_b_tree_sum_b_b_tree_sum_fun$ A_b_tree_sum$) B$)
(declare-fun comp$bv (B_b_tree_sum_b_fun$ B_tree_b_tree_sum_b_b_tree_sum_fun$ B_tree_b_tree_sum$) B$)
(declare-fun comp$bw (B_tree_b_sum_b_tree_fun$ B_tree_b_sum_b_tree_b_sum_fun$ B_tree_b_sum$) B_tree$)
(declare-fun comp$bx (B_tree_b_tree_sum_b_tree_fun$ B_b_tree_sum_b_tree_b_tree_sum_fun$ B_b_tree_sum$) B_tree$)
(declare-fun comp$by (B_tree_b_tree_sum_b_tree_fun$ B_tree_b_tree_sum_b_tree_b_tree_sum_fun$ B_tree_b_tree_sum$) B_tree$)
(declare-fun comp$bz (B_b_tree_b_tree_prod_prod_b_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$)
(declare-fun comp$ca (B_b_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$)
(declare-fun comp$cb (B_tree_b_tree_prod_b_tree_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_fun$)
(declare-fun comp$cc (B_tree_a_b_fun_sum_b_tree_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_fun$)
(declare-fun comp$cd (B_b_tree_b_tree_prod_prod_b_tree_b_tree_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_b_tree_prod_fun$)
(declare-fun comp$ce (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_b_tree_prod_fun$)
(declare-fun comp$cf (B_b_prod_b_fun$) B_b_b_prod_fun_b_b_fun_fun$)
(declare-fun comp$cg (B_tree_b_tree_prod_b_tree_fun$) B_tree_b_tree_b_tree_prod_fun_b_tree_b_tree_fun_fun$)
(declare-fun comp$ch (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_fun$)
(declare-fun comp$ci (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod$) B$)
(declare-fun comp$cj (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun_fun$)
(declare-fun convol$ (B_b_fun$ B_b_fun$) B_b_b_prod_fun$)
(declare-fun id_bnf$ (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun member$ (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$) Bool)
(declare-fun convol$a (B_b_tree_fun$ B_b_fun$ B$) B_tree_b_prod$)
(declare-fun convol$b (B_tree_b_tree_fun$ B_tree_b_fun$) B_tree_b_tree_b_prod_fun$)
(declare-fun convol$c (B_tree_b_fun$ B_tree_b_fun$ B_tree$) B_b_prod$)
(declare-fun convol$d (B_b_fun$ B_b_tree_fun$) B_b_b_tree_prod_fun$)
(declare-fun convol$e (B_b_tree_fun$ B_b_tree_fun$ B$) B_tree_b_tree_prod$)
(declare-fun convol$f (B_tree_b_tree_fun$ B_tree_b_tree_fun$) B_tree_b_tree_b_tree_prod_fun$)
(declare-fun convol$g (B_tree_b_fun$ B_tree_b_tree_fun$ B_tree$) B_b_tree_prod$)
(declare-fun convol$h (A_b_fun$) A_b_fun_a_b_b_prod_fun_fun$)
(declare-fun convol$i (A_a_fun$ A_a_fun$) A_a_a_prod_fun$)
(declare-fun fun_app$ (B_tree_b_tree_b_tree_prod_fun$ B_tree$) B_tree_b_tree_prod$)
(declare-fun id_bnf$a (B_b_tree_b_tree_prod_prod$) B_b_tree_b_tree_prod_prod$)
(declare-fun id_bnf$b (A_a_tree_a_tree_prod_prod$) A_a_tree_a_tree_prod_prod$)
(declare-fun id_bnf$c () A_a_fun$)
(declare-fun id_bnf$d (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun id_bnf$e (B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum$)
(declare-fun map_sum$ (A_tree_b_tree_fun$ B_b_fun$) A_tree_b_sum_b_tree_b_sum_fun$)
(declare-fun member$a (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$) Bool)
(declare-fun uncurry$ (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun case_sum$ (B_tree_b_tree_fun$) A_b_fun_b_tree_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$)
(declare-fun ctor_rec$ (A_b_fun$) A_b_fun$)
(declare-fun fun_app$a (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun fun_app$b (B_b_b_prod_fun$ B$) B_b_prod$)
(declare-fun fun_app$c (A_b_fun_b_tree_fun$ A_b_fun$) B_tree$)
(declare-fun fun_app$d (A_tree_b_tree_fun$ A_tree$) B_tree$)
(declare-fun fun_app$e (B_tree_b_tree_prod_b_tree_fun$ B_tree_b_tree_prod$) B_tree$)
(declare-fun fun_app$f (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_tree_a_b_fun_sum$)
(declare-fun fun_app$g (B_b_tree_b_tree_prod_prod_b_tree_b_tree_prod_fun$ B_b_tree_b_tree_prod_prod$) B_tree_b_tree_prod$)
(declare-fun fun_app$h (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun fun_app$i (B_b_prod_b_fun$ B_b_prod$) B$)
(declare-fun fun_app$j (B_b_tree_b_tree_prod_prod_b_fun$ B_b_tree_b_tree_prod_prod$) B$)
(declare-fun fun_app$k (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B$)
(declare-fun fun_app$l (A_b_fun_b_tree_a_b_fun_sum_fun$ A_b_fun$) B_tree_a_b_fun_sum$)
(declare-fun fun_app$m (B_tree_b_tree_a_b_fun_sum_fun$ B_tree$) B_tree_a_b_fun_sum$)
(declare-fun fun_app$n (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$ B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun fun_app$o (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun fun_app$p (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$ B$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun fun_app$q (B_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ B$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun fun_app$r (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun fun_app$s (B_tree_b_tree_fun_b_tree_b_tree_fun_fun$ B_tree_b_tree_fun$) B_tree_b_tree_fun$)
(declare-fun fun_app$t (B_b_fun_b_b_fun_fun$ B_b_fun$) B_b_fun$)
(declare-fun fun_app$u (A_b_fun_a_b_fun_fun$ A_b_fun$) A_b_fun$)
(declare-fun fun_app$v (A_a_fun_a_b_fun_fun$ A_a_fun$) A_b_fun$)
(declare-fun fun_app$w (B_tree_a_b_fun_sum_b_tree_fun$ B_tree_a_b_fun_sum$) B_tree$)
(declare-fun fun_app$x (B_tree_b_tree_fun$ B_tree$) B_tree$)
(declare-fun fun_app$y (B_tree_b_tree_fun_b_tree_fun$ B_tree_b_tree_fun$) B_tree$)
(declare-fun fun_app$z (B_b_fun_b_fun$ B_b_fun$) B$)
(declare-fun map_prod$ (B_b_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_sum$a (A_tree_b_tree_fun$ B_tree_b_tree_fun$) A_tree_b_tree_sum_b_tree_b_tree_sum_fun$)
(declare-fun map_sum$b (A_tree_a_tree_fun$ B_b_fun$) A_tree_b_sum_a_tree_b_sum_fun$)
(declare-fun map_sum$c (A_tree_a_tree_fun$ B_tree_b_tree_fun$) A_tree_b_tree_sum_a_tree_b_tree_sum_fun$)
(declare-fun map_sum$d (A_b_fun$ A_b_fun$) A_a_sum_b_b_sum_fun$)
(declare-fun map_sum$e (A_a_fun$ A_a_fun$) A_a_sum_a_a_sum_fun$)
(declare-fun map_sum$f (B_b_fun$ B_b_fun$) B_b_sum_b_b_sum_fun$)
(declare-fun map_sum$g (B_b_fun$ B_tree_b_tree_fun$) B_b_tree_sum_b_b_tree_sum_fun$)
(declare-fun map_sum$h (B_tree_b_tree_fun$ B_b_fun$) B_tree_b_sum_b_tree_b_sum_fun$)
(declare-fun map_sum$i (B_tree_b_tree_fun$ B_tree_b_tree_fun$) B_tree_b_tree_sum_b_tree_b_tree_sum_fun$)
(declare-fun map_sum$j (B_tree_b_tree_fun$) A_b_fun_a_b_fun_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_fun$)
(declare-fun map_sum$k (A_b_fun$ B_b_fun$) A_b_sum_b_b_sum_fun$)
(declare-fun map_sum$l (B_tree_b_fun$ B_b_fun$) B_tree_b_sum_b_b_sum_fun$)
(declare-fun map_sum$m (B_b_tree_fun$ B_b_fun$) B_b_sum_b_tree_b_sum_fun$)
(declare-fun map_sum$n (A_b_fun$ B_tree_b_tree_fun$) A_b_tree_sum_b_b_tree_sum_fun$)
(declare-fun map_sum$o (B_tree_b_fun$ B_tree_b_tree_fun$) B_tree_b_tree_sum_b_b_tree_sum_fun$)
(declare-fun map_sum$p (B_b_tree_fun$ B_tree_b_tree_fun$) B_b_tree_sum_b_tree_b_tree_sum_fun$)
(declare-fun map_tree$ (A_b_fun$) A_tree_b_tree_fun$)
(declare-fun uncurry$a (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun uncurry$b (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun uncurry$c (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun uncurry$d (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_b_tree_prod_fun_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)
(declare-fun case_sum$a (B_b_fun$ B_b_fun$) B_b_sum_b_fun$)
(declare-fun case_sum$b (A_b_fun$ B_tree_b_fun$ A_b_tree_sum$) B$)
(declare-fun case_sum$c (A_b_fun$ B_b_fun$ A_b_sum$) B$)
(declare-fun case_sum$d (A_b_fun$ A_b_fun$) A_a_sum_b_fun$)
(declare-fun case_sum$e (A_a_fun$) A_a_fun_a_a_sum_a_fun_fun$)
(declare-fun case_sum$f (B_tree_bool_fun$) A_b_fun_bool_fun_b_tree_a_b_fun_sum_bool_fun_fun$)
(declare-fun case_sum$g (B_tree_b_fun$ B_b_fun$ B_tree_b_sum$) B$)
(declare-fun case_sum$h (B_b_fun$ B_tree_b_fun$) B_b_tree_sum_b_fun$)
(declare-fun case_sum$i (B_tree_b_tree_fun$ B_b_tree_fun$) B_tree_b_sum_b_tree_fun$)
(declare-fun case_sum$j (B_b_tree_fun$ B_b_tree_fun$ B_b_sum$) B_tree$)
(declare-fun case_sum$k (B_tree_b_fun$ B_tree_b_fun$ B_tree_b_tree_sum$) B$)
(declare-fun case_sum$l (B_tree_b_tree_fun$ B_tree_b_tree_fun$) B_tree_b_tree_sum_b_tree_fun$)
(declare-fun case_sum$m (B_b_tree_fun$ B_tree_b_tree_fun$ B_b_tree_sum$) B_tree$)
(declare-fun ctor_tree$ (B_b_tree_b_tree_prod_prod$) B_tree$)
(declare-fun dtor_tree$ () B_tree_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun fun_app$aa (B_b_fun$ B$) B$)
(declare-fun fun_app$ab (A_b_fun_b_fun$ A_b_fun$) B$)
(declare-fun fun_app$ac (A_b_fun$ A$) B$)
(declare-fun fun_app$ad (B_tree_a_b_fun_sum_bool_fun$ B_tree_a_b_fun_sum$) Bool)
(declare-fun fun_app$ae (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_bool_fun_fun$ B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum_bool_fun$)
(declare-fun fun_app$af (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) Bool)
(declare-fun fun_app$ag (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun_fun$ B$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun$)
(declare-fun fun_app$ah (A_b_fun_b_tree_fun_a_b_fun_b_tree_fun_fun$ A_b_fun_b_tree_fun$) A_b_fun_b_tree_fun$)
(declare-fun fun_app$ai (B_tree_a_b_fun_sum_b_tree_b_tree_prod_fun$ B_tree_a_b_fun_sum$) B_tree_b_tree_prod$)
(declare-fun fun_app$aj (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_b_tree_prod_fun_fun$ B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum_b_tree_b_tree_prod_fun$)
(declare-fun fun_app$ak (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_b_tree_b_tree_prod_prod$)
(declare-fun fun_app$al (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun_fun$ B$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun fun_app$am (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_tree_b_tree_prod$)
(declare-fun fun_app$an (A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ A_b_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun fun_app$ao (A_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$ A_b_fun_a_b_fun_fun$) A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun fun_app$ap (A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun$ A_b_fun_b_tree_fun$) A_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun$)
(declare-fun fun_app$aq (A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun$ A_b_fun_bool_fun$) A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun$)
(declare-fun fun_app$ar (A_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun$ A_b_fun_a_b_fun_fun$) A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun$)
(declare-fun fun_app$as (A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun_fun$ A_b_fun_b_tree_fun$) A_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun$)
(declare-fun fun_app$at (A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun_fun_fun$ A_b_fun_bool_fun$) A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun_fun_fun_fun_fun_fun$)
(declare-fun fun_app$au (A_b_fun_bool_fun$ A_b_fun$) Bool)
(declare-fun fun_app$av (B_tree_b_fun$ B_tree$) B$)
(declare-fun fun_app$aw (A_a_fun$ A$) A$)
(declare-fun fun_app$ax (B_tree_b_tree_prod_b_tree_b_tree_prod_fun$ B_tree_b_tree_prod$) B_tree_b_tree_prod$)
(declare-fun fun_app$ay (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun fun_app$az (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_b_tree_b_tree_prod_prod$)
(declare-fun fun_app$ba (B_tree_a_b_fun_sum_b_tree_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$ B_tree_a_b_fun_sum_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)
(declare-fun fun_app$bb (A_b_fun_b_tree_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$ A_b_fun_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_fun$)
(declare-fun fun_app$bc (B_tree_b_b_tree_b_tree_prod_prod_fun$ B_tree$) B_b_tree_b_tree_prod_prod$)
(declare-fun fun_app$bd (A_tree_a_a_tree_a_tree_prod_prod_fun$ A_tree$) A_a_tree_a_tree_prod_prod$)
(declare-fun fun_app$be (B_tree_a_tree_fun$ B_tree$) A_tree$)
(declare-fun fun_app$bf (A_tree_a_tree_fun$ A_tree$) A_tree$)
(declare-fun fun_app$bg (A_b_fun_a_a_fun_fun$ A_b_fun$) A_a_fun$)
(declare-fun fun_app$bh (A_a_fun_a_a_fun_fun$ A_a_fun$) A_a_fun$)
(declare-fun fun_app$bi (B_a_fun_b_b_fun_fun$ B_a_fun$) B_b_fun$)
(declare-fun fun_app$bj (B_a_fun_b_a_fun_fun$ B_a_fun$) B_a_fun$)
(declare-fun fun_app$bk (B_b_fun_b_a_fun_fun$ B_b_fun$) B_a_fun$)
(declare-fun fun_app$bl (A_tree_b_b_prod_tree_fun$ A_tree$) B_b_prod_tree$)
(declare-fun fun_app$bm (A_a_fun_a_b_b_prod_fun_fun$ A_a_fun$) A_b_b_prod_fun$)
(declare-fun fun_app$bn (A_a_sum_tree_a_tree_fun$ A_a_sum_tree$) A_tree$)
(declare-fun fun_app$bo (A_a_sum_tree_b_tree_fun$ A_a_sum_tree$) B_tree$)
(declare-fun fun_app$bp (A_tree_b_tree_fun_a_tree_b_tree_fun_fun$ A_tree_b_tree_fun$) A_tree_b_tree_fun$)
(declare-fun fun_app$bq (A_tree_a_tree_fun_a_tree_b_tree_fun_fun$ A_tree_a_tree_fun$) A_tree_b_tree_fun$)
(declare-fun fun_app$br (A_tree_b_tree_fun_a_tree_a_tree_fun_fun$ A_tree_b_tree_fun$) A_tree_a_tree_fun$)
(declare-fun fun_app$bs (A_tree_a_tree_fun_a_tree_a_tree_fun_fun$ A_tree_a_tree_fun$) A_tree_a_tree_fun$)
(declare-fun fun_app$bt (B_tree_a_tree_fun_b_tree_b_tree_fun_fun$ B_tree_a_tree_fun$) B_tree_b_tree_fun$)
(declare-fun fun_app$bu (B_tree_tree_b_tree_tree_fun$ B_tree_tree$) B_tree_tree$)
(declare-fun fun_app$bv (B_b_sum_tree_b_b_sum_tree_fun$ B_b_sum_tree$) B_b_sum_tree$)
(declare-fun fun_app$bw (B_tree_b_tree_fun_tree_b_tree_b_tree_fun_tree_fun$ B_tree_b_tree_fun_tree$) B_tree_b_tree_fun_tree$)
(declare-fun fun_app$bx (B_b_fun_tree_b_b_fun_tree_fun$ B_b_fun_tree$) B_b_fun_tree$)
(declare-fun fun_app$by (A_b_fun_tree_a_b_fun_tree_fun$ A_b_fun_tree$) A_b_fun_tree$)
(declare-fun fun_app$bz (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)
(declare-fun fun_app$ca (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$ B_tree_a_b_fun_sum$) B_tree_a_b_fun_sum$)
(declare-fun fun_app$cb (B_b_tree_a_b_fun_sum_fun$ B$) B_tree_a_b_fun_sum$)
(declare-fun fun_app$cc (B_tree_a_b_fun_sum_b_fun$ B_tree_a_b_fun_sum$) B$)
(declare-fun fun_app$cd (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun fun_app$ce (B_b_prod_b_b_prod_fun$ B_b_prod$) B_b_prod$)
(declare-fun fun_app$cf (A_a_prod_b_b_prod_fun$ A_a_prod$) B_b_prod$)
(declare-fun fun_app$cg (A_a_prod_a_a_prod_fun$ A_a_prod$) A_a_prod$)
(declare-fun fun_app$ch (A_tree_b_fun$ A_tree$) B$)
(declare-fun fun_app$ci (B_b_sum_b_fun$ B_b_sum$) B$)
(declare-fun fun_app$cj (A_a_sum_b_fun$ A_a_sum$) B$)
(declare-fun fun_app$ck (A_a_sum_a_fun$ A_a_sum$) A$)
(declare-fun fun_app$cl (A_a_fun_a_a_sum_a_fun_fun$ A_a_fun$) A_a_sum_a_fun$)
(declare-fun fun_app$cm (B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ B_b_tree_b_tree_prod_prod$) B_b_tree_b_tree_prod_prod$)
(declare-fun fun_app$cn (B_b_sum_b_b_sum_fun$ B_b_sum$) B_b_sum$)
(declare-fun fun_app$co (B_a_fun$ B$) A$)
(declare-fun fun_app$cp (A_b_b_prod_fun$ A$) B_b_prod$)
(declare-fun fun_app$cq (B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_bool_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) Bool)
(declare-fun fun_app$cr (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)
(declare-fun fun_app$cs (B_tree_b_tree_fun_b_tree_b_tree_prod_b_tree_b_tree_prod_fun_fun$ B_tree_b_tree_fun$) B_tree_b_tree_prod_b_tree_b_tree_prod_fun$)
(declare-fun fun_app$ct (B_tree_a_b_fun_sum_b_tree_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$ B_tree_a_b_fun_sum_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_fun$)
(declare-fun fun_app$cu (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)
(declare-fun fun_app$cv (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_b_tree_a_b_fun_sum_b_tree_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_fun$)
(declare-fun fun_app$cw (B_b_tree_prod_b_b_tree_prod_fun$ B_b_tree_prod$) B_b_tree_prod$)
(declare-fun fun_app$cx (B_tree_b_prod_b_tree_b_prod_fun$ B_tree_b_prod$) B_tree_b_prod$)
(declare-fun fun_app$cy (A_b_fun_b_tree_a_b_fun_sum_fun_a_b_fun_b_tree_fun_fun$ A_b_fun_b_tree_a_b_fun_sum_fun$) A_b_fun_b_tree_fun$)
(declare-fun fun_app$cz (A_a_fun_a_a_tree_fun_fun$ A_a_fun$) A_a_tree_fun$)
(declare-fun fun_app$da (A_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun$ A_a_tree_fun$) A_a_fun_a_a_tree_fun_fun$)
(declare-fun fun_app$db (A_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun$ A_bool_fun$) A_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun$)
(declare-fun fun_app$dc (A_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun$ A_a_fun$) A_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun$)
(declare-fun fun_app$dd (A_a_tree_fun_a_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun_fun$ A_a_tree_fun$) A_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun$)
(declare-fun fun_app$de (A_bool_fun_a_a_tree_fun_a_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun_fun_fun$ A_bool_fun$) A_a_tree_fun_a_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun_fun$)
(declare-fun fun_app$df (A_b_fun_bool_fun_b_tree_a_b_fun_sum_bool_fun_fun$ A_b_fun_bool_fun$) B_tree_a_b_fun_sum_bool_fun$)
(declare-fun fun_app$dg (B_tree_bool_fun$ B_tree$) Bool)
(declare-fun fun_app$dh (A_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun$ A_b_fun_a_b_fun_fun$) A_b_fun_b_tree_fun$)
(declare-fun fun_app$di (A_b_fun_a_b_fun_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun$ A_b_fun_a_b_fun_fun$) A_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun$)
(declare-fun fun_app$dj (A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun$ A_b_fun_b_tree_fun$) A_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun$)
(declare-fun fun_app$dk (A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun$ A_b_fun_bool_fun$) A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun$)
(declare-fun fun_app$dl (A_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun$ A_b_fun_a_b_fun_fun$) A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun$)
(declare-fun fun_app$dm (A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun_fun$ A_b_fun_b_tree_fun$) A_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun$)
(declare-fun fun_app$dn (A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun_fun_fun$ A_b_fun_bool_fun$) A_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun_fun$)
(declare-fun fun_app$do (B_tree_b_tree_a_b_fun_sum_fun_b_tree_b_tree_fun_fun$ B_tree_b_tree_a_b_fun_sum_fun$) B_tree_b_tree_fun$)
(declare-fun fun_app$dp (A_a_tree_fun$ A$) A_tree$)
(declare-fun fun_app$dq (A_a_fun_a_a_fun_a_a_tree_fun_fun_fun$ A_a_fun$) A_a_fun_a_a_tree_fun_fun$)
(declare-fun fun_app$dr (A_a_a_prod_prod_b_b_b_prod_prod_fun$ A_a_a_prod_prod$) B_b_b_prod_prod$)
(declare-fun fun_app$ds (A_a_a_prod_prod_a_a_a_prod_prod_fun$ A_a_a_prod_prod$) A_a_a_prod_prod$)
(declare-fun fun_app$dt (B_b_b_prod_prod_b_b_b_prod_prod_fun$ B_b_b_prod_prod$) B_b_b_prod_prod$)
(declare-fun fun_app$du (B_tree_b_b_prod_prod_b_tree_b_b_prod_prod_fun$ B_tree_b_b_prod_prod$) B_tree_b_b_prod_prod$)
(declare-fun fun_app$dv (B_tree_b_tree_b_tree_prod_prod_b_tree_b_tree_b_tree_prod_prod_fun$ B_tree_b_tree_b_tree_prod_prod$) B_tree_b_tree_b_tree_prod_prod$)
(declare-fun fun_app$dw (B_a_tree_fun_b_b_tree_fun_fun$ B_a_tree_fun$) B_b_tree_fun$)
(declare-fun fun_app$dx (B_a_b_b_prod_prod_fun_b_a_b_b_prod_prod_fun_fun$ B_a_b_b_prod_prod_fun$) B_a_b_b_prod_prod_fun$)
(declare-fun fun_app$dy (B_tree_a_b_tree_b_tree_prod_prod_fun_b_tree_a_b_tree_b_tree_prod_prod_fun_fun$ B_tree_a_b_tree_b_tree_prod_prod_fun$) B_tree_a_b_tree_b_tree_prod_prod_fun$)
(declare-fun fun_app$dz (B_b_tree_fun$ B$) B_tree$)
(declare-fun fun_app$ea (B_b_fun_b_b_tree_fun_fun$ B_b_fun$) B_b_tree_fun$)
(declare-fun fun_app$eb (B_b_tree_fun_b_b_tree_fun_fun$ B_b_tree_fun$) B_b_tree_fun$)
(declare-fun fun_app$ec (B_tree_b_fun_b_tree_b_fun_fun$ B_tree_b_fun$) B_tree_b_fun$)
(declare-fun fun_app$ed (B_tree_b_tree_b_prod_fun$ B_tree$) B_tree_b_prod$)
(declare-fun fun_app$ee (B_b_b_tree_prod_fun$ B$) B_b_tree_prod$)
(declare-fun fun_app$ef (A_a_tree_a_tree_prod_prod_a_a_tree_a_tree_prod_prod_fun$ A_a_tree_a_tree_prod_prod$) A_a_tree_a_tree_prod_prod$)
(declare-fun fun_app$eg (A_a_tree_a_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$ A_a_tree_a_tree_prod_prod$) B_b_tree_b_tree_prod_prod$)
(declare-fun fun_app$eh (A_b_fun_a_b_b_prod_fun_fun$ A_b_fun$) A_b_b_prod_fun$)
(declare-fun fun_app$ei (A_a_a_prod_fun_a_b_b_prod_fun_fun$ A_a_a_prod_fun$) A_b_b_prod_fun$)
(declare-fun fun_app$ej (B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun_b_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun_fun$ B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$) B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$)
(declare-fun fun_app$ek (B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun_b_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun_fun$ B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$) B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$)
(declare-fun fun_app$el (A_a_sum_b_b_sum_fun$ A_a_sum$) B_b_sum$)
(declare-fun fun_app$em (A_a_sum_a_a_sum_fun$ A_a_sum$) A_a_sum$)
(declare-fun fun_app$en (B_b_tree_sum_b_b_tree_sum_fun$ B_b_tree_sum$) B_b_tree_sum$)
(declare-fun fun_app$eo (B_tree_b_sum_b_tree_b_sum_fun$ B_tree_b_sum$) B_tree_b_sum$)
(declare-fun fun_app$ep (B_tree_b_tree_sum_b_tree_b_tree_sum_fun$ B_tree_b_tree_sum$) B_tree_b_tree_sum$)
(declare-fun fun_app$eq (A_b_fun_a_b_fun_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_fun$ A_b_fun_a_b_fun_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$)
(declare-fun fun_app$er (B_tree_b_tree_fun_b_tree_b_fun_fun$ B_tree_b_tree_fun$) B_tree_b_fun$)
(declare-fun fun_app$es (B_b_tree_sum_b_fun$ B_b_tree_sum$) B$)
(declare-fun fun_app$et (B_tree_b_sum_b_tree_fun$ B_tree_b_sum$) B_tree$)
(declare-fun fun_app$eu (B_tree_b_tree_sum_b_tree_fun$ B_tree_b_tree_sum$) B_tree$)
(declare-fun fun_app$ev (A_bool_fun$ A$) Bool)
(declare-fun fun_app$ew (B_bool_fun$ B$) Bool)
(declare-fun fun_app$ex (B_b_bool_fun_fun$ B$) B_bool_fun$)
(declare-fun fun_app$ey (B_b_fun_b_b_bool_fun_fun_fun$ B_b_fun$) B_b_bool_fun_fun$)
(declare-fun fun_app$ez (B_b_b_fun_b_b_bool_fun_fun_fun_fun$ B$) B_b_fun_b_b_bool_fun_fun_fun$)
(declare-fun fun_app$fa (B_b_fun_b_b_b_fun_b_b_bool_fun_fun_fun_fun_fun$ B_b_fun$) B_b_b_fun_b_b_bool_fun_fun_fun_fun$)
(declare-fun fun_app$fb (B_tree_b_tree_bool_fun_fun$ B_tree$) B_tree_bool_fun$)
(declare-fun fun_app$fc (B_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun$ B_tree_b_tree_fun$) B_tree_b_tree_bool_fun_fun$)
(declare-fun fun_app$fd (B_tree_b_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun_fun$ B_tree$) B_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun$)
(declare-fun fun_app$fe (B_tree_b_tree_fun_b_tree_b_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun_fun_fun$ B_tree_b_tree_fun$) B_tree_b_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun_fun$)
(declare-fun fun_app$ff (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_bool_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_bool_fun$)
(declare-fun fun_app$fg (B_b_b_prod_fun_b_b_fun_fun$ B_b_b_prod_fun$) B_b_fun$)
(declare-fun fun_app$fh (B_tree_b_tree_b_tree_prod_fun_b_tree_b_tree_fun_fun$ B_tree_b_tree_b_tree_prod_fun$) B_tree_b_tree_fun$)
(declare-fun fun_app$fi (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$)
(declare-fun fun_app$fj (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$)
(declare-fun map_prod$a (B_tree_a_b_fun_sum_b_tree_fun$) B_tree_a_b_fun_sum_b_tree_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun_fun$)
(declare-fun map_prod$b (B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun_fun$)
(declare-fun map_prod$c (B_b_tree_a_b_fun_sum_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$ B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)
(declare-fun map_prod$d (B_tree_a_b_fun_sum_b_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)
(declare-fun map_prod$e (B_b_fun$ B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)
(declare-fun map_prod$f (B_b_fun$ B_b_fun$) B_b_prod_b_b_prod_fun$)
(declare-fun map_prod$g (A_b_fun$ A_b_fun$) A_a_prod_b_b_prod_fun$)
(declare-fun map_prod$h (A_a_fun$ A_a_fun$) A_a_prod_a_a_prod_fun$)
(declare-fun map_prod$i (A_tree_b_fun$ A_tree_b_fun$ A_tree_a_tree_prod$) B_b_prod$)
(declare-fun map_prod$j (B_b_fun$ B_tree_b_tree_prod_b_tree_b_tree_prod_fun$) B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_prod$k (B_tree_b_tree_fun$) B_tree_b_tree_fun_b_tree_b_tree_prod_b_tree_b_tree_prod_fun_fun$)
(declare-fun map_prod$l (B_b_fun$ B_tree_b_tree_fun$) B_b_tree_prod_b_b_tree_prod_fun$)
(declare-fun map_prod$m (B_tree_b_tree_fun$ B_b_fun$) B_tree_b_prod_b_tree_b_prod_fun$)
(declare-fun map_prod$n (B_b_tree_fun$ B_b_fun$) B_b_prod_b_tree_b_prod_fun$)
(declare-fun map_prod$o (B_tree_b_fun$ B_b_fun$) B_tree_b_prod_b_b_prod_fun$)
(declare-fun map_prod$p (B_b_tree_fun$ B_tree_b_tree_fun$) B_b_tree_prod_b_tree_b_tree_prod_fun$)
(declare-fun map_prod$q (B_tree_b_fun$ B_tree_b_tree_fun$) B_tree_b_tree_prod_b_b_tree_prod_fun$)
(declare-fun map_tree$a (B_b_fun$) B_tree_b_tree_fun$)
(declare-fun map_tree$b (B_a_fun$) B_tree_a_tree_fun$)
(declare-fun map_tree$c (A_a_fun$) A_tree_a_tree_fun$)
(declare-fun map_tree$d (A_b_b_prod_fun$) A_tree_b_b_prod_tree_fun$)
(declare-fun map_tree$e (A_a_sum_a_fun$) A_a_sum_tree_a_tree_fun$)
(declare-fun map_tree$f (A_a_sum_b_fun$) A_a_sum_tree_b_tree_fun$)
(declare-fun map_tree$g (B_tree_b_tree_fun$) B_tree_tree_b_tree_tree_fun$)
(declare-fun map_tree$h (B_b_sum_b_b_sum_fun$) B_b_sum_tree_b_b_sum_tree_fun$)
(declare-fun map_tree$i (B_tree_b_tree_fun_b_tree_b_tree_fun_fun$) B_tree_b_tree_fun_tree_b_tree_b_tree_fun_tree_fun$)
(declare-fun map_tree$j (B_b_fun_b_b_fun_fun$) B_b_fun_tree_b_b_fun_tree_fun$)
(declare-fun map_tree$k (A_b_fun_a_b_fun_fun$) A_b_fun_tree_a_b_fun_tree_fun$)
(declare-fun pred_tree$ (A_bool_fun$ A_tree$) Bool)
(declare-fun corec_tree$ (A_a_fun$) A_bool_fun_a_a_tree_fun_a_a_fun_a_bool_fun_a_a_tree_fun_a_a_fun_a_a_tree_fun_fun_fun_fun_fun_fun_fun$)
(declare-fun ctor_tree$a (A_a_tree_a_tree_prod_prod$) A_tree$)
(declare-fun dtor_tree$a () A_tree_a_a_tree_a_tree_prod_prod_fun$)
(declare-fun corec_tree$a (A_b_fun$ A_bool_fun$ A_b_tree_fun$ A_a_fun$ A_bool_fun$ A_b_tree_fun$ A_a_fun$) A_b_tree_fun$)
(declare-fun corec_tree$b (A_b_fun_b_fun$) A_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_bool_fun_a_b_fun_b_tree_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun_fun_fun_fun_fun$)
(declare-fun unfold_tree$ (A_b_fun_b_fun$) A_b_fun_a_b_fun_fun_a_b_fun_a_b_fun_fun_a_b_fun_b_tree_fun_fun_fun$)
(declare-fun map_pre_tree$ (B_b_fun$ B_tree_a_b_fun_sum_b_tree_fun$) B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun tree_recurse$ (B_b_fun$) B_b_fun_b_b_tree_fun_fun$)
(declare-fun unfold_tree$a (A_a_fun$) A_a_fun_a_a_fun_a_a_tree_fun_fun_fun$)
(declare-fun unfold_tree$b (A_b_fun$ A_a_fun$ A_a_fun$ A$) B_tree$)
(declare-fun unfold_tree$c (B_b_fun_b_fun$ B_b_fun_b_b_fun_fun$ B_b_fun_b_b_fun_fun$ B_b_fun$) B_tree$)
(declare-fun unfold_tree$d (B_tree_b_tree_fun_b_tree_fun$ B_tree_b_tree_fun_b_tree_b_tree_fun_fun$ B_tree_b_tree_fun_b_tree_b_tree_fun_fun$ B_tree_b_tree_fun$) B_tree_tree$)
(declare-fun map_pre_tree$a (A_b_fun$ A_b_fun$) A_a_a_prod_prod_b_b_b_prod_prod_fun$)
(declare-fun map_pre_tree$b (A_a_fun$ A_a_fun$) A_a_a_prod_prod_a_a_a_prod_prod_fun$)
(declare-fun map_pre_tree$c (B_b_fun$ B_b_fun$) B_b_b_prod_prod_b_b_b_prod_prod_fun$)
(declare-fun map_pre_tree$d (B_b_fun$ B_tree_b_tree_fun$) B_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_pre_tree$e (B_tree_b_tree_fun$ B_b_fun$) B_tree_b_b_prod_prod_b_tree_b_b_prod_prod_fun$)
(declare-fun map_pre_tree$f (B_tree_b_tree_fun$ B_tree_b_tree_fun$) B_tree_b_tree_b_tree_prod_prod_b_tree_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_pre_tree$g (A_b_fun$ B_b_fun$) A_b_b_prod_prod_b_b_b_prod_prod_fun$)
(declare-fun map_pre_tree$h (A_b_fun$ B_tree_b_tree_fun$) A_b_tree_b_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_pre_tree$i (A_a_fun$ B_b_fun$) A_b_b_prod_prod_a_b_b_prod_prod_fun$)
(declare-fun map_pre_tree$j (A_a_fun$ B_tree_b_tree_fun$) A_b_tree_b_tree_prod_prod_a_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_pre_tree$k (A_a_fun$ A_tree_a_tree_fun$) A_a_tree_a_tree_prod_prod_a_a_tree_a_tree_prod_prod_fun$)
(declare-fun map_pre_tree$l (A_b_fun$ A_tree_b_tree_fun$) A_a_tree_a_tree_prod_prod_b_b_tree_b_tree_prod_prod_fun$)
(declare-fun map_pre_tree$m (A_b_fun$ A_tree_b_sum_b_tree_b_sum_fun$) A_a_tree_b_sum_a_tree_b_sum_prod_prod_b_b_tree_b_sum_b_tree_b_sum_prod_prod_fun$)
(declare-fun map_pre_tree$n (A_b_fun$ A_tree_b_tree_sum_b_tree_b_tree_sum_fun$) A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_b_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod_fun$)
(declare-fun map_pre_tree$o (A_a_fun$ A_tree_b_sum_a_tree_b_sum_fun$) A_a_tree_b_sum_a_tree_b_sum_prod_prod_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$)
(declare-fun map_pre_tree$p (A_a_fun$ A_tree_b_tree_sum_a_tree_b_tree_sum_fun$) A_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$)
(declare-fun tree_recurse$a (B_tree_b_tree_fun$ B_tree_b_tree_fun$ B_tree$) B_tree_tree$)
(declare-fun tree_recurse$b (A_a_fun$) A_a_fun_a_a_tree_fun_fun$)
(declare-fun dtor_corec_tree$ (A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$) A_b_fun_b_tree_fun$)
(declare-fun dtor_corec_tree$a (B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$) B_a_tree_fun$)
(declare-fun dtor_corec_tree$b (B_b_b_tree_b_sum_b_tree_b_sum_prod_prod_fun$) B_b_tree_fun$)
(declare-fun dtor_corec_tree$c (B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$) B_tree_a_tree_fun$)
(declare-fun dtor_corec_tree$d (B_tree_b_b_tree_b_tree_sum_b_tree_b_tree_sum_prod_prod_fun$) B_tree_b_tree_fun$)
(declare-fun dtor_unfold_tree$ (B_a_b_b_prod_prod_fun$) B_a_tree_fun$)
(declare-fun dtor_unfold_tree$a (B_b_b_b_prod_prod_fun$) B_b_tree_fun$)
(declare-fun dtor_unfold_tree$b (B_tree_a_b_tree_b_tree_prod_prod_fun$) B_tree_a_tree_fun$)
(declare-fun dtor_unfold_tree$c (B_tree_b_b_tree_b_tree_prod_prod_fun$) B_tree_b_tree_fun$)
(declare-fun iso_tuple_update_accessor_eq_assist$ (B_b_fun_b_b_fun_fun$) B_b_fun_b_b_b_fun_b_b_bool_fun_fun_fun_fun_fun$)
(declare-fun iso_tuple_update_accessor_eq_assist$a (B_tree_b_tree_fun_b_tree_b_tree_fun_fun$) B_tree_b_tree_fun_b_tree_b_tree_b_tree_fun_b_tree_b_tree_bool_fun_fun_fun_fun_fun$)
(assert (forall ((?v0 B_tree$)) (! (= (fun_app$ uvk$ ?v0) (pair$ ?v0 ?v0)) :pattern ((fun_app$ uvk$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum$)) (! (= (fun_app$a uvl$ ?v0) (pair$b ?v0 ?v0)) :pattern ((fun_app$a uvl$ ?v0)))))
(assert (forall ((?v0 B$)) (! (= (fun_app$b uvj$ ?v0) (pair$f ?v0 ?v0)) :pattern ((fun_app$b uvj$ ?v0)))))
(assert (forall ((?v0 A_b_fun$)) (! (= (fun_app$c uu$ ?v0) (fun_app$d (map_tree$ ?v0) t$)) :pattern ((fun_app$c uu$ ?v0)))))
(assert (forall ((?v0 B_tree_b_tree_prod$)) (! (= (fun_app$e uvg$ ?v0) (snd$ ?v0)) :pattern ((fun_app$e uvg$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$f uvh$ ?v0) (snd$b ?v0)) :pattern ((fun_app$f uvh$ ?v0)))))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (! (= (fun_app$g uve$ ?v0) (snd$a ?v0)) :pattern ((fun_app$g uve$ ?v0)))))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (! (= (fun_app$h uvf$ ?v0) (snd$c ?v0)) :pattern ((fun_app$h uvf$ ?v0)))))
(assert (forall ((?v0 B_b_prod$)) (! (= (fun_app$i uvi$ ?v0) (snd$f ?v0)) :pattern ((fun_app$i uvi$ ?v0)))))
(assert (forall ((?v0 B_tree_b_tree_prod$)) (! (= (fun_app$e uvc$ ?v0) (fst$ ?v0)) :pattern ((fun_app$e uvc$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$f uvd$ ?v0) (fst$b ?v0)) :pattern ((fun_app$f uvd$ ?v0)))))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (! (= (fun_app$j uva$ ?v0) (fst$a ?v0)) :pattern ((fun_app$j uva$ ?v0)))))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (! (= (fun_app$k uvb$ ?v0) (fst$c ?v0)) :pattern ((fun_app$k uvb$ ?v0)))))
(assert (forall ((?v0 B_b_prod$)) (! (= (fun_app$i uvm$ ?v0) (fst$f ?v0)) :pattern ((fun_app$i uvm$ ?v0)))))
(assert (forall ((?v0 A_b_fun$)) (! (= (fun_app$l uun$ ?v0) (inr$ ?v0)) :pattern ((fun_app$l uun$ ?v0)))))
(assert (forall ((?v0 B_tree$)) (! (= (fun_app$m uur$ ?v0) (inl$ ?v0)) :pattern ((fun_app$m uur$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$)) (! (= (fun_app$a (fun_app$n uvq$ ?v0) ?v1) (pair$b ?v0 ?v1)) :pattern ((fun_app$a (fun_app$n uvq$ ?v0) ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$o (fun_app$p uvp$ ?v0) ?v1) (pair$c ?v0 ?v1)) :pattern ((fun_app$o (fun_app$p uvp$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B$)) (! (= (fun_app$q (fun_app$r uvn$ ?v0) ?v1) (pair$c ?v1 ?v0)) :pattern ((fun_app$q (fun_app$r uvn$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$)) (! (= (fun_app$a (fun_app$n uvo$ ?v0) ?v1) (pair$b ?v1 ?v0)) :pattern ((fun_app$a (fun_app$n uvo$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$)) (! (= (fun_app$s (uux$ ?v0) ?v1) (fun_app$s (comp$ ?v1) ?v0)) :pattern ((fun_app$s (uux$ ?v0) ?v1)))))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$)) (! (= (fun_app$t (uuv$ ?v0) ?v1) (fun_app$t (comp$a ?v1) ?v0)) :pattern ((fun_app$t (uuv$ ?v0) ?v1)))))
(assert (forall ((?v0 A_a_fun$) (?v1 A_b_fun$)) (! (= (fun_app$u (uup$ ?v0) ?v1) (fun_app$v (comp$b ?v1) ?v0)) :pattern ((fun_app$u (uup$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 A_b_fun$)) (! (= (fun_app$c (uut$ ?v0) ?v1) (fun_app$w ?v0 (inr$ ?v1))) :pattern ((fun_app$c (uut$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree$)) (! (= (fun_app$x (uus$ ?v0) ?v1) (fun_app$w ?v0 (inl$ ?v1))) :pattern ((fun_app$x (uus$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree$) (?v1 B_tree_b_tree_fun$)) (! (= (fun_app$y (uuw$ ?v0) ?v1) (fun_app$x ?v1 ?v0)) :pattern ((fun_app$y (uuw$ ?v0) ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_b_fun$)) (! (= (fun_app$z (uuu$ ?v0) ?v1) (fun_app$aa ?v1 ?v0)) :pattern ((fun_app$z (uuu$ ?v0) ?v1)))))
(assert (forall ((?v0 A$) (?v1 A_b_fun$)) (! (= (fun_app$ab (uuo$ ?v0) ?v1) (fun_app$ac ?v1 ?v0)) :pattern ((fun_app$ab (uuo$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (! (= (fun_app$ad (fun_app$ae (uuz$ ?v0) ?v1) ?v2) (member$ (pair$b ?v1 ?v2) ?v0)) :pattern ((fun_app$ad (fun_app$ae (uuz$ ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$af (fun_app$ag (uuy$ ?v0) ?v1) ?v2) (member$a (pair$c ?v1 ?v2) ?v0)) :pattern ((fun_app$af (fun_app$ag (uuy$ ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree$)) (! (= (fun_app$x (fun_app$s (uul$ ?v0) ?v1) ?v2) (fun_app$x ?v0 (fun_app$x ?v1 ?v2))) :pattern ((fun_app$x (fun_app$s (uul$ ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 A_b_fun$)) (! (= (fun_app$c (fun_app$ah (uum$ ?v0) ?v1) ?v2) (fun_app$x ?v0 (fun_app$c ?v1 ?v2))) :pattern ((fun_app$c (fun_app$ah (uum$ ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (! (= (fun_app$ai (fun_app$aj (uvs$ ?v0 ?v1) ?v2) ?v3) (pair$ (fun_app$w ?v0 ?v2) (fun_app$w ?v1 ?v3))) :pattern ((fun_app$ai (fun_app$aj (uvs$ ?v0 ?v1) ?v2) ?v3)))))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$ak (fun_app$al (uvr$ ?v0 ?v1) ?v2) ?v3) (pair$a (fun_app$aa ?v0 ?v2) (fun_app$am ?v1 ?v3))) :pattern ((fun_app$ak (fun_app$al (uvr$ ?v0 ?v1) ?v2) ?v3)))))
(assert (forall ((?v0 A_b_fun_b_fun$) (?v1 A_b_fun_bool_fun$) (?v2 A_b_fun_b_tree_fun$) (?v3 A_b_fun_a_b_fun_fun$) (?v4 A_b_fun_bool_fun$) (?v5 A_b_fun_b_tree_fun$) (?v6 A_b_fun_a_b_fun_fun$) (?v7 A_b_fun$)) (! (= (fun_app$an (fun_app$ao (fun_app$ap (fun_app$aq (fun_app$ar (fun_app$as (fun_app$at (uuq$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) ?v6) ?v7) (id_bnf$ (pair$c (fun_app$ab ?v0 ?v7) (pair$b (ite (fun_app$au ?v1 ?v7) (inl$ (fun_app$c ?v2 ?v7)) (inr$ (fun_app$u ?v3 ?v7))) (ite (fun_app$au ?v4 ?v7) (inl$ (fun_app$c ?v5 ?v7)) (inr$ (fun_app$u ?v6 ?v7))))))) :pattern ((fun_app$an (fun_app$ao (fun_app$ap (fun_app$aq (fun_app$ar (fun_app$as (fun_app$at (uuq$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) ?v6) ?v7)))))
(assert (forall ((?v0 B_tree$) (?v1 B_tree$)) (! (= (fun_app$x (uuh$ ?v0) ?v1) ?v0) :pattern ((fun_app$x (uuh$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree$) (?v1 A_b_fun$)) (! (= (fun_app$c (uui$ ?v0) ?v1) ?v0) :pattern ((fun_app$c (uui$ ?v0) ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_tree$)) (! (= (fun_app$av (uuf$ ?v0) ?v1) ?v0) :pattern ((fun_app$av (uuf$ ?v0) ?v1)))))
(assert (forall ((?v0 B$) (?v1 B$)) (! (= (fun_app$aa (uud$ ?v0) ?v1) ?v0) :pattern ((fun_app$aa (uud$ ?v0) ?v1)))))
(assert (forall ((?v0 B$) (?v1 A$)) (! (= (fun_app$ac (uue$ ?v0) ?v1) ?v0) :pattern ((fun_app$ac (uue$ ?v0) ?v1)))))
(assert (forall ((?v0 A$) (?v1 A$)) (! (= (fun_app$aw (uug$ ?v0) ?v1) ?v0) :pattern ((fun_app$aw (uug$ ?v0) ?v1)))))
(assert (forall ((?v0 B_tree$)) (! (= (fun_app$x uub$ ?v0) ?v0) :pattern ((fun_app$x uub$ ?v0)))))
(assert (forall ((?v0 B_tree_b_tree_prod$)) (! (= (fun_app$ax uuj$ ?v0) ?v0) :pattern ((fun_app$ax uuj$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$ay uuk$ ?v0) ?v0) :pattern ((fun_app$ay uuk$ ?v0)))))
(assert (forall ((?v0 B$)) (! (= (fun_app$aa uua$ ?v0) ?v0) :pattern ((fun_app$aa uua$ ?v0)))))
(assert (forall ((?v0 A$)) (! (= (fun_app$aw uuc$ ?v0) ?v0) :pattern ((fun_app$aw uuc$ ?v0)))))
(assert (not (forall ((?v0 A_b_fun$)) (= (id_bnf$a (fun_app$az (map_prod$ id$ (fun_app$ba (map_prod$a (fun_app$bb (case_sum$ id$a) uu$)) (fun_app$bb (case_sum$ id$a) uu$))) (id_bnf$ (id_bnf$ (pair$c (fun_app$ac ?v0 x$) (pair$b (inr$ (fun_app$v (comp$b ?v0) l$)) (inr$ (fun_app$v (comp$b ?v0) r$)))))))) (fun_app$bc dtor_tree$ (fun_app$d (map_tree$ ?v0) t$))) )))
(assert (forall ((?v0 A_tree$) (?v1 A_tree$)) (= (= (fun_app$bd dtor_tree$a ?v0) (fun_app$bd dtor_tree$a ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 B_tree$) (?v1 B_tree$)) (= (= (fun_app$bc dtor_tree$ ?v0) (fun_app$bc dtor_tree$ ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A_tree$)) (= (fun_app$x (map_tree$a ?v0) (fun_app$d (map_tree$ ?v1) ?v2)) (fun_app$d (map_tree$ (fun_app$u (comp$c ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 B_a_fun$) (?v1 A_b_fun$) (?v2 A_tree$)) (= (fun_app$be (map_tree$b ?v0) (fun_app$d (map_tree$ ?v1) ?v2)) (fun_app$bf (map_tree$c (fun_app$bg (comp$d ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_tree$)) (= (fun_app$d (map_tree$ ?v0) (fun_app$bf (map_tree$c ?v1) ?v2)) (fun_app$d (map_tree$ (fun_app$v (comp$b ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A_tree$)) (= (fun_app$bf (map_tree$c ?v0) (fun_app$bf (map_tree$c ?v1) ?v2)) (fun_app$bf (map_tree$c (fun_app$bh (comp$e ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_a_fun$) (?v2 B_tree$)) (= (fun_app$d (map_tree$ ?v0) (fun_app$be (map_tree$b ?v1) ?v2)) (fun_app$x (map_tree$a (fun_app$bi (comp$f ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_a_fun$) (?v1 B_a_fun$) (?v2 B_tree$)) (= (fun_app$bf (map_tree$c ?v0) (fun_app$be (map_tree$b ?v1) ?v2)) (fun_app$be (map_tree$b (fun_app$bj (comp$g ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 B_a_fun$) (?v1 B_b_fun$) (?v2 B_tree$)) (= (fun_app$be (map_tree$b ?v0) (fun_app$x (map_tree$a ?v1) ?v2)) (fun_app$be (map_tree$b (fun_app$bk (comp$h ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B_tree$)) (= (fun_app$x (map_tree$a ?v0) (fun_app$x (map_tree$a ?v1) ?v2)) (fun_app$x (map_tree$a (fun_app$t (comp$a ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_b_b_prod_fun$) (?v1 A_a_fun$) (?v2 A_tree$)) (= (fun_app$bl (map_tree$d ?v0) (fun_app$bf (map_tree$c ?v1) ?v2)) (fun_app$bl (map_tree$d (fun_app$bm (comp$i ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_sum_a_fun$) (?v2 A_a_sum_tree$)) (= (fun_app$d (map_tree$ ?v0) (fun_app$bn (map_tree$e ?v1) ?v2)) (fun_app$bo (map_tree$f (comp$j ?v0 ?v1)) ?v2)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$)) (= (map_tree$ (fun_app$u (comp$c ?v0) ?v1)) (fun_app$bp (comp$k (map_tree$a ?v0)) (map_tree$ ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$)) (= (map_tree$ (fun_app$v (comp$b ?v0) ?v1)) (fun_app$bq (comp$l (map_tree$ ?v0)) (map_tree$c ?v1))) ))
(assert (forall ((?v0 B_a_fun$) (?v1 A_b_fun$)) (= (map_tree$c (fun_app$bg (comp$d ?v0) ?v1)) (fun_app$br (comp$m (map_tree$b ?v0)) (map_tree$ ?v1))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$)) (= (map_tree$c (fun_app$bh (comp$e ?v0) ?v1)) (fun_app$bs (comp$n (map_tree$c ?v0)) (map_tree$c ?v1))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 B_a_fun$)) (= (map_tree$b (fun_app$bj (comp$g ?v0) ?v1)) (comp$o (map_tree$c ?v0) (map_tree$b ?v1))) ))
(assert (forall ((?v0 B_a_fun$) (?v1 B_b_fun$)) (= (map_tree$b (fun_app$bk (comp$h ?v0) ?v1)) (comp$p (map_tree$b ?v0) (map_tree$a ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_a_fun$)) (= (map_tree$a (fun_app$bi (comp$f ?v0) ?v1)) (fun_app$bt (comp$q (map_tree$ ?v0)) (map_tree$b ?v1))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$)) (= (map_tree$a (fun_app$t (comp$a ?v0) ?v1)) (fun_app$s (comp$ (map_tree$a ?v0)) (map_tree$a ?v1))) ))
(assert (forall ((?v0 A_b_b_prod_fun$) (?v1 A_a_fun$)) (= (map_tree$d (fun_app$bm (comp$i ?v0) ?v1)) (comp$r (map_tree$d ?v0) (map_tree$c ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_sum_a_fun$)) (= (map_tree$f (comp$j ?v0 ?v1)) (comp$s (map_tree$ ?v0) (map_tree$e ?v1))) ))
(assert (forall ((?v0 B_tree$)) (= (fun_app$x (map_tree$a uua$) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_tree$)) (= (fun_app$bu (map_tree$g uub$) ?v0) ?v0) ))
(assert (forall ((?v0 A_tree$)) (= (fun_app$bf (map_tree$c uuc$) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_sum_tree$)) (= (fun_app$bv (map_tree$h id$b) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_tree_fun_tree$)) (= (fun_app$bw (map_tree$i id$c) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_fun_tree$)) (= (fun_app$bx (map_tree$j id$d) ?v0) ?v0) ))
(assert (forall ((?v0 A_b_fun_tree$)) (= (fun_app$by (map_tree$k id$e) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree$)) (= (fun_app$x (map_tree$a id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_tree$)) (= (fun_app$bu (map_tree$g id$a) ?v0) ?v0) ))
(assert (forall ((?v0 A_tree$)) (= (fun_app$bf (map_tree$c id$f) ?v0) ?v0) ))
(assert (= (map_tree$h id$b) id$g))
(assert (= (map_tree$i id$c) id$h))
(assert (= (map_tree$j id$d) id$i))
(assert (= (map_tree$k id$e) id$j))
(assert (= (map_tree$a id$) id$a))
(assert (= (map_tree$g id$a) id$k))
(assert (= (map_tree$c id$f) id$l))
(assert (forall ((?v0 A_a_tree_a_tree_prod_prod$)) (=> (forall ((?v1 A_tree$)) (=> (= ?v0 (fun_app$bd dtor_tree$a ?v1)) false) ) false) ))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (=> (forall ((?v1 B_tree$)) (=> (= ?v0 (fun_app$bc dtor_tree$ ?v1)) false) ) false) ))
(assert (= t$ (node$a x$ (fun_app$bf (map_tree$c l$) t$) (fun_app$bf (map_tree$c r$) t$))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (! (= (fun_app$am (fun_app$ba (map_prod$a ?v0) ?v1) (pair$b ?v2 ?v3)) (pair$ (fun_app$w ?v0 ?v2) (fun_app$w ?v1 ?v3))) :pattern ((fun_app$am (fun_app$ba (map_prod$a ?v0) ?v1) (pair$b ?v2 ?v3))))))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$az (map_prod$ ?v0 ?v1) (pair$c ?v2 ?v3)) (pair$a (fun_app$aa ?v0 ?v2) (fun_app$am ?v1 ?v3))) :pattern ((fun_app$az (map_prod$ ?v0 ?v1) (pair$c ?v2 ?v3))))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (! (= (fun_app$ay (fun_app$bz (map_prod$b ?v0) ?v1) (pair$b ?v2 ?v3)) (pair$b (fun_app$ca ?v0 ?v2) (fun_app$ca ?v1 ?v3))) :pattern ((fun_app$ay (fun_app$bz (map_prod$b ?v0) ?v1) (pair$b ?v2 ?v3))))))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_fun$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (map_prod$c ?v0 ?v1 (pair$c ?v2 ?v3)) (pair$b (fun_app$cb ?v0 ?v2) (fun_app$f ?v1 ?v3))) :pattern ((map_prod$c ?v0 ?v1 (pair$c ?v2 ?v3))))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (! (= (map_prod$d ?v0 ?v1 (pair$b ?v2 ?v3)) (pair$c (fun_app$cc ?v0 ?v2) (fun_app$a ?v1 ?v3))) :pattern ((map_prod$d ?v0 ?v1 (pair$b ?v2 ?v3))))))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$cd (map_prod$e ?v0 ?v1) (pair$c ?v2 ?v3)) (pair$c (fun_app$aa ?v0 ?v2) (fun_app$ay ?v1 ?v3))) :pattern ((fun_app$cd (map_prod$e ?v0 ?v1) (pair$c ?v2 ?v3))))))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B$) (?v3 B$)) (! (= (fun_app$ce (map_prod$f ?v0 ?v1) (pair$f ?v2 ?v3)) (pair$f (fun_app$aa ?v0 ?v2) (fun_app$aa ?v1 ?v3))) :pattern ((fun_app$ce (map_prod$f ?v0 ?v1) (pair$f ?v2 ?v3))))))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A$) (?v3 A$)) (! (= (fun_app$cf (map_prod$g ?v0 ?v1) (pair$g ?v2 ?v3)) (pair$f (fun_app$ac ?v0 ?v2) (fun_app$ac ?v1 ?v3))) :pattern ((fun_app$cf (map_prod$g ?v0 ?v1) (pair$g ?v2 ?v3))))))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A$) (?v3 A$)) (! (= (fun_app$cg (map_prod$h ?v0 ?v1) (pair$g ?v2 ?v3)) (pair$g (fun_app$aw ?v0 ?v2) (fun_app$aw ?v1 ?v3))) :pattern ((fun_app$cg (map_prod$h ?v0 ?v1) (pair$g ?v2 ?v3))))))
(assert (forall ((?v0 A_tree_b_fun$) (?v1 A_tree_b_fun$) (?v2 A_tree$) (?v3 A_tree$)) (! (= (map_prod$i ?v0 ?v1 (pair$d ?v2 ?v3)) (pair$f (fun_app$ch ?v0 ?v2) (fun_app$ch ?v1 ?v3))) :pattern ((map_prod$i ?v0 ?v1 (pair$d ?v2 ?v3))))))
(assert (forall ((?v0 A_b_b_prod_fun$)) (= (fun_app$bm (comp$i ?v0) id$f) ?v0) ))
(assert (forall ((?v0 A_a_fun$)) (= (fun_app$bh (comp$e ?v0) id$f) ?v0) ))
(assert (forall ((?v0 A_b_fun$)) (= (fun_app$v (comp$b ?v0) id$f) ?v0) ))
(assert (forall ((?v0 A_b_fun$)) (= (fun_app$u (comp$c id$) ?v0) ?v0) ))
(assert (forall ((?v0 A_a_fun$)) (= (fun_app$bh (comp$e id$f) ?v0) ?v0) ))
(assert (forall ((?v0 A_b_fun$)) (= (fun_app$u (comp$c id$) ?v0) ?v0) ))
(assert (forall ((?v0 A_a_fun$)) (= (fun_app$bh (comp$e id$f) ?v0) ?v0) ))
(assert (forall ((?v0 B$) (?v1 B_b_sum$)) (= (fun_app$ci (case_sum$a (uud$ ?v0) (uud$ ?v0)) ?v1) ?v0) ))
(assert (forall ((?v0 B$) (?v1 A_b_tree_sum$)) (= (case_sum$b (uue$ ?v0) (uuf$ ?v0) ?v1) ?v0) ))
(assert (forall ((?v0 B$) (?v1 A_b_sum$)) (= (case_sum$c (uue$ ?v0) (uud$ ?v0) ?v1) ?v0) ))
(assert (forall ((?v0 B$) (?v1 A_a_sum$)) (= (fun_app$cj (case_sum$d (uue$ ?v0) (uue$ ?v0)) ?v1) ?v0) ))
(assert (forall ((?v0 A$) (?v1 A_a_sum$)) (= (fun_app$ck (fun_app$cl (case_sum$e (uug$ ?v0)) (uug$ ?v0)) ?v1) ?v0) ))
(assert (forall ((?v0 B_tree$) (?v1 B_tree_a_b_fun_sum$)) (= (fun_app$w (fun_app$bb (case_sum$ (uuh$ ?v0)) (uui$ ?v0)) ?v1) ?v0) ))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (= (fun_app$cm (map_prod$j uua$ uuj$) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (fun_app$cd (map_prod$e uua$ uuk$) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_prod$)) (= (fun_app$ce (map_prod$f uua$ uua$) ?v0) ?v0) ))
(assert (forall ((?v0 A_a_prod$)) (= (fun_app$cg (map_prod$h uuc$ uuc$) ?v0) ?v0) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$)) (= (= (inr$ ?v0) (inr$ ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$)) (= (= (inr$ ?v0) (inr$ ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 B_b_sum$)) (! (= (fun_app$cn id$b ?v0) ?v0) :pattern ((fun_app$cn id$b ?v0)))))
(assert (forall ((?v0 B_tree_b_tree_fun$)) (! (= (fun_app$s id$c ?v0) ?v0) :pattern ((fun_app$s id$c ?v0)))))
(assert (forall ((?v0 B_b_fun$)) (! (= (fun_app$t id$d ?v0) ?v0) :pattern ((fun_app$t id$d ?v0)))))
(assert (forall ((?v0 A_b_fun$)) (! (= (fun_app$u id$e ?v0) ?v0) :pattern ((fun_app$u id$e ?v0)))))
(assert (forall ((?v0 A$)) (! (= (fun_app$aw id$f ?v0) ?v0) :pattern ((fun_app$aw id$f ?v0)))))
(assert (forall ((?v0 B$)) (! (= (fun_app$aa id$ ?v0) ?v0) :pattern ((fun_app$aa id$ ?v0)))))
(assert (forall ((?v0 B_tree$)) (! (= (fun_app$x id$a ?v0) ?v0) :pattern ((fun_app$x id$a ?v0)))))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A$)) (! (= (fun_app$ac (fun_app$u (comp$c ?v0) ?v1) ?v2) (fun_app$aa ?v0 (fun_app$ac ?v1 ?v2))) :pattern ((fun_app$ac (fun_app$u (comp$c ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 B_a_fun$) (?v1 A_b_fun$) (?v2 A$)) (! (= (fun_app$aw (fun_app$bg (comp$d ?v0) ?v1) ?v2) (fun_app$co ?v0 (fun_app$ac ?v1 ?v2))) :pattern ((fun_app$aw (fun_app$bg (comp$d ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 A_b_b_prod_fun$) (?v1 A_a_fun$) (?v2 A$)) (! (= (fun_app$cp (fun_app$bm (comp$i ?v0) ?v1) ?v2) (fun_app$cp ?v0 (fun_app$aw ?v1 ?v2))) :pattern ((fun_app$cp (fun_app$bm (comp$i ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_sum_a_fun$) (?v2 A_a_sum$)) (! (= (fun_app$cj (comp$j ?v0 ?v1) ?v2) (fun_app$ac ?v0 (fun_app$ck ?v1 ?v2))) :pattern ((fun_app$cj (comp$j ?v0 ?v1) ?v2)))))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A$)) (! (= (fun_app$aw (fun_app$bh (comp$e ?v0) ?v1) ?v2) (fun_app$aw ?v0 (fun_app$aw ?v1 ?v2))) :pattern ((fun_app$aw (fun_app$bh (comp$e ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A$)) (! (= (fun_app$ac (fun_app$v (comp$b ?v0) ?v1) ?v2) (fun_app$ac ?v0 (fun_app$aw ?v1 ?v2))) :pattern ((fun_app$ac (fun_app$v (comp$b ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 A_tree$) (?v1 A_tree$) (?v2 A_tree$) (?v3 A_tree$)) (= (= (pair$d ?v0 ?v1) (pair$d ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v3 B$)) (= (= (pair$h ?v0 ?v1) (pair$h ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B_tree_b_tree_prod$) (?v2 B$) (?v3 B_tree_b_tree_prod$)) (= (= (pair$a ?v0 ?v1) (pair$a ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B$) (?v2 B$) (?v3 B$)) (= (= (pair$f ?v0 ?v1) (pair$f ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 A$) (?v1 A_tree_a_tree_prod$) (?v2 A$) (?v3 A_tree_a_tree_prod$)) (= (= (pair$e ?v0 ?v1) (pair$e ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (= (pair$c ?v0 ?v1) (pair$c ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (= (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 A_tree$) (?v1 A_tree$) (?v2 A_tree$) (?v3 A_tree$)) (= (= (pair$d ?v0 ?v1) (pair$d ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v3 B$)) (= (= (pair$h ?v0 ?v1) (pair$h ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B_tree_b_tree_prod$) (?v2 B$) (?v3 B_tree_b_tree_prod$)) (= (= (pair$a ?v0 ?v1) (pair$a ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B$) (?v2 B$) (?v3 B$)) (= (= (pair$f ?v0 ?v1) (pair$f ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 A$) (?v1 A_tree_a_tree_prod$) (?v2 A$) (?v3 A_tree_a_tree_prod$)) (= (= (pair$e ?v0 ?v1) (pair$e ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (= (pair$c ?v0 ?v1) (pair$c ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (= (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 B$) (?v1 B_tree$) (?v2 B_tree$) (?v3 B$) (?v4 B_tree$) (?v5 B_tree$)) (= (= (node$ ?v0 ?v1 ?v2) (node$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ))
(assert (forall ((?v0 A$) (?v1 A_tree$) (?v2 A_tree$) (?v3 A$) (?v4 A_tree$) (?v5 A_tree$)) (= (= (node$a ?v0 ?v1 ?v2) (node$a ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ))
(assert (forall ((?v0 B_tree$)) (=> (forall ((?v1 B$) (?v2 B_tree$) (?v3 B_tree$)) (=> (= ?v0 (node$ ?v1 ?v2 ?v3)) false) ) false) ))
(assert (forall ((?v0 A_tree$)) (=> (forall ((?v1 A$) (?v2 A_tree$) (?v3 A_tree$)) (=> (= ?v0 (node$a ?v1 ?v2 ?v3)) false) ) false) ))
(assert (= (map_prod$j uua$ uuj$) id$m))
(assert (= (map_prod$e uua$ uuk$) id$n))
(assert (= (map_prod$f uua$ uua$) id$o))
(assert (= (map_prod$h uuc$ uuc$) id$p))
(assert (forall ((?v0 B_a_fun$) (?v1 B$) (?v2 B_tree$) (?v3 B_tree$)) (! (= (fun_app$be (map_tree$b ?v0) (node$ ?v1 ?v2 ?v3)) (node$a (fun_app$co ?v0 ?v1) (fun_app$be (map_tree$b ?v0) ?v2) (fun_app$be (map_tree$b ?v0) ?v3))) :pattern ((fun_app$be (map_tree$b ?v0) (node$ ?v1 ?v2 ?v3))))))
(assert (forall ((?v0 B_b_fun$) (?v1 B$) (?v2 B_tree$) (?v3 B_tree$)) (! (= (fun_app$x (map_tree$a ?v0) (node$ ?v1 ?v2 ?v3)) (node$ (fun_app$aa ?v0 ?v1) (fun_app$x (map_tree$a ?v0) ?v2) (fun_app$x (map_tree$a ?v0) ?v3))) :pattern ((fun_app$x (map_tree$a ?v0) (node$ ?v1 ?v2 ?v3))))))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree$) (?v2 B_tree_tree$) (?v3 B_tree_tree$)) (! (= (fun_app$bu (map_tree$g ?v0) (node$d ?v1 ?v2 ?v3)) (node$d (fun_app$x ?v0 ?v1) (fun_app$bu (map_tree$g ?v0) ?v2) (fun_app$bu (map_tree$g ?v0) ?v3))) :pattern ((fun_app$bu (map_tree$g ?v0) (node$d ?v1 ?v2 ?v3))))))
(assert (forall ((?v0 A_b_fun$) (?v1 A$) (?v2 A_tree$) (?v3 A_tree$)) (! (= (fun_app$d (map_tree$ ?v0) (node$a ?v1 ?v2 ?v3)) (node$ (fun_app$ac ?v0 ?v1) (fun_app$d (map_tree$ ?v0) ?v2) (fun_app$d (map_tree$ ?v0) ?v3))) :pattern ((fun_app$d (map_tree$ ?v0) (node$a ?v1 ?v2 ?v3))))))
(assert (forall ((?v0 A_a_fun$) (?v1 A$) (?v2 A_tree$) (?v3 A_tree$)) (! (= (fun_app$bf (map_tree$c ?v0) (node$a ?v1 ?v2 ?v3)) (node$a (fun_app$aw ?v0 ?v1) (fun_app$bf (map_tree$c ?v0) ?v2) (fun_app$bf (map_tree$c ?v0) ?v3))) :pattern ((fun_app$bf (map_tree$c ?v0) (node$a ?v1 ?v2 ?v3))))))
(assert (forall ((?v0 B_b_prod$)) (exists ((?v1 B$) (?v2 B$)) (= ?v0 (pair$f ?v1 ?v2)) ) ))
(assert (forall ((?v0 A_a_tree_a_tree_prod_prod$)) (exists ((?v1 A$) (?v2 A_tree_a_tree_prod$)) (= ?v0 (pair$e ?v1 ?v2)) ) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (exists ((?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= ?v0 (pair$c ?v1 ?v2)) ) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (exists ((?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (= ?v0 (pair$b ?v1 ?v2)) ) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (and (= (pair$c ?v0 ?v1) (pair$c ?v2 ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (=> (and (= (pair$b ?v0 ?v1) (pair$b ?v2 ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_bool_fun$) (?v1 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (=> (forall ((?v2 B$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (fun_app$cq ?v0 (pair$c ?v2 ?v3)) ) (fun_app$cq ?v0 ?v1)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (forall ((?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (fun_app$af ?v0 (pair$b ?v2 ?v3)) ) (fun_app$af ?v0 ?v1)) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (=> (forall ((?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (= ?v0 (pair$c ?v1 ?v2)) false) ) false) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (forall ((?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (=> (= ?v0 (pair$b ?v1 ?v2)) false) ) false) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A$)) (=> (= (fun_app$v (comp$b ?v0) ?v1) ?v2) (= (fun_app$ac ?v0 (fun_app$aw ?v1 ?v3)) (fun_app$ac ?v2 ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$) (?v4 A$)) (=> (= (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (= (fun_app$ac ?v0 (fun_app$aw ?v1 ?v4)) (fun_app$ac ?v2 (fun_app$aw ?v3 ?v4)))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$)) (=> (and (= (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (=> (forall ((?v4 A$)) (= (fun_app$ac ?v0 (fun_app$aw ?v1 ?v4)) (fun_app$ac ?v2 (fun_app$aw ?v3 ?v4))) ) false)) false) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A$)) (! (= (fun_app$ac (fun_app$v (comp$b ?v0) ?v1) ?v2) (fun_app$ac ?v0 (fun_app$aw ?v1 ?v2))) :pattern ((fun_app$ac (fun_app$v (comp$b ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$)) (= (fun_app$v (comp$b (fun_app$u (comp$c ?v0) ?v1)) ?v2) (fun_app$u (comp$c ?v0) (fun_app$v (comp$b ?v1) ?v2))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_a_fun$)) (= (fun_app$v (comp$b (fun_app$v (comp$b ?v0) ?v1)) ?v2) (fun_app$v (comp$b ?v0) (fun_app$bh (comp$e ?v1) ?v2))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$)) (= (fun_app$u (comp$c ?v0) (fun_app$v (comp$b ?v1) ?v2)) (fun_app$v (comp$b (fun_app$u (comp$c ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_a_fun$)) (= (fun_app$v (comp$b ?v0) (fun_app$bh (comp$e ?v1) ?v2)) (fun_app$v (comp$b (fun_app$v (comp$b ?v0) ?v1)) ?v2)) ))
(assert (forall ((?v0 B$)) (! (= (fun_app$aa id$ ?v0) ?v0) :pattern ((fun_app$aa id$ ?v0)))))
(assert (forall ((?v0 B_tree$)) (! (= (fun_app$x id$a ?v0) ?v0) :pattern ((fun_app$x id$a ?v0)))))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$)) (=> (= (inr$ ?v0) (inr$ ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 B_tree_b_tree_fun$) (?v3 A_b_fun_b_tree_fun$)) (=> (and (= (fun_app$bb (case_sum$ ?v0) ?v1) (fun_app$bb (case_sum$ ?v2) ?v3)) (=> (and (= ?v0 ?v2) (= ?v1 ?v3)) false)) false) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 A_b_fun_b_tree_fun$) (?v3 B_tree_a_b_fun_sum$)) (= (fun_app$x ?v0 (fun_app$w (fun_app$bb (case_sum$ ?v1) ?v2) ?v3)) (fun_app$w (fun_app$bb (case_sum$ (fun_app$s (uul$ ?v0) ?v1)) (fun_app$ah (uum$ ?v0) ?v2)) ?v3)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A$)) (=> (= (fun_app$v (comp$b ?v0) ?v1) (fun_app$u (comp$c id$) ?v2)) (= (fun_app$ac ?v0 (fun_app$aw ?v1 ?v3)) (fun_app$ac ?v2 ?v3))) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (=> (forall ((?v1 B$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum$)) (=> (= ?v0 (pair$c ?v1 (pair$b ?v2 ?v3))) false) ) false) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_bool_fun$) (?v1 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (=> (forall ((?v2 B$) (?v3 B_tree_a_b_fun_sum$) (?v4 B_tree_a_b_fun_sum$)) (fun_app$cq ?v0 (pair$c ?v2 (pair$b ?v3 ?v4))) ) (fun_app$cq ?v0 ?v1)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$)) (= (comp$t (map_prod$g ?v0 ?v1) (map_prod$h ?v2 ?v3)) (map_prod$g (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_b_tree_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)) (= (comp$u (map_prod$j ?v0 ?v1) (map_prod$ ?v2 ?v3)) (map_prod$ (fun_app$t (comp$a ?v0) ?v2) (fun_app$cr (comp$v ?v1) ?v3))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_fun$)) (= (fun_app$cr (comp$v (fun_app$cs (map_prod$k ?v0) ?v1)) (fun_app$ba (map_prod$a ?v2) ?v3)) (fun_app$ba (map_prod$a (fun_app$ct (comp$w ?v0) ?v2)) (fun_app$ct (comp$w ?v1) ?v3))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)) (= (comp$x (map_prod$ ?v0 ?v1) (map_prod$e ?v2 ?v3)) (map_prod$ (fun_app$t (comp$a ?v0) ?v2) (fun_app$cu (comp$y ?v1) ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$)) (= (fun_app$cu (comp$y (fun_app$ba (map_prod$a ?v0) ?v1)) (fun_app$bz (map_prod$b ?v2) ?v3)) (fun_app$ba (map_prod$a (fun_app$cv (comp$z ?v0) ?v2)) (fun_app$cv (comp$z ?v1) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$)) (= (map_prod$g (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (comp$t (map_prod$g ?v0 ?v2) (map_prod$h ?v1 ?v3))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B_tree_b_tree_prod_b_tree_b_tree_prod_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)) (= (map_prod$ (fun_app$t (comp$a ?v0) ?v1) (fun_app$cr (comp$v ?v2) ?v3)) (comp$u (map_prod$j ?v0 ?v2) (map_prod$ ?v1 ?v3))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$)) (= (map_prod$ (fun_app$t (comp$a ?v0) ?v1) (fun_app$cu (comp$y ?v2) ?v3)) (comp$x (map_prod$ ?v0 ?v2) (map_prod$e ?v1 ?v3))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_b_tree_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_fun$)) (= (fun_app$ba (map_prod$a (fun_app$ct (comp$w ?v0) ?v1)) (fun_app$ct (comp$w ?v2) ?v3)) (fun_app$cr (comp$v (fun_app$cs (map_prod$k ?v0) ?v2)) (fun_app$ba (map_prod$a ?v1) ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$)) (= (fun_app$ba (map_prod$a (fun_app$cv (comp$z ?v0) ?v1)) (fun_app$cv (comp$z ?v2) ?v3)) (fun_app$cu (comp$y (fun_app$ba (map_prod$a ?v0) ?v2)) (fun_app$bz (map_prod$b ?v1) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_a_prod$)) (= (fun_app$cf (map_prod$g ?v0 ?v1) (fun_app$cg (map_prod$h ?v2 ?v3) ?v4)) (fun_app$cf (map_prod$g (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_b_tree_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v4 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (fun_app$cm (map_prod$j ?v0 ?v1) (fun_app$az (map_prod$ ?v2 ?v3) ?v4)) (fun_app$az (map_prod$ (fun_app$t (comp$a ?v0) ?v2) (fun_app$cr (comp$v ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_fun$) (?v4 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (fun_app$ax (fun_app$cs (map_prod$k ?v0) ?v1) (fun_app$am (fun_app$ba (map_prod$a ?v2) ?v3) ?v4)) (fun_app$am (fun_app$ba (map_prod$a (fun_app$ct (comp$w ?v0) ?v2)) (fun_app$ct (comp$w ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) (?v4 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (fun_app$az (map_prod$ ?v0 ?v1) (fun_app$cd (map_prod$e ?v2 ?v3) ?v4)) (fun_app$az (map_prod$ (fun_app$t (comp$a ?v0) ?v2) (fun_app$cu (comp$y ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v4 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (fun_app$am (fun_app$ba (map_prod$a ?v0) ?v1) (fun_app$ay (fun_app$bz (map_prod$b ?v2) ?v3) ?v4)) (fun_app$am (fun_app$ba (map_prod$a (fun_app$cv (comp$z ?v0) ?v2)) (fun_app$cv (comp$z ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_a_prod$)) (= (fun_app$cf (map_prod$g ?v0 ?v1) (fun_app$cg (map_prod$h ?v2 ?v3) ?v4)) (fun_app$cf (map_prod$g (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_b_tree_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v4 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (fun_app$cm (map_prod$j ?v0 ?v1) (fun_app$az (map_prod$ ?v2 ?v3) ?v4)) (fun_app$az (map_prod$ (fun_app$t (comp$a ?v0) ?v2) (fun_app$cr (comp$v ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_fun$) (?v4 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (fun_app$ax (fun_app$cs (map_prod$k ?v0) ?v1) (fun_app$am (fun_app$ba (map_prod$a ?v2) ?v3) ?v4)) (fun_app$am (fun_app$ba (map_prod$a (fun_app$ct (comp$w ?v0) ?v2)) (fun_app$ct (comp$w ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) (?v4 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (fun_app$az (map_prod$ ?v0 ?v1) (fun_app$cd (map_prod$e ?v2 ?v3) ?v4)) (fun_app$az (map_prod$ (fun_app$t (comp$a ?v0) ?v2) (fun_app$cu (comp$y ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v4 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (fun_app$am (fun_app$ba (map_prod$a ?v0) ?v1) (fun_app$ay (fun_app$bz (map_prod$b ?v2) ?v3) ?v4)) (fun_app$am (fun_app$ba (map_prod$a (fun_app$cv (comp$z ?v0) ?v2)) (fun_app$cv (comp$z ?v1) ?v3)) ?v4)) ))
(assert (= (map_prod$f id$ id$) id$o))
(assert (= (map_prod$l id$ id$a) id$q))
(assert (= (map_prod$m id$a id$) id$r))
(assert (= (fun_app$cs (map_prod$k id$a) id$a) id$s))
(assert (forall ((?v0 B_b_prod$)) (= (fun_app$ce (map_prod$f id$ id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_tree_prod$)) (= (fun_app$cw (map_prod$l id$ id$a) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_prod$)) (= (fun_app$cx (map_prod$m id$a id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_tree_prod$)) (= (fun_app$ax (fun_app$cs (map_prod$k id$a) id$a) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 A_b_fun$)) (! (= (fun_app$w (fun_app$bb (case_sum$ ?v0) ?v1) (inr$ ?v2)) (fun_app$c ?v1 ?v2)) :pattern ((fun_app$w (fun_app$bb (case_sum$ ?v0) ?v1) (inr$ ?v2))))))
(assert (forall ((?v0 B$) (?v1 B_tree$) (?v2 B_tree$)) (! (= (node$ ?v0 ?v1 ?v2) (ctor_tree$ (id_bnf$a (pair$a ?v0 (pair$ ?v1 ?v2))))) :pattern ((node$ ?v0 ?v1 ?v2)))))
(assert (forall ((?v0 A$) (?v1 A_tree$) (?v2 A_tree$)) (! (= (node$a ?v0 ?v1 ?v2) (ctor_tree$a (id_bnf$b (pair$e ?v0 (pair$d ?v1 ?v2))))) :pattern ((node$a ?v0 ?v1 ?v2)))))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$)) (= (fun_app$cy (comp$aa (fun_app$bb (case_sum$ ?v0) ?v1)) uun$) ?v1) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_a_fun$)) (= (comp$j ?v0 (fun_app$cl (case_sum$e ?v1) ?v2)) (case_sum$d (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v0) ?v2))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 A_b_fun_b_tree_fun$)) (= (fun_app$ct (comp$w ?v0) (fun_app$bb (case_sum$ ?v1) ?v2)) (fun_app$bb (case_sum$ (fun_app$s (comp$ ?v0) ?v1)) (fun_app$ah (comp$ab ?v0) ?v2))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_bool_fun$) (?v3 A_a_tree_fun$) (?v4 A_a_fun$) (?v5 A_bool_fun$) (?v6 A_a_tree_fun$) (?v7 A_a_fun$)) (= (comp$ac (map_tree$ ?v0) (fun_app$cz (fun_app$da (fun_app$db (fun_app$dc (fun_app$dd (fun_app$de (corec_tree$ ?v1) ?v2) ?v3) ?v4) ?v5) ?v6) ?v7)) (corec_tree$a (fun_app$v (comp$b ?v0) ?v1) ?v2 (comp$ac (map_tree$ ?v0) ?v3) ?v4 ?v5 (comp$ac (map_tree$ ?v0) ?v6) ?v7)) ))
(assert (forall ((?v0 B_tree_bool_fun$) (?v1 A_b_fun_bool_fun$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_bool_fun$) (?v4 B_tree_b_tree_fun$) (?v5 A_b_fun_b_tree_fun$)) (=> (and (fun_app$ad (fun_app$df (case_sum$f ?v0) ?v1) ?v2) (and (forall ((?v6 B_tree$)) (=> (fun_app$dg ?v0 ?v6) (fun_app$dg ?v3 (fun_app$x ?v4 ?v6))) ) (forall ((?v6 A_b_fun$)) (=> (fun_app$au ?v1 ?v6) (fun_app$dg ?v3 (fun_app$c ?v5 ?v6))) ))) (fun_app$dg ?v3 (fun_app$w (fun_app$bb (case_sum$ ?v4) ?v5) ?v2))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_b_fun$)) (= (fun_app$x (map_tree$a ?v0) (fun_app$c (fun_app$dh (fun_app$di (unfold_tree$ (uuo$ ?v1)) (uup$ ?v2)) (uup$ ?v3)) ?v4)) (fun_app$c (fun_app$dh (fun_app$di (unfold_tree$ (uuo$ ?v1)) (uup$ ?v2)) (uup$ ?v3)) (fun_app$u (comp$c ?v0) ?v4))) ))
(assert (forall ((?v0 A_b_fun_b_fun$) (?v1 A_b_fun_bool_fun$) (?v2 A_b_fun_b_tree_fun$) (?v3 A_b_fun_a_b_fun_fun$) (?v4 A_b_fun_bool_fun$) (?v5 A_b_fun_b_tree_fun$) (?v6 A_b_fun_a_b_fun_fun$)) (= (fun_app$dh (fun_app$dj (fun_app$dk (fun_app$dl (fun_app$dm (fun_app$dn (corec_tree$b ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) ?v6) (dtor_corec_tree$ (fun_app$ao (fun_app$ap (fun_app$aq (fun_app$ar (fun_app$as (fun_app$at (uuq$ ?v0) ?v1) ?v2) ?v3) ?v4) ?v5) ?v6))) ))
(assert (forall ((?v0 B_tree$) (?v1 A_b_fun$)) (= (= (inl$ ?v0) (inr$ ?v1)) false) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_tree$)) (= (= (inr$ ?v0) (inl$ ?v1)) false) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$)) (= (fun_app$do (comp$ad (fun_app$bb (case_sum$ ?v0) ?v1)) uur$) ?v0) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_bool_fun$)) (= (exists ((?v1 B_tree_a_b_fun_sum$)) (fun_app$ad ?v0 ?v1) ) (or (exists ((?v1 B_tree$)) (fun_app$ad ?v0 (inl$ ?v1)) ) (exists ((?v1 A_b_fun$)) (fun_app$ad ?v0 (inr$ ?v1)) ))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_bool_fun$)) (= (forall ((?v1 B_tree_a_b_fun_sum$)) (fun_app$ad ?v0 ?v1) ) (and (forall ((?v1 B_tree$)) (fun_app$ad ?v0 (inl$ ?v1)) ) (forall ((?v1 A_b_fun$)) (fun_app$ad ?v0 (inr$ ?v1)) ))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$)) (=> (and (forall ((?v1 B_tree$)) (=> (= ?v0 (inl$ ?v1)) false) ) (forall ((?v1 A_b_fun$)) (=> (= ?v0 (inr$ ?v1)) false) )) false) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$)) (=> (and (forall ((?v1 B_tree$)) (=> (= ?v0 (inl$ ?v1)) false) ) (forall ((?v1 A_b_fun$)) (=> (= ?v0 (inr$ ?v1)) false) )) false) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_tree$)) (not (= (inr$ ?v0) (inl$ ?v1))) ))
(assert (forall ((?v0 B_tree$) (?v1 A_b_fun$)) (not (= (inl$ ?v0) (inr$ ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_tree$)) (not (= (inr$ ?v0) (inl$ ?v1))) ))
(assert (forall ((?v0 B_tree$) (?v1 A_b_fun$)) (not (= (inl$ ?v0) (inr$ ?v1))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 B_tree$)) (! (= (fun_app$w (fun_app$bb (case_sum$ ?v0) ?v1) (inl$ ?v2)) (fun_app$x ?v0 ?v2)) :pattern ((fun_app$w (fun_app$bb (case_sum$ ?v0) ?v1) (inl$ ?v2))))))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 Bool) (?v3 B_tree$) (?v4 A_b_fun$)) (= (fun_app$w (fun_app$bb (case_sum$ ?v0) ?v1) (ite ?v2 (inl$ ?v3) (inr$ ?v4))) (ite ?v2 (fun_app$x ?v0 ?v3) (fun_app$c ?v1 ?v4))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$)) (= (fun_app$bb (case_sum$ (uus$ ?v0)) (uut$ ?v0)) ?v0) ))
(assert (forall ((?v0 B_tree$)) (= (ctor_tree$ (fun_app$bc dtor_tree$ ?v0)) ?v0) ))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (= (fun_app$bc dtor_tree$ (ctor_tree$ ?v0)) ?v0) ))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_b_fun$) (?v5 A_b_fun$)) (=> (and (= (fun_app$bh (comp$e ?v0) ?v1) (fun_app$bh (comp$e ?v2) ?v3)) (= (fun_app$v (comp$b ?v4) ?v2) ?v5)) (= (fun_app$v (comp$b (fun_app$v (comp$b ?v4) ?v0)) ?v1) (fun_app$v (comp$b ?v5) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$) (?v4 B_b_fun$) (?v5 A_b_fun$)) (=> (and (= (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (= (fun_app$u (comp$c ?v4) ?v2) ?v5)) (= (fun_app$v (comp$b (fun_app$u (comp$c ?v4) ?v0)) ?v1) (fun_app$v (comp$b ?v5) ?v3))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$) (?v4 A_a_fun$) (?v5 A_a_fun$)) (=> (and (= (fun_app$u (comp$c ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (= (fun_app$bh (comp$e ?v3) ?v4) ?v5)) (= (fun_app$u (comp$c ?v0) (fun_app$v (comp$b ?v1) ?v4)) (fun_app$v (comp$b ?v2) ?v5))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 B_b_fun$) (?v3 A_b_fun$) (?v4 A_a_fun$) (?v5 A_b_fun$)) (=> (and (= (fun_app$v (comp$b ?v0) ?v1) (fun_app$u (comp$c ?v2) ?v3)) (= (fun_app$v (comp$b ?v3) ?v4) ?v5)) (= (fun_app$v (comp$b ?v0) (fun_app$bh (comp$e ?v1) ?v4)) (fun_app$u (comp$c ?v2) ?v5))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$) (?v4 A_a_fun$) (?v5 A_a_fun$)) (=> (and (= (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (= (fun_app$bh (comp$e ?v3) ?v4) ?v5)) (= (fun_app$v (comp$b ?v0) (fun_app$bh (comp$e ?v1) ?v4)) (fun_app$v (comp$b ?v2) ?v5))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A_a_fun$) (?v3 A_b_fun$)) (=> (= (fun_app$bh (comp$e ?v0) ?v1) ?v2) (= (fun_app$v (comp$b (fun_app$v (comp$b ?v3) ?v0)) ?v1) (fun_app$v (comp$b ?v3) ?v2))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 B_b_fun$)) (=> (= (fun_app$v (comp$b ?v0) ?v1) ?v2) (= (fun_app$v (comp$b (fun_app$u (comp$c ?v3) ?v0)) ?v1) (fun_app$u (comp$c ?v3) ?v2))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$)) (=> (= (fun_app$u (comp$c ?v0) ?v1) ?v2) (= (fun_app$u (comp$c ?v0) (fun_app$v (comp$b ?v1) ?v3)) (fun_app$v (comp$b ?v2) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$)) (=> (= (fun_app$v (comp$b ?v0) ?v1) ?v2) (= (fun_app$v (comp$b ?v0) (fun_app$bh (comp$e ?v1) ?v3)) (fun_app$v (comp$b ?v2) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A$) (?v3 A_b_fun$) (?v4 A_a_fun$)) (=> (= (fun_app$ac ?v0 (fun_app$aw ?v1 ?v2)) (fun_app$ac ?v3 (fun_app$aw ?v4 ?v2))) (= (fun_app$ac (fun_app$v (comp$b ?v0) ?v1) ?v2) (fun_app$ac (fun_app$v (comp$b ?v3) ?v4) ?v2))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A$)) (= (fun_app$d (map_tree$ ?v0) (fun_app$dp (fun_app$cz (fun_app$dq (unfold_tree$a ?v1) ?v2) ?v3) ?v4)) (unfold_tree$b (fun_app$v (comp$b ?v0) ?v1) ?v2 ?v3 ?v4)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 A_b_fun_b_tree_fun$)) (=> (= (fun_app$do (comp$ad ?v0) uur$) ?v1) (= (= ?v2 (fun_app$cy (comp$aa ?v0) uun$)) (= (fun_app$bb (case_sum$ ?v1) ?v2) ?v0))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree_a_b_fun_sum$)) (=> (= (fun_app$do (comp$ad ?v0) uur$) ?v1) (= (fun_app$w ?v0 ?v2) (fun_app$w (fun_app$bb (case_sum$ ?v1) (fun_app$cy (comp$aa ?v0) uun$)) ?v2))) ))
(assert (forall ((?v0 A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$) (?v1 A_b_fun$)) (= (fun_app$bc dtor_tree$ (fun_app$c (dtor_corec_tree$ ?v0) ?v1)) (fun_app$az (map_pre_tree$ id$ (fun_app$bb (case_sum$ id$a) (dtor_corec_tree$ ?v0))) (fun_app$an ?v0 ?v1))) ))
(assert (forall ((?v0 A_b_fun_b_tree_fun$) (?v1 A_b_fun_b_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_fun$)) (=> (= (comp$ae (map_pre_tree$ id$ (fun_app$bb (case_sum$ id$a) ?v0)) ?v1) (comp$af dtor_tree$ ?v0)) (= ?v0 (dtor_corec_tree$ ?v1))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$)) (=> (and (forall ((?v1 B_tree$)) (=> (= ?v0 (inl$ ?v1)) false) ) (forall ((?v1 A_b_fun$)) (=> (= ?v0 (inr$ ?v1)) false) )) false) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B$)) (= (swap$ (pair$h ?v0 ?v1)) (pair$c ?v1 ?v0)) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (swap$a (pair$c ?v0 ?v1)) (pair$h ?v1 ?v0)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$)) (= (swap$b (pair$b ?v0 ?v1)) (pair$b ?v1 ?v0)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$) (?v2 A_b_fun$) (?v3 A_a_fun$)) (= (map_pre_tree$a (fun_app$v (comp$b ?v0) ?v1) (fun_app$v (comp$b ?v2) ?v3)) (comp$ag (map_pre_tree$a ?v0 ?v2) (map_pre_tree$b ?v1 ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_a_a_prod_prod$)) (= (fun_app$dr (map_pre_tree$a ?v0 ?v1) (fun_app$ds (map_pre_tree$b ?v2 ?v3) ?v4)) (fun_app$dr (map_pre_tree$a (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3)) ?v4)) ))
(assert (= (map_pre_tree$c id$ id$) id$t))
(assert (= (map_pre_tree$d id$ id$a) id$m))
(assert (= (map_pre_tree$e id$a id$) id$u))
(assert (= (map_pre_tree$f id$a id$a) id$v))
(assert (forall ((?v0 B_b_b_prod_prod$)) (= (fun_app$dt (map_pre_tree$c id$ id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (= (fun_app$cm (map_pre_tree$d id$ id$a) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_b_prod_prod$)) (= (fun_app$du (map_pre_tree$e id$a id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_tree_b_tree_prod_prod$)) (= (fun_app$dv (map_pre_tree$f id$a id$a) ?v0) ?v0) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$)) (=> (not (= ?v0 ?v1)) (not (= (inr$ ?v0) (inr$ ?v1)))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_a_b_b_prod_prod_fun$)) (= (fun_app$dw (comp$ah (map_tree$ ?v0)) (dtor_unfold_tree$ ?v1)) (dtor_unfold_tree$a (comp$ai (map_pre_tree$g ?v0 id$) ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_tree_a_b_tree_b_tree_prod_prod_fun$)) (= (fun_app$bt (comp$q (map_tree$ ?v0)) (dtor_unfold_tree$b ?v1)) (dtor_unfold_tree$c (comp$aj (map_pre_tree$h ?v0 id$a) ?v1))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 B_a_b_b_prod_prod_fun$)) (= (comp$ak (map_tree$c ?v0) (dtor_unfold_tree$ ?v1)) (dtor_unfold_tree$ (fun_app$dx (comp$al (map_pre_tree$i ?v0 id$)) ?v1))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 B_tree_a_b_tree_b_tree_prod_prod_fun$)) (= (comp$o (map_tree$c ?v0) (dtor_unfold_tree$b ?v1)) (dtor_unfold_tree$b (fun_app$dy (comp$am (map_pre_tree$j ?v0 id$a)) ?v1))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B$)) (= (fun_app$dz (fun_app$ea (tree_recurse$ ?v0) ?v1) ?v2) (unfold_tree$c (uuu$ ?v2) (uuv$ ?v0) (uuv$ ?v1) id$)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree$)) (= (tree_recurse$a ?v0 ?v1 ?v2) (unfold_tree$d (uuw$ ?v2) (uux$ ?v0) (uux$ ?v1) id$a)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B$)) (= (comp$an (map_prod$f ?v0 id$) (convol$ id$ ?v1) ?v2) (fun_app$b (convol$ (fun_app$t (comp$a id$) ?v0) ?v1) ?v2)) ))
(assert (forall ((?v0 B_b_tree_fun$) (?v1 B_b_fun$) (?v2 B$)) (= (comp$ao (map_prod$n ?v0 id$) (convol$ id$ ?v1) ?v2) (convol$a (fun_app$eb (comp$ap id$a) ?v0) ?v1 ?v2)) ))
(assert (forall ((?v0 B_tree_b_fun$) (?v1 B_tree_b_fun$) (?v2 B_tree$)) (= (comp$aq (map_prod$o ?v0 id$) (convol$b id$a ?v1) ?v2) (convol$c (fun_app$ec (comp$ar id$) ?v0) ?v1 ?v2)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_fun$) (?v2 B_tree$)) (= (comp$as (map_prod$m ?v0 id$) (convol$b id$a ?v1) ?v2) (fun_app$ed (convol$b (fun_app$s (comp$ id$a) ?v0) ?v1) ?v2)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_tree_fun$) (?v2 B$)) (= (comp$at (map_prod$l ?v0 id$a) (convol$d id$ ?v1) ?v2) (fun_app$ee (convol$d (fun_app$t (comp$a id$) ?v0) ?v1) ?v2)) ))
(assert (forall ((?v0 B_b_tree_fun$) (?v1 B_b_tree_fun$) (?v2 B$)) (= (comp$au (map_prod$p ?v0 id$a) (convol$d id$ ?v1) ?v2) (convol$e (fun_app$eb (comp$ap id$a) ?v0) ?v1 ?v2)) ))
(assert (forall ((?v0 B_tree_b_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree$)) (= (comp$av (map_prod$q ?v0 id$a) (convol$f id$a ?v1) ?v2) (convol$g (fun_app$ec (comp$ar id$) ?v0) ?v1 ?v2)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree$)) (= (comp$aw (fun_app$cs (map_prod$k ?v0) id$a) (convol$f id$a ?v1) ?v2) (fun_app$ (convol$f (fun_app$s (comp$ id$a) ?v0) ?v1) ?v2)) ))
(assert (forall ((?v0 A_a_fun$) (?v1 A_tree$)) (= (fun_app$bd dtor_tree$a (fun_app$bf (map_tree$c ?v0) ?v1)) (fun_app$ef (map_pre_tree$k ?v0 (map_tree$c ?v0)) (fun_app$bd dtor_tree$a ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_tree$)) (= (fun_app$bc dtor_tree$ (fun_app$d (map_tree$ ?v0) ?v1)) (fun_app$eg (map_pre_tree$l ?v0 (map_tree$ ?v0)) (fun_app$bd dtor_tree$a ?v1))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree$)) (= (fun_app$bc dtor_tree$ (fun_app$x (map_tree$a ?v0) ?v1)) (fun_app$cm (map_pre_tree$d ?v0 (map_tree$a ?v0)) (fun_app$bc dtor_tree$ ?v1))) ))
(assert (forall ((?v0 A_tree_a_tree_fun$) (?v1 A_a_fun$)) (=> (= (comp$ax dtor_tree$a ?v0) (comp$ay (map_pre_tree$k ?v1 ?v0) dtor_tree$a)) (= ?v0 (map_tree$c ?v1))) ))
(assert (forall ((?v0 A_tree_b_tree_fun$) (?v1 A_b_fun$)) (=> (= (comp$az dtor_tree$ ?v0) (comp$ba (map_pre_tree$l ?v1 ?v0) dtor_tree$a)) (= ?v0 (map_tree$ ?v1))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_b_fun$)) (=> (= (comp$bb dtor_tree$ ?v0) (comp$bc (map_pre_tree$d ?v1 ?v0) dtor_tree$)) (= ?v0 (map_tree$a ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$)) (= (fun_app$bm (comp$i (fun_app$eh (convol$h ?v0) ?v1)) ?v2) (fun_app$eh (convol$h (fun_app$v (comp$b ?v0) ?v2)) (fun_app$v (comp$b ?v1) ?v2))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A$)) (! (= (fun_app$dp (fun_app$cz (tree_recurse$b ?v0) ?v1) ?v2) (node$a ?v2 (fun_app$bf (map_tree$c ?v0) (fun_app$dp (fun_app$cz (tree_recurse$b ?v0) ?v1) ?v2)) (fun_app$bf (map_tree$c ?v1) (fun_app$dp (fun_app$cz (tree_recurse$b ?v0) ?v1) ?v2)))) :pattern ((fun_app$dp (fun_app$cz (tree_recurse$b ?v0) ?v1) ?v2)))))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$)) (= (fun_app$ei (comp$bd (map_prod$g ?v0 ?v1)) (convol$i ?v2 ?v3)) (fun_app$eh (convol$h (fun_app$v (comp$b ?v0) ?v2)) (fun_app$v (comp$b ?v1) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$)) (= (fun_app$dw (comp$ah (map_tree$ ?v0)) (dtor_corec_tree$a ?v1)) (dtor_corec_tree$b (comp$be (map_pre_tree$m ?v0 (map_sum$ (map_tree$ ?v0) id$)) ?v1))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$)) (= (fun_app$bt (comp$q (map_tree$ ?v0)) (dtor_corec_tree$c ?v1)) (dtor_corec_tree$d (comp$bf (map_pre_tree$n ?v0 (map_sum$a (map_tree$ ?v0) id$a)) ?v1))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 B_a_a_tree_b_sum_a_tree_b_sum_prod_prod_fun$)) (= (comp$ak (map_tree$c ?v0) (dtor_corec_tree$a ?v1)) (dtor_corec_tree$a (fun_app$ej (comp$bg (map_pre_tree$o ?v0 (map_sum$b (map_tree$c ?v0) id$))) ?v1))) ))
(assert (forall ((?v0 A_a_fun$) (?v1 B_tree_a_a_tree_b_tree_sum_a_tree_b_tree_sum_prod_prod_fun$)) (= (comp$o (map_tree$c ?v0) (dtor_corec_tree$c ?v1)) (dtor_corec_tree$c (fun_app$ek (comp$bh (map_pre_tree$p ?v0 (map_sum$c (map_tree$c ?v0) id$a))) ?v1))) ))
(assert (forall ((?v0 B$) (?v1 A_a_fun$) (?v2 A$)) (= (fun_app$ac (fun_app$v (comp$b (uue$ ?v0)) ?v1) ?v2) ?v0) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$) (?v1 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$)) (= (= (uuy$ ?v0) (uuy$ ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$)) (= (= (uuz$ ?v0) (uuz$ ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$)) (= (comp$bi (map_sum$d ?v0 ?v1) (map_sum$e ?v2 ?v3)) (map_sum$d (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_a_sum$)) (= (fun_app$el (map_sum$d ?v0 ?v1) (fun_app$em (map_sum$e ?v2 ?v3) ?v4)) (fun_app$el (map_sum$d (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_a_sum$)) (= (fun_app$el (map_sum$d ?v0 ?v1) (fun_app$em (map_sum$e ?v2 ?v3) ?v4)) (fun_app$el (map_sum$d (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3)) ?v4)) ))
(assert (= (map_sum$f id$ id$) id$b))
(assert (= (map_sum$g id$ id$a) id$w))
(assert (= (map_sum$h id$a id$) id$x))
(assert (= (map_sum$i id$a id$a) id$y))
(assert (forall ((?v0 B_b_sum$)) (= (fun_app$cn (map_sum$f id$ id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_b_tree_sum$)) (= (fun_app$en (map_sum$g id$ id$a) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_sum$)) (= (fun_app$eo (map_sum$h id$a id$) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_tree_sum$)) (= (fun_app$ep (map_sum$i id$a id$a) ?v0) ?v0) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_a_b_fun_fun$) (?v2 Bool) (?v3 A_b_fun$) (?v4 B_tree_a_b_fun_sum$)) (= (fun_app$ca (fun_app$eq (map_sum$j ?v0) ?v1) (ite ?v2 (inr$ ?v3) ?v4)) (ite ?v2 (inr$ (fun_app$u ?v1 ?v3)) (fun_app$ca (fun_app$eq (map_sum$j ?v0) ?v1) ?v4))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_a_b_fun_fun$) (?v2 Bool) (?v3 B_tree_a_b_fun_sum$) (?v4 A_b_fun$)) (= (fun_app$ca (fun_app$eq (map_sum$j ?v0) ?v1) (ite ?v2 ?v3 (inr$ ?v4))) (ite ?v2 (fun_app$ca (fun_app$eq (map_sum$j ?v0) ?v1) ?v3) (inr$ (fun_app$u ?v1 ?v4)))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_a_b_fun_fun$)) (= (comp$bj (fun_app$eq (map_sum$j ?v0) ?v1) uun$) (comp$bk uun$ ?v1)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_a_b_fun_fun$) (?v2 A_b_fun$)) (! (= (fun_app$ca (fun_app$eq (map_sum$j ?v0) ?v1) (inr$ ?v2)) (inr$ (fun_app$u ?v1 ?v2))) :pattern ((fun_app$ca (fun_app$eq (map_sum$j ?v0) ?v1) (inr$ ?v2))))))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$)) (= (comp$bl (case_sum$d ?v0 ?v1) (map_sum$e ?v2 ?v3)) (case_sum$d (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3))) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 B_tree_b_tree_fun$) (?v3 A_b_fun_a_b_fun_fun$)) (= (fun_app$cv (comp$z (fun_app$bb (case_sum$ ?v0) ?v1)) (fun_app$eq (map_sum$j ?v2) ?v3)) (fun_app$bb (case_sum$ (fun_app$s (comp$ ?v0) ?v2)) (fun_app$dh (comp$bm ?v1) ?v3))) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_b_fun$) (?v2 A_a_fun$) (?v3 A_a_fun$) (?v4 A_a_sum$)) (= (fun_app$cj (case_sum$d ?v0 ?v1) (fun_app$em (map_sum$e ?v2 ?v3) ?v4)) (fun_app$cj (case_sum$d (fun_app$v (comp$b ?v0) ?v2) (fun_app$v (comp$b ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 A_b_fun_b_tree_fun$) (?v2 B_tree_b_tree_fun$) (?v3 A_b_fun_a_b_fun_fun$) (?v4 B_tree_a_b_fun_sum$)) (= (fun_app$w (fun_app$bb (case_sum$ ?v0) ?v1) (fun_app$ca (fun_app$eq (map_sum$j ?v2) ?v3) ?v4)) (fun_app$w (fun_app$bb (case_sum$ (fun_app$s (comp$ ?v0) ?v2)) (fun_app$dh (comp$bm ?v1) ?v3)) ?v4)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_b_fun$) (?v2 B_b_sum$)) (= (comp$bn (case_sum$a id$ ?v0) (map_sum$f ?v1 id$) ?v2) (fun_app$ci (case_sum$a (fun_app$t (comp$a ?v1) id$) ?v0) ?v2)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 A_b_fun$) (?v2 A_b_sum$)) (= (comp$bo (case_sum$a id$ ?v0) (map_sum$k ?v1 id$) ?v2) (case_sum$c (fun_app$v (comp$b ?v1) id$f) ?v0 ?v2)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_b_fun$) (?v2 B_tree_b_sum$)) (= (comp$bp (case_sum$a id$ ?v0) (map_sum$l ?v1 id$) ?v2) (case_sum$g (fun_app$er (comp$bq ?v1) id$a) ?v0 ?v2)) ))
(assert (forall ((?v0 B_tree_b_fun$) (?v1 B_b_fun$) (?v2 B_b_tree_sum$)) (= (comp$br (case_sum$h id$ ?v0) (map_sum$g ?v1 id$a) ?v2) (fun_app$es (case_sum$h (fun_app$t (comp$a ?v1) id$) ?v0) ?v2)) ))
(assert (forall ((?v0 B_b_tree_fun$) (?v1 B_b_tree_fun$) (?v2 B_b_sum$)) (= (comp$bs (case_sum$i id$a ?v0) (map_sum$m ?v1 id$) ?v2) (case_sum$j (fun_app$ea (comp$bt ?v1) id$) ?v0 ?v2)) ))
(assert (forall ((?v0 B_tree_b_fun$) (?v1 A_b_fun$) (?v2 A_b_tree_sum$)) (= (comp$bu (case_sum$h id$ ?v0) (map_sum$n ?v1 id$a) ?v2) (case_sum$b (fun_app$v (comp$b ?v1) id$f) ?v0 ?v2)) ))
(assert (forall ((?v0 B_tree_b_fun$) (?v1 B_tree_b_fun$) (?v2 B_tree_b_tree_sum$)) (= (comp$bv (case_sum$h id$ ?v0) (map_sum$o ?v1 id$a) ?v2) (case_sum$k (fun_app$er (comp$bq ?v1) id$a) ?v0 ?v2)) ))
(assert (forall ((?v0 B_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree_b_sum$)) (= (comp$bw (case_sum$i id$a ?v0) (map_sum$h ?v1 id$) ?v2) (fun_app$et (case_sum$i (fun_app$s (comp$ ?v1) id$a) ?v0) ?v2)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_b_tree_fun$) (?v2 B_b_tree_sum$)) (= (comp$bx (case_sum$l id$a ?v0) (map_sum$p ?v1 id$a) ?v2) (case_sum$m (fun_app$ea (comp$bt ?v1) id$) ?v0 ?v2)) ))
(assert (forall ((?v0 B_tree_b_tree_fun$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree_b_tree_sum$)) (= (comp$by (case_sum$l id$a ?v0) (map_sum$i ?v1 id$a) ?v2) (fun_app$eu (case_sum$l (fun_app$s (comp$ ?v1) id$a) ?v0) ?v2)) ))
(assert (forall ((?v0 A_bool_fun$) (?v1 A$) (?v2 A_tree$) (?v3 A_tree$)) (! (= (pred_tree$ ?v0 (node$a ?v1 ?v2 ?v3)) (and (fun_app$ev ?v0 ?v1) (and (pred_tree$ ?v0 ?v2) (pred_tree$ ?v0 ?v3)))) :pattern ((pred_tree$ ?v0 (node$a ?v1 ?v2 ?v3))))))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (! (= (id_bnf$a ?v0) ?v0) :pattern ((id_bnf$a ?v0)))))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (! (= (id_bnf$ ?v0) ?v0) :pattern ((id_bnf$ ?v0)))))
(assert (forall ((?v0 B_b_fun$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (apfst$ ?v0 (pair$c ?v1 ?v2)) (pair$c (fun_app$aa ?v0 ?v1) ?v2)) :pattern ((apfst$ ?v0 (pair$c ?v1 ?v2))))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (! (= (fun_app$ay (apfst$a ?v0) (pair$b ?v1 ?v2)) (pair$b (fun_app$ca ?v0 ?v1) ?v2)) :pattern ((fun_app$ay (apfst$a ?v0) (pair$b ?v1 ?v2))))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_fun$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (apsnd$ ?v0 (pair$c ?v1 ?v2)) (pair$c ?v1 (fun_app$ay ?v0 ?v2))) :pattern ((apsnd$ ?v0 (pair$c ?v1 ?v2))))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_fun$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (! (= (fun_app$ay (apsnd$a ?v0) (pair$b ?v1 ?v2)) (pair$b ?v1 (fun_app$ca ?v0 ?v2))) :pattern ((fun_app$ay (apsnd$a ?v0) (pair$b ?v1 ?v2))))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)) (! (= (apsnd$b ?v0) (map_prod$ id$ ?v0)) :pattern ((apsnd$b ?v0)))))
(assert (forall ((?v0 A_a_fun$) (?v1 A_a_fun$) (?v2 A$) (?v3 A_a_fun$) (?v4 A_a_fun$) (?v5 A_b_fun$)) (=> (= (fun_app$aw ?v0 (fun_app$aw ?v1 ?v2)) (fun_app$aw ?v3 (fun_app$aw ?v4 ?v2))) (= (fun_app$ac (fun_app$v (comp$b (fun_app$v (comp$b ?v5) ?v0)) ?v1) ?v2) (fun_app$ac (fun_app$v (comp$b (fun_app$v (comp$b ?v5) ?v3)) ?v4) ?v2))) ))
(assert (forall ((?v0 B_b_tree_b_tree_prod_prod$)) (! (= (id_bnf$a ?v0) ?v0) :pattern ((id_bnf$a ?v0)))))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (! (= (id_bnf$ ?v0) ?v0) :pattern ((id_bnf$ ?v0)))))
(assert (forall ((?v0 B$) (?v1 B_b_fun$) (?v2 B$)) (=> (= ?v0 (fun_app$aa ?v1 ?v2)) (fun_app$ew (fun_app$ex (fun_app$ey (fun_app$ez (fun_app$fa (iso_tuple_update_accessor_eq_assist$ id$d) id$) ?v2) ?v1) ?v0) ?v2)) ))
(assert (forall ((?v0 B_tree$) (?v1 B_tree_b_tree_fun$) (?v2 B_tree$)) (=> (= ?v0 (fun_app$x ?v1 ?v2)) (fun_app$dg (fun_app$fb (fun_app$fc (fun_app$fd (fun_app$fe (iso_tuple_update_accessor_eq_assist$a id$c) id$a) ?v2) ?v1) ?v0) ?v2)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (fst$a (fun_app$az (map_prod$ ?v0 ?v1) ?v2)) (fun_app$aa ?v0 (fst$c ?v2))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (fst$ (fun_app$am (fun_app$ba (map_prod$a ?v0) ?v1) ?v2)) (fun_app$w ?v0 (fst$b ?v2))) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$) (?v2 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (snd$a (fun_app$az (map_prod$ ?v0 ?v1) ?v2)) (fun_app$am ?v1 (snd$c ?v2))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (snd$ (fun_app$am (fun_app$ba (map_prod$a ?v0) ?v1) ?v2)) (fun_app$w ?v1 (snd$b ?v2))) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (pair$c (fst$c ?v0) (snd$c ?v0)) ?v0) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (pair$b (fst$b ?v0) (snd$b ?v0)) ?v0) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)) (= (comp$bz uva$ (map_prod$ ?v0 ?v1)) (comp$ca ?v0 uvb$)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$)) (= (comp$cb uvc$ (fun_app$ba (map_prod$a ?v0) ?v1)) (comp$cc ?v0 uvd$)) ))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)) (= (comp$cd uve$ (map_prod$ ?v0 ?v1)) (comp$ce ?v1 uvf$)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$)) (= (comp$cb uvg$ (fun_app$ba (map_prod$a ?v0) ?v1)) (comp$cc ?v1 uvh$)) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= ?v0 (pair$c (fst$c ?v0) (snd$c ?v0))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= ?v0 (pair$b (fst$b ?v0) (snd$b ?v0))) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (=> (=> (= ?v0 (pair$c (fst$c ?v0) (snd$c ?v0))) false) false) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (=> (= ?v0 (pair$b (fst$b ?v0) (snd$b ?v0))) false) false) ))
(assert (forall ((?v0 B_bool_fun$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (and (fun_app$ew ?v0 ?v1) (fun_app$af ?v2 ?v3)) (and (fun_app$ew ?v0 (fst$c (pair$c ?v1 ?v3))) (fun_app$af ?v2 (snd$c (pair$c ?v1 ?v3))))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_bool_fun$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum_bool_fun$) (?v3 B_tree_a_b_fun_sum$)) (=> (and (fun_app$ad ?v0 ?v1) (fun_app$ad ?v2 ?v3)) (and (fun_app$ad ?v0 (fst$b (pair$b ?v1 ?v3))) (fun_app$ad ?v2 (snd$b (pair$b ?v1 ?v3))))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_bool_fun_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B$)) (=> (fun_app$ew (fun_app$ff ?v0 ?v1) ?v2) (fun_app$ew (fun_app$ff ?v0 (snd$c (pair$c ?v2 ?v1))) (fst$c (pair$c ?v2 ?v1)))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_bool_fun_fun$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (=> (fun_app$ad (fun_app$ae ?v0 ?v1) ?v2) (fun_app$ad (fun_app$ae ?v0 (snd$b (pair$b ?v2 ?v1))) (fst$b (pair$b ?v2 ?v1)))) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (= ?v0 (pair$c ?v1 ?v2)) (= (fst$c ?v0) ?v1)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (=> (= ?v0 (pair$b ?v1 ?v2)) (= (fst$b ?v0) ?v1)) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fst$c (pair$c ?v0 ?v1)) ?v0) :pattern ((pair$c ?v0 ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$)) (! (= (fst$b (pair$b ?v0 ?v1)) ?v0) :pattern ((pair$b ?v0 ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B$)) (=> (= (fst$c (pair$c ?v0 ?v1)) ?v2) (= ?v0 ?v2)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (=> (= (fst$b (pair$b ?v0 ?v1)) ?v2) (= ?v0 ?v2)) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (= ?v0 (pair$c ?v1 ?v2)) (= (snd$c ?v0) ?v2)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (=> (= ?v0 (pair$b ?v1 ?v2)) (= (snd$b ?v0) ?v2)) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (snd$c (pair$c ?v0 ?v1)) ?v1) :pattern ((pair$c ?v0 ?v1)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$)) (! (= (snd$b (pair$b ?v0 ?v1)) ?v1) :pattern ((pair$b ?v0 ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (= (snd$c (pair$c ?v0 ?v1)) ?v2) (= ?v1 ?v2)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$)) (=> (= (snd$b (pair$b ?v0 ?v1)) ?v2) (= ?v1 ?v2)) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_bool_fun_fun$) (?v1 B$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v3 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (=> (and (fun_app$af (fun_app$ag ?v0 ?v1) ?v2) (= ?v3 (pair$c ?v1 ?v2))) (fun_app$af (fun_app$ag ?v0 (fst$c ?v3)) (snd$c ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_bool_fun_fun$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (and (fun_app$ad (fun_app$ae ?v0 ?v1) ?v2) (= ?v3 (pair$b ?v1 ?v2))) (fun_app$ad (fun_app$ae ?v0 (fst$b ?v3)) (snd$b ?v3))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod$)) (! (= (swap$ ?v0) (pair$c (snd$h ?v0) (fst$h ?v0))) :pattern ((swap$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (swap$b ?v0) (pair$b (snd$b ?v0) (fst$b ?v0))) :pattern ((swap$b ?v0)))))
(assert (forall ((?v0 B$)) (= (fun_app$aa (fun_app$fg (comp$cf uvi$) uvj$) ?v0) (fun_app$aa id$ ?v0)) ))
(assert (forall ((?v0 B_tree$)) (= (fun_app$x (fun_app$fh (comp$cg uvg$) uvk$) ?v0) (fun_app$x id$a ?v0)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$)) (= (fun_app$ca (fun_app$fi (comp$ch uvh$) uvl$) ?v0) (id$z ?v0)) ))
(assert (forall ((?v0 B$)) (= (fun_app$aa (fun_app$fg (comp$cf uvm$) uvj$) ?v0) (fun_app$aa id$ ?v0)) ))
(assert (forall ((?v0 B_tree$)) (= (fun_app$x (fun_app$fh (comp$cg uvc$) uvk$) ?v0) (fun_app$x id$a ?v0)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$)) (= (fun_app$ca (fun_app$fi (comp$ch uvd$) uvl$) ?v0) (id$z ?v0)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v1 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (= ?v0 (snd$c ?v1)) (exists ((?v2 B$)) (= ?v1 (pair$c ?v2 ?v0)) )) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (= ?v0 (snd$b ?v1)) (exists ((?v2 B_tree_a_b_fun_sum$)) (= ?v1 (pair$b ?v2 ?v0)) )) ))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$) (?v2 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod_set$) (?v3 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (=> (and (member$a (pair$c ?v0 ?v1) ?v2) (= ?v3 ?v1)) (member$a (pair$c ?v0 ?v3) ?v2)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$) (?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_set$) (?v3 B_tree_a_b_fun_sum$)) (=> (and (member$ (pair$b ?v0 ?v1) ?v2) (= ?v3 ?v1)) (member$ (pair$b ?v0 ?v3) ?v2)) ))
(assert (forall ((?v0 B$) (?v1 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (= (= ?v0 (fst$c ?v1)) (exists ((?v2 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= ?v1 (pair$c ?v0 ?v2)) )) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (= ?v0 (fst$b ?v1)) (exists ((?v2 B_tree_a_b_fun_sum$)) (= ?v1 (pair$b ?v0 ?v2)) )) ))
(assert (forall ((?v0 A_b_fun$) (?v1 A_a_fun$)) (= (fun_app$v (comp$b (ctor_rec$ ?v0)) ?v1) (ctor_rec$ (fun_app$v (comp$b ?v0) (fun_app$bh (comp$e (fun_app$bh (comp$e id_bnf$c) ?v1)) id_bnf$c)))) ))
(assert (forall ((?v0 A_b_fun$)) (= ?v0 (ctor_rec$ (fun_app$v (comp$b ?v0) id_bnf$c))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum$) (?v1 B_tree_a_b_fun_sum$)) (! (= (pair$b ?v0 ?v1) (xtor$ (id_bnf$d (pair$b ?v0 ?v1)))) :pattern ((pair$b ?v0 ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_tree_b_tree_prod$)) (! (= (pair$a ?v0 ?v1) (xtor$a (id_bnf$a (pair$a ?v0 ?v1)))) :pattern ((pair$a ?v0 ?v1)))))
(assert (forall ((?v0 B$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (pair$c ?v0 ?v1) (xtor$b (id_bnf$ (pair$c ?v0 ?v1)))) :pattern ((pair$c ?v0 ?v1)))))
(assert (forall ((?v0 A_b_fun$)) (! (= (inr$ ?v0) (xtor$c (id_bnf$e (inr$ ?v0)))) :pattern ((inr$ ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_prod$)) (= (snd$h ?v0) (comp$ci uvb$ (uncurry$ uvn$) ?v0)) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (= (snd$b ?v0) (fun_app$f (fun_app$fj (comp$cj uvd$) (uncurry$a uvo$)) ?v0)) ))
(assert (= (uncurry$b uvp$) id$n))
(assert (= (uncurry$a uvq$) id$aa))
(assert (forall ((?v0 B_b_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_b_tree_b_tree_prod_fun$)) (= (map_prod$ ?v0 ?v1) (uncurry$c (uvr$ ?v0 ?v1))) ))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_fun$) (?v1 B_tree_a_b_fun_sum_b_tree_fun$)) (= (fun_app$ba (map_prod$a ?v0) ?v1) (uncurry$d (uvs$ ?v0 ?v1))) ))
(assert (forall ((?v0 B_b_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod_prod$)) (! (= (fun_app$cd (uncurry$b uvp$) ?v0) ?v0) :pattern ((fun_app$cd (uncurry$b uvp$) ?v0)))))
(assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$ay (uncurry$a uvq$) ?v0) ?v0) :pattern ((fun_app$ay (uncurry$a uvq$) ?v0)))))
(check-sat)
(exit)