include('Axioms/alignment+2.ax').
fof(ne_ty_2Esptree_2Espt,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Esptree_2Espt(A0)) ) )).
fof(mem_c_2Esptree_2EBN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EBN(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))) ) )).
fof(mem_c_2Esptree_2EBS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EBS(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))) ) )).
fof(mem_c_2Esptree_2ELN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2ELN(A_27a),ty_2Esptree_2Espt(A_27a)) ) )).
fof(mem_c_2Esptree_2ELS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2ELS(A_27a),arr(A_27a,ty_2Esptree_2Espt(A_27a))) ) )).
fof(mem_c_2Esptree_2Edelete,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Edelete(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))) ) )).
fof(mem_c_2Esptree_2Edifference,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Edifference(A_27a,A_27b),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a)))) ) ) )).
fof(mem_c_2Esptree_2Edomain,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Edomain(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Enum_2Enum,bool))) ) )).
fof(mem_c_2Esptree_2Efilter__v,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Efilter__v(A_27a),arr(arr(A_27a,bool),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))) ) )).
fof(mem_c_2Esptree_2Efoldi,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Efoldi(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a))),arr(ty_2Enum_2Enum,arr(A_27a,arr(ty_2Esptree_2Espt(A_27b),A_27a))))) ) ) )).
fof(mem_c_2Esptree_2EfromAList,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EfromAList(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ty_2Esptree_2Espt(A_27a))) ) )).
fof(mem_c_2Esptree_2EfromList,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EfromList(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Esptree_2Espt(A_27a))) ) )).
fof(mem_c_2Esptree_2Einsert,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Einsert(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))) ) )).
fof(mem_c_2Esptree_2Einter,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Einter(A_27a,A_27b),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a)))) ) ) )).
fof(mem_c_2Esptree_2Einter__eq,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Einter__eq(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))) ) )).
fof(mem_c_2Esptree_2Elist__insert,axiom,( mem(c_2Esptree_2Elist__insert,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),arr(ty_2Esptree_2Espt(ty_2Eone_2Eone),ty_2Esptree_2Espt(ty_2Eone_2Eone)))) )).
fof(mem_c_2Esptree_2Elist__to__num__set,axiom,( mem(c_2Esptree_2Elist__to__num__set,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Esptree_2Espt(ty_2Eone_2Eone))) )).
fof(mem_c_2Esptree_2Elookup,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Elookup(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27a),ty_2Eoption_2Eoption(A_27a)))) ) )).
fof(mem_c_2Esptree_2Elrnext,axiom,( mem(c_2Esptree_2Elrnext,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Esptree_2Emap,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Emap(A_27a,A_27b),arr(arr(A_27b,A_27a),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a)))) ) ) )).
fof(mem_c_2Esptree_2Emapi,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Emapi(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,A_27a)),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a)))) ) ) )).
fof(mem_c_2Esptree_2Emapi0,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Emapi0(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,A_27a)),arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a))))) ) ) )).
fof(mem_c_2Esptree_2Emk__BN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Emk__BN(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))) ) )).
fof(mem_c_2Esptree_2Emk__BS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Emk__BS(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))) ) )).
fof(mem_c_2Esptree_2Emk__wf,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Emk__wf(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))) ) )).
fof(mem_c_2Esptree_2Esize,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Esize(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Esptree_2Espt__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Espt__CASE(A_27a,A_27b),arr(ty_2Esptree_2Espt(A_27a),arr(A_27b,arr(arr(A_27a,A_27b),arr(arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b)),arr(arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b))),A_27b)))))) ) ) )).
fof(mem_c_2Esptree_2Espt__acc,axiom,( mem(c_2Esptree_2Espt__acc,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Esptree_2Espt__center,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Espt__center(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Eoption_2Eoption(A_27a))) ) )).
fof(mem_c_2Esptree_2Espt__fold,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Esptree_2Espt__fold(A_27a,A_27b),arr(arr(A_27b,arr(A_27a,A_27a)),arr(A_27a,arr(ty_2Esptree_2Espt(A_27b),A_27a)))) ) ) )).
fof(mem_c_2Esptree_2Espt__left,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Espt__left(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))) ) )).
fof(mem_c_2Esptree_2Espt__right,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Espt__right(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))) ) )).
fof(mem_c_2Esptree_2Espt__size,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Espt__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Esptree_2Espt(A_27a),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Esptree_2Esubspt,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Esubspt(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),bool))) ) )).
fof(mem_c_2Esptree_2EtoAList,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EtoAList(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)))) ) )).
fof(mem_c_2Esptree_2EtoList,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EtoList(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Esptree_2EtoListA,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2EtoListA(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Esptree_2Eunion,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Eunion(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))) ) )).
fof(mem_c_2Esptree_2Ewf,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Esptree_2Ewf(A_27a),arr(ty_2Esptree_2Espt(A_27a),bool)) ) )).
fof(ax_thm_2Esptree_2Espt__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Esptree_2Espt(A_27a),ty_2Eind__type_2Erecspace(A_27a))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(A_27a),ty_2Esptree_2Espt(A_27a)),f2345(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Esptree_2Espt__case__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0v] : ( mem(V0v,A_27b) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2f1] : ( mem(V2f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V3f2] : ( mem(V3f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),c_2Esptree_2ELN(A_27a)),V0v),V1f),V2f1),V3f2) = V0v ) ) ) ) ) ) & ( ( ! [V4a] : ( mem(V4a,A_27a) => ! [V5v] : ( mem(V5v,A_27b) => ! [V6f] : ( mem(V6f,arr(A_27a,A_27b)) => ! [V7f1] : ( mem(V7f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V8f2] : ( mem(V8f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),ap(c_2Esptree_2ELS(A_27a),V4a)),V5v),V6f),V7f1),V8f2) = ap(V6f,V4a) ) ) ) ) ) ) ) & ( ( ! [V9a0] : ( mem(V9a0,ty_2Esptree_2Espt(A_27a)) => ! [V10a1] : ( mem(V10a1,ty_2Esptree_2Espt(A_27a)) => ! [V11v] : ( mem(V11v,A_27b) => ! [V12f] : ( mem(V12f,arr(A_27a,A_27b)) => ! [V13f1] : ( mem(V13f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V14f2] : ( mem(V14f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),ap(ap(c_2Esptree_2EBN(A_27a),V9a0),V10a1)),V11v),V12f),V13f1),V14f2) = ap(ap(V13f1,V9a0),V10a1) ) ) ) ) ) ) ) ) & ! [V15a0] : ( mem(V15a0,ty_2Esptree_2Espt(A_27a)) => ! [V16a1] : ( mem(V16a1,A_27a) => ! [V17a2] : ( mem(V17a2,ty_2Esptree_2Espt(A_27a)) => ! [V18v] : ( mem(V18v,A_27b) => ! [V19f] : ( mem(V19f,arr(A_27a,A_27b)) => ! [V20f1] : ( mem(V20f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V21f2] : ( mem(V21f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),ap(ap(ap(c_2Esptree_2EBS(A_27a),V15a0),V16a1),V17a2)),V18v),V19f),V20f1),V21f2) = ap(ap(ap(V21f2,V15a0),V16a1),V17a2) ) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Esptree_2Espt__size__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Esptree_2Espt__size(A_27a),V0f),c_2Esptree_2ELN(A_27a)) = c_2Enum_2E0 ) ) ) & ( ( ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ! [V2a] : ( mem(V2a,A_27a) => ( ap(ap(c_2Esptree_2Espt__size(A_27a),V1f),ap(c_2Esptree_2ELS(A_27a),V2a)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(V1f,V2a)) ) ) ) ) & ( ( ! [V3f] : ( mem(V3f,arr(A_27a,ty_2Enum_2Enum)) => ! [V4a0] : ( mem(V4a0,ty_2Esptree_2Espt(A_27a)) => ! [V5a1] : ( mem(V5a1,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Espt__size(A_27a),V3f),ap(ap(c_2Esptree_2EBN(A_27a),V4a0),V5a1)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Esptree_2Espt__size(A_27a),V3f),V4a0)),ap(ap(c_2Esptree_2Espt__size(A_27a),V3f),V5a1))) ) ) ) ) ) & ! [V6f] : ( mem(V6f,arr(A_27a,ty_2Enum_2Enum)) => ! [V7a0] : ( mem(V7a0,ty_2Esptree_2Espt(A_27a)) => ! [V8a1] : ( mem(V8a1,A_27a) => ! [V9a2] : ( mem(V9a2,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Espt__size(A_27a),V6f),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7a0),V8a1),V9a2)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Esptree_2Espt__size(A_27a),V6f),V7a0)),ap(ap(c_2Earithmetic_2E_2B,ap(V6f,V8a1)),ap(ap(c_2Esptree_2Espt__size(A_27a),V6f),V9a2)))) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Edatatype__spt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0spt] : ( mem(V0spt,arr(ty_2Esptree_2Espt(A_27a),arr(arr(A_27a,ty_2Esptree_2Espt(A_27a)),arr(arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))),arr(arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))),bool))))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(ap(V0spt,c_2Esptree_2ELN(A_27a)),c_2Esptree_2ELS(A_27a)),c_2Esptree_2EBN(A_27a)),c_2Esptree_2EBS(A_27a)))) )))).
fof(conj_thm_2Esptree_2Espt__11,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,A_27a) => ! [V1a_27] : ( mem(V1a_27,A_27a) => ( ( ap(c_2Esptree_2ELS(A_27a),V0a) = ap(c_2Esptree_2ELS(A_27a),V1a_27) ) <=> ( V0a = V1a_27 ) ) ) ) ) & ( ( ! [V2a0] : ( mem(V2a0,ty_2Esptree_2Espt(A_27a)) => ! [V3a1] : ( mem(V3a1,ty_2Esptree_2Espt(A_27a)) => ! [V4a0_27] : ( mem(V4a0_27,ty_2Esptree_2Espt(A_27a)) => ! [V5a1_27] : ( mem(V5a1_27,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(c_2Esptree_2EBN(A_27a),V2a0),V3a1) = ap(ap(c_2Esptree_2EBN(A_27a),V4a0_27),V5a1_27) ) <=> ( ( V2a0 = V4a0_27 ) & ( V3a1 = V5a1_27 ) ) ) ) ) ) ) ) & ! [V6a0] : ( mem(V6a0,ty_2Esptree_2Espt(A_27a)) => ! [V7a1] : ( mem(V7a1,A_27a) => ! [V8a2] : ( mem(V8a2,ty_2Esptree_2Espt(A_27a)) => ! [V9a0_27] : ( mem(V9a0_27,ty_2Esptree_2Espt(A_27a)) => ! [V10a1_27] : ( mem(V10a1_27,A_27a) => ! [V11a2_27] : ( mem(V11a2_27,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(ap(c_2Esptree_2EBS(A_27a),V6a0),V7a1),V8a2) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V9a0_27),V10a1_27),V11a2_27) ) <=> ( ( V6a0 = V9a0_27 ) & ( ( V7a1 = V10a1_27 ) & ( V8a2 = V11a2_27 ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Espt__distinct,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,A_27a) => ( ~~ ( c_2Esptree_2ELN(A_27a) = ap(c_2Esptree_2ELS(A_27a),V0a) ) ) ) ) & ( ( ! [V1a1] : ( mem(V1a1,ty_2Esptree_2Espt(A_27a)) => ! [V2a0] : ( mem(V2a0,ty_2Esptree_2Espt(A_27a)) => ( ~~ ( c_2Esptree_2ELN(A_27a) = ap(ap(c_2Esptree_2EBN(A_27a),V2a0),V1a1) ) ) ) ) ) & ( ( ! [V3a2] : ( mem(V3a2,ty_2Esptree_2Espt(A_27a)) => ! [V4a1] : ( mem(V4a1,A_27a) => ! [V5a0] : ( mem(V5a0,ty_2Esptree_2Espt(A_27a)) => ( ~~ ( c_2Esptree_2ELN(A_27a) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V5a0),V4a1),V3a2) ) ) ) ) ) ) & ( ( ! [V6a1] : ( mem(V6a1,ty_2Esptree_2Espt(A_27a)) => ! [V7a0] : ( mem(V7a0,ty_2Esptree_2Espt(A_27a)) => ! [V8a] : ( mem(V8a,A_27a) => ( ~~ ( ap(c_2Esptree_2ELS(A_27a),V8a) = ap(ap(c_2Esptree_2EBN(A_27a),V7a0),V6a1) ) ) ) ) ) ) & ( ( ! [V9a2] : ( mem(V9a2,ty_2Esptree_2Espt(A_27a)) => ! [V10a1] : ( mem(V10a1,A_27a) => ! [V11a0] : ( mem(V11a0,ty_2Esptree_2Espt(A_27a)) => ! [V12a] : ( mem(V12a,A_27a) => ( ~~ ( ap(c_2Esptree_2ELS(A_27a),V12a) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V11a0),V10a1),V9a2) ) ) ) ) ) ) ) & ! [V13a2] : ( mem(V13a2,ty_2Esptree_2Espt(A_27a)) => ! [V14a1_27] : ( mem(V14a1_27,A_27a) => ! [V15a1] : ( mem(V15a1,ty_2Esptree_2Espt(A_27a)) => ! [V16a0_27] : ( mem(V16a0_27,ty_2Esptree_2Espt(A_27a)) => ! [V17a0] : ( mem(V17a0,ty_2Esptree_2Espt(A_27a)) => ( ~~ ( ap(ap(c_2Esptree_2EBN(A_27a),V17a0),V15a1) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V16a0_27),V14a1_27),V13a2) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Espt__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0ss] : ( mem(V0ss,ty_2Esptree_2Espt(A_27a)) => ( ( V0ss = c_2Esptree_2ELN(A_27a) ) | ( ( ? [V1a] : ( mem(V1a,A_27a) & ( V0ss = ap(c_2Esptree_2ELS(A_27a),V1a) ) ) ) | ( ( ? [V2s] : ( mem(V2s,ty_2Esptree_2Espt(A_27a)) & ? [V3s0] : ( mem(V3s0,ty_2Esptree_2Espt(A_27a)) & ( V0ss = ap(ap(c_2Esptree_2EBN(A_27a),V2s),V3s0) ) ) ) ) | ? [V4s] : ( mem(V4s,ty_2Esptree_2Espt(A_27a)) & ? [V5a] : ( mem(V5a,A_27a) & ? [V6s0] : ( mem(V6s0,ty_2Esptree_2Espt(A_27a)) & ( V0ss = ap(ap(ap(c_2Esptree_2EBS(A_27a),V4s),V5a),V6s0) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Espt__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f0] : ( mem(V0f0,A_27b) => ! [V1f1] : ( mem(V1f1,arr(A_27a,A_27b)) => ! [V2f2] : ( mem(V2f2,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27b,arr(A_27b,A_27b))))) => ! [V3f3] : ( mem(V3f3,arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27b,arr(A_27b,A_27b)))))) => ? [V4fn] : ( mem(V4fn,arr(ty_2Esptree_2Espt(A_27a),A_27b)) & ( ( ap(V4fn,c_2Esptree_2ELN(A_27a)) = V0f0 ) & ( ( ! [V5a] : ( mem(V5a,A_27a) => ( ap(V4fn,ap(c_2Esptree_2ELS(A_27a),V5a)) = ap(V1f1,V5a) ) ) ) & ( ( ! [V6a0] : ( mem(V6a0,ty_2Esptree_2Espt(A_27a)) => ! [V7a1] : ( mem(V7a1,ty_2Esptree_2Espt(A_27a)) => ( ap(V4fn,ap(ap(c_2Esptree_2EBN(A_27a),V6a0),V7a1)) = ap(ap(ap(ap(V2f2,V6a0),V7a1),ap(V4fn,V6a0)),ap(V4fn,V7a1)) ) ) ) ) & ! [V8a0] : ( mem(V8a0,ty_2Esptree_2Espt(A_27a)) => ! [V9a1] : ( mem(V9a1,A_27a) => ! [V10a2] : ( mem(V10a2,ty_2Esptree_2Espt(A_27a)) => ( ap(V4fn,ap(ap(ap(c_2Esptree_2EBS(A_27a),V8a0),V9a1),V10a2)) = ap(ap(ap(ap(ap(V3f3,V9a1),V8a0),V10a2),ap(V4fn,V8a0)),ap(V4fn,V10a2)) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Esptree_2Espt__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Esptree_2Espt(A_27a),bool)) => ( ( p(ap(V0P,c_2Esptree_2ELN(A_27a))) & ( ( ! [V1a] : ( mem(V1a,A_27a) => p(ap(V0P,ap(c_2Esptree_2ELS(A_27a),V1a))) ) ) & ( ( ! [V2s] : ( mem(V2s,ty_2Esptree_2Espt(A_27a)) => ! [V3s0] : ( mem(V3s0,ty_2Esptree_2Espt(A_27a)) => ( ( p(ap(V0P,V2s)) & p(ap(V0P,V3s0)) ) => p(ap(V0P,ap(ap(c_2Esptree_2EBN(A_27a),V2s),V3s0))) ) ) ) ) & ! [V4s] : ( mem(V4s,ty_2Esptree_2Espt(A_27a)) => ! [V5s0] : ( mem(V5s0,ty_2Esptree_2Espt(A_27a)) => ( ( p(ap(V0P,V4s)) & p(ap(V0P,V5s0)) ) => ! [V6a] : ( mem(V6a,A_27a) => p(ap(V0P,ap(ap(ap(c_2Esptree_2EBS(A_27a),V4s),V6a),V5s0))) ) ) ) ) ) ) ) => ! [V7s] : ( mem(V7s,ty_2Esptree_2Espt(A_27a)) => p(ap(V0P,V7s)) ) ) )))).
fof(conj_thm_2Esptree_2Espt__case__cong,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v_27] : ( mem(V0v_27,A_27b) => ! [V1f_27] : ( mem(V1f_27,arr(A_27a,A_27b)) => ! [V2f1_27] : ( mem(V2f1_27,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V3f2_27] : ( mem(V3f2_27,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ! [V4M] : ( mem(V4M,ty_2Esptree_2Espt(A_27a)) => ! [V5M_27] : ( mem(V5M_27,ty_2Esptree_2Espt(A_27a)) => ! [V6v] : ( mem(V6v,A_27b) => ! [V7f] : ( mem(V7f,arr(A_27a,A_27b)) => ! [V8f1] : ( mem(V8f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V9f2] : ( mem(V9f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ( ( V4M = V5M_27 ) & ( ( ( V5M_27 = c_2Esptree_2ELN(A_27a) ) => ( V6v = V0v_27 ) ) & ( ( ! [V10a] : ( mem(V10a,A_27a) => ( ( V5M_27 = ap(c_2Esptree_2ELS(A_27a),V10a) ) => ( ap(V7f,V10a) = ap(V1f_27,V10a) ) ) ) ) & ( ( ! [V11a0] : ( mem(V11a0,ty_2Esptree_2Espt(A_27a)) => ! [V12a1] : ( mem(V12a1,ty_2Esptree_2Espt(A_27a)) => ( ( V5M_27 = ap(ap(c_2Esptree_2EBN(A_27a),V11a0),V12a1) ) => ( ap(ap(V8f1,V11a0),V12a1) = ap(ap(V2f1_27,V11a0),V12a1) ) ) ) ) ) & ! [V13a0] : ( mem(V13a0,ty_2Esptree_2Espt(A_27a)) => ! [V14a1] : ( mem(V14a1,A_27a) => ! [V15a2] : ( mem(V15a2,ty_2Esptree_2Espt(A_27a)) => ( ( V5M_27 = ap(ap(ap(c_2Esptree_2EBS(A_27a),V13a0),V14a1),V15a2) ) => ( ap(ap(ap(V9f2,V13a0),V14a1),V15a2) = ap(ap(ap(V3f2_27,V13a0),V14a1),V15a2) ) ) ) ) ) ) ) ) ) => ( ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),V4M),V6v),V7f),V8f1),V9f2) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),V5M_27),V0v_27),V1f_27),V2f1_27),V3f2_27) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Esptree_2Espt__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Esptree_2Espt(A_27a)) => ! [V1v] : ( mem(V1v,A_27b) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ! [V3f1] : ( mem(V3f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ! [V4f2] : ( mem(V4f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ! [V5v_27] : ( mem(V5v_27,A_27b) => ( ( ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),V0x),V1v),V2f),V3f1),V4f2) = V5v_27 ) <=> ( ( ( V0x = c_2Esptree_2ELN(A_27a) ) & ( V1v = V5v_27 ) ) | ( ( ? [V6a] : ( mem(V6a,A_27a) & ( ( V0x = ap(c_2Esptree_2ELS(A_27a),V6a) ) & ( ap(V2f,V6a) = V5v_27 ) ) ) ) | ( ( ? [V7s] : ( mem(V7s,ty_2Esptree_2Espt(A_27a)) & ? [V8s0] : ( mem(V8s0,ty_2Esptree_2Espt(A_27a)) & ( ( V0x = ap(ap(c_2Esptree_2EBN(A_27a),V7s),V8s0) ) & ( ap(ap(V3f1,V7s),V8s0) = V5v_27 ) ) ) ) ) | ? [V9s] : ( mem(V9s,ty_2Esptree_2Espt(A_27a)) & ? [V10a] : ( mem(V10a,A_27a) & ? [V11s0] : ( mem(V11s0,ty_2Esptree_2Espt(A_27a)) & ( ( V0x = ap(ap(ap(c_2Esptree_2EBS(A_27a),V9s),V10a),V11s0) ) & ( ap(ap(ap(V4f2,V9s),V10a),V11s0) = V5v_27 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(ax_thm_2Esptree_2Ewf__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( p(ap(c_2Esptree_2Ewf(A_27a),c_2Esptree_2ELN(A_27a))) <=> $true ) & ( ( ! [V0a] : ( mem(V0a,A_27a) => ( p(ap(c_2Esptree_2Ewf(A_27a),ap(c_2Esptree_2ELS(A_27a),V0a))) <=> $true ) ) ) & ( ( ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2))) <=> ( p(ap(c_2Esptree_2Ewf(A_27a),V1t1)) & ( p(ap(c_2Esptree_2Ewf(A_27a),V2t2)) & ( ~~ ( ( V1t1 = c_2Esptree_2ELN(A_27a) ) & ( V2t2 = c_2Esptree_2ELN(A_27a) ) ) ) ) ) ) ) ) ) & ! [V3t1] : ( mem(V3t1,ty_2Esptree_2Espt(A_27a)) => ! [V4a] : ( mem(V4a,A_27a) => ! [V5t2] : ( mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3t1),V4a),V5t2))) <=> ( p(ap(c_2Esptree_2Ewf(A_27a),V3t1)) & ( p(ap(c_2Esptree_2Ewf(A_27a),V5t2)) & ( ~~ ( ( V3t1 = c_2Esptree_2ELN(A_27a) ) & ( V5t2 = c_2Esptree_2ELN(A_27a) ) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Elookup__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27a),bool))) => ( ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => p(ap(ap(V0P,V1k),c_2Esptree_2ELN(A_27a))) ) ) & ( ( ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ! [V3a] : ( mem(V3a,A_27a) => p(ap(ap(V0P,V2k),ap(c_2Esptree_2ELS(A_27a),V3a))) ) ) ) & ( ( ! [V4k] : ( mem(V4k,ty_2Enum_2Enum) => ! [V5t1] : ( mem(V5t1,ty_2Esptree_2Espt(A_27a)) => ! [V6t2] : ( mem(V6t2,ty_2Esptree_2Espt(A_27a)) => ( ( ( ~~ ( V4k = c_2Enum_2E0 ) ) => p(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V4k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V4k)),V5t1),V6t2))) ) => p(ap(ap(V0P,V4k),ap(ap(c_2Esptree_2EBN(A_27a),V5t1),V6t2))) ) ) ) ) ) & ! [V7k] : ( mem(V7k,ty_2Enum_2Enum) => ! [V8t1] : ( mem(V8t1,ty_2Esptree_2Espt(A_27a)) => ! [V9a] : ( mem(V9a,A_27a) => ! [V10t2] : ( mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ( ( ( ~~ ( V7k = c_2Enum_2E0 ) ) => p(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V7k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V7k)),V8t1),V10t2))) ) => p(ap(ap(V0P,V7k),ap(ap(ap(c_2Esptree_2EBS(A_27a),V8t1),V9a),V10t2))) ) ) ) ) ) ) ) ) => ! [V11v] : ( mem(V11v,ty_2Enum_2Enum) => ! [V12v1] : ( mem(V12v1,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,V11v),V12v1)) ) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__def,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0k),c_2Esptree_2ELN(A_27a)) = c_2Eoption_2ENONE(A_27a) ) ) ) & ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,A_27a) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V1k),ap(c_2Esptree_2ELS(A_27a),V2a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),c_2Enum_2E0)),ap(c_2Eoption_2ESOME(A_27a),V2a)),c_2Eoption_2ENONE(A_27a)) ) ) ) ) & ( ( ! [V3t2] : ( mem(V3t2,ty_2Esptree_2Espt(A_27a)) => ! [V4t1] : ( mem(V4t1,ty_2Esptree_2Espt(A_27a)) => ! [V5k] : ( mem(V5k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V5k),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V3t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V5k),c_2Enum_2E0)),c_2Eoption_2ENONE(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V5k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V5k)),V4t1),V3t2))) ) ) ) ) ) & ! [V6t2] : ( mem(V6t2,ty_2Esptree_2Espt(A_27a)) => ! [V7t1] : ( mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ! [V8k] : ( mem(V8k,ty_2Enum_2Enum) => ! [V9a] : ( mem(V9a,A_27a) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V8k),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V9a),V6t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V8k),c_2Enum_2E0)),ap(c_2Eoption_2ESOME(A_27a),V9a)),ap(ap(c_2Esptree_2Elookup(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V8k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V8k)),V7t1),V6t2))) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Einsert__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),bool)))) => ( ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,A_27a) => ( ( ( ( ( ~~ ( V1k = c_2Enum_2E0 ) ) & p(ap(c_2Earithmetic_2EEVEN,V1k)) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V1k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2a),c_2Esptree_2ELN(A_27a))) ) & ( ( ( ~~ ( V1k = c_2Enum_2E0 ) ) & ( ~~ p(ap(c_2Earithmetic_2EEVEN,V1k)) ) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V1k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V2a),c_2Esptree_2ELN(A_27a))) ) ) => p(ap(ap(ap(V0P,V1k),V2a),c_2Esptree_2ELN(A_27a))) ) ) ) ) & ( ( ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ! [V4a] : ( mem(V4a,A_27a) => ! [V5a_27] : ( mem(V5a_27,A_27a) => ( ( ( ( ( ~~ ( V3k = c_2Enum_2E0 ) ) & p(ap(c_2Earithmetic_2EEVEN,V3k)) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V3k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V4a),c_2Esptree_2ELN(A_27a))) ) & ( ( ( ~~ ( V3k = c_2Enum_2E0 ) ) & ( ~~ p(ap(c_2Earithmetic_2EEVEN,V3k)) ) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V3k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V4a),c_2Esptree_2ELN(A_27a))) ) ) => p(ap(ap(ap(V0P,V3k),V4a),ap(c_2Esptree_2ELS(A_27a),V5a_27))) ) ) ) ) ) & ( ( ! [V6k] : ( mem(V6k,ty_2Enum_2Enum) => ! [V7a] : ( mem(V7a,A_27a) => ! [V8t1] : ( mem(V8t1,ty_2Esptree_2Espt(A_27a)) => ! [V9t2] : ( mem(V9t2,ty_2Esptree_2Espt(A_27a)) => ( ( ( ( ( ~~ ( V6k = c_2Enum_2E0 ) ) & p(ap(c_2Earithmetic_2EEVEN,V6k)) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V6k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V7a),V8t1)) ) & ( ( ( ~~ ( V6k = c_2Enum_2E0 ) ) & ( ~~ p(ap(c_2Earithmetic_2EEVEN,V6k)) ) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V6k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V7a),V9t2)) ) ) => p(ap(ap(ap(V0P,V6k),V7a),ap(ap(c_2Esptree_2EBN(A_27a),V8t1),V9t2))) ) ) ) ) ) ) & ! [V10k] : ( mem(V10k,ty_2Enum_2Enum) => ! [V11a] : ( mem(V11a,A_27a) => ! [V12t1] : ( mem(V12t1,ty_2Esptree_2Espt(A_27a)) => ! [V13a_27] : ( mem(V13a_27,A_27a) => ! [V14t2] : ( mem(V14t2,ty_2Esptree_2Espt(A_27a)) => ( ( ( ( ( ~~ ( V10k = c_2Enum_2E0 ) ) & p(ap(c_2Earithmetic_2EEVEN,V10k)) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V10k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V11a),V12t1)) ) & ( ( ( ~~ ( V10k = c_2Enum_2E0 ) ) & ( ~~ p(ap(c_2Earithmetic_2EEVEN,V10k)) ) ) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V10k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V11a),V14t2)) ) ) => p(ap(ap(ap(V0P,V10k),V11a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V12t1),V13a_27),V14t2))) ) ) ) ) ) ) ) ) ) => ! [V15v] : ( mem(V15v,ty_2Enum_2Enum) => ! [V16v1] : ( mem(V16v1,A_27a) => ! [V17v2] : ( mem(V17v2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V15v),V16v1),V17v2)) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Einsert__def,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1a] : ( mem(V1a,A_27a) => ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1a),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V0k),c_2Enum_2E0)),ap(c_2Esptree_2ELS(A_27a),V1a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V0k)),ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V0k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V1a),c_2Esptree_2ELN(A_27a))),c_2Esptree_2ELN(A_27a))),ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V0k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V1a),c_2Esptree_2ELN(A_27a))))) ) ) ) ) & ( ( ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ! [V3a_27] : ( mem(V3a_27,A_27a) => ! [V4a] : ( mem(V4a,A_27a) => ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V2k),V4a),ap(c_2Esptree_2ELS(A_27a),V3a_27)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V2k),c_2Enum_2E0)),ap(c_2Esptree_2ELS(A_27a),V4a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V2k)),ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V2k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V4a),c_2Esptree_2ELN(A_27a))),V3a_27),c_2Esptree_2ELN(A_27a))),ap(ap(ap(c_2Esptree_2EBS(A_27a),c_2Esptree_2ELN(A_27a)),V3a_27),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V2k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V4a),c_2Esptree_2ELN(A_27a))))) ) ) ) ) ) & ( ( ! [V5t2] : ( mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ! [V6t1] : ( mem(V6t1,ty_2Esptree_2Espt(A_27a)) => ! [V7k] : ( mem(V7k,ty_2Enum_2Enum) => ! [V8a] : ( mem(V8a,A_27a) => ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V7k),V8a),ap(ap(c_2Esptree_2EBN(A_27a),V6t1),V5t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V7k),c_2Enum_2E0)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V6t1),V8a),V5t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V7k)),ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V7k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V8a),V6t1)),V5t2)),ap(ap(c_2Esptree_2EBN(A_27a),V6t1),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V7k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V8a),V5t2)))) ) ) ) ) ) ) & ! [V9t2] : ( mem(V9t2,ty_2Esptree_2Espt(A_27a)) => ! [V10t1] : ( mem(V10t1,ty_2Esptree_2Espt(A_27a)) => ! [V11k] : ( mem(V11k,ty_2Enum_2Enum) => ! [V12a_27] : ( mem(V12a_27,A_27a) => ! [V13a] : ( mem(V13a,A_27a) => ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V11k),V13a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10t1),V12a_27),V9t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V11k),c_2Enum_2E0)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10t1),V13a),V9t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V11k)),ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V11k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V13a),V10t1)),V12a_27),V9t2)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10t1),V12a_27),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V11k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V13a),V9t2)))) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Emk__BN__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),bool))) => ( ( p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),c_2Esptree_2ELN(A_27a))) & ( ( ! [V1v14] : ( mem(V1v14,A_27a) => p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V1v14))) ) ) & ( ( ! [V2v15] : ( mem(V2v15,ty_2Esptree_2Espt(A_27a)) => ! [V3v16] : ( mem(V3v16,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),ap(ap(c_2Esptree_2EBN(A_27a),V2v15),V3v16))) ) ) ) & ( ( ! [V4v17] : ( mem(V4v17,ty_2Esptree_2Espt(A_27a)) => ! [V5v18] : ( mem(V5v18,A_27a) => ! [V6v19] : ( mem(V6v19,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V4v17),V5v18),V6v19))) ) ) ) ) & ( ( ! [V7v2] : ( mem(V7v2,A_27a) => ! [V8t2] : ( mem(V8t2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,ap(c_2Esptree_2ELS(A_27a),V7v2)),V8t2)) ) ) ) & ( ( ! [V9v3] : ( mem(V9v3,ty_2Esptree_2Espt(A_27a)) => ! [V10v4] : ( mem(V10v4,ty_2Esptree_2Espt(A_27a)) => ! [V11t2] : ( mem(V11t2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,ap(ap(c_2Esptree_2EBN(A_27a),V9v3),V10v4)),V11t2)) ) ) ) ) & ! [V12v5] : ( mem(V12v5,ty_2Esptree_2Espt(A_27a)) => ! [V13v6] : ( mem(V13v6,A_27a) => ! [V14v7] : ( mem(V14v7,ty_2Esptree_2Espt(A_27a)) => ! [V15t2] : ( mem(V15t2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,ap(ap(ap(c_2Esptree_2EBS(A_27a),V12v5),V13v6),V14v7)),V15t2)) ) ) ) ) ) ) ) ) ) ) => ! [V16v] : ( mem(V16v,ty_2Esptree_2Espt(A_27a)) => ! [V17v1] : ( mem(V17v1,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,V16v),V17v1)) ) ) ) )))).
fof(conj_thm_2Esptree_2Emk__BN__def,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v14] : ( mem(V0v14,A_27a) => ! [V1v15] : ( mem(V1v15,ty_2Esptree_2Espt(A_27a)) => ! [V2v16] : ( mem(V2v16,ty_2Esptree_2Espt(A_27a)) => ! [V3v17] : ( mem(V3v17,ty_2Esptree_2Espt(A_27a)) => ! [V4v18] : ( mem(V4v18,A_27a) => ! [V5v19] : ( mem(V5v19,ty_2Esptree_2Espt(A_27a)) => ! [V6v2] : ( mem(V6v2,A_27a) => ! [V7t2] : ( mem(V7t2,ty_2Esptree_2Espt(A_27a)) => ! [V8v3] : ( mem(V8v3,ty_2Esptree_2Espt(A_27a)) => ! [V9v4] : ( mem(V9v4,ty_2Esptree_2Espt(A_27a)) => ! [V10v5] : ( mem(V10v5,ty_2Esptree_2Espt(A_27a)) => ! [V11v6] : ( mem(V11v6,A_27a) => ! [V12v7] : ( mem(V12v7,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),c_2Esptree_2ELN(A_27a)) = c_2Esptree_2ELN(A_27a) ) & ( ( ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V0v14)) = ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V0v14)) ) & ( ( ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(c_2Esptree_2EBN(A_27a),V1v15),V2v16)) = ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(c_2Esptree_2EBN(A_27a),V1v15),V2v16)) ) & ( ( ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3v17),V4v18),V5v19)) = ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3v17),V4v18),V5v19)) ) & ( ( ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(c_2Esptree_2ELS(A_27a),V6v2)),V7t2) = ap(ap(c_2Esptree_2EBN(A_27a),ap(c_2Esptree_2ELS(A_27a),V6v2)),V7t2) ) & ( ( ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V8v3),V9v4)),V7t2) = ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V8v3),V9v4)),V7t2) ) & ( ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10v5),V11v6),V12v7)),V7t2) = ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10v5),V11v6),V12v7)),V7t2) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Emk__BS__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),bool)))) => ( ( ( ! [V1x] : ( mem(V1x,A_27a) => p(ap(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),V1x),c_2Esptree_2ELN(A_27a))) ) ) & ( ( ! [V2v16] : ( mem(V2v16,A_27a) => ! [V3x] : ( mem(V3x,A_27a) => p(ap(ap(ap(V0P,ap(c_2Esptree_2ELS(A_27a),V2v16)),V3x),c_2Esptree_2ELN(A_27a))) ) ) ) & ( ( ! [V4v17] : ( mem(V4v17,ty_2Esptree_2Espt(A_27a)) => ! [V5v18] : ( mem(V5v18,ty_2Esptree_2Espt(A_27a)) => ! [V6x] : ( mem(V6x,A_27a) => p(ap(ap(ap(V0P,ap(ap(c_2Esptree_2EBN(A_27a),V4v17),V5v18)),V6x),c_2Esptree_2ELN(A_27a))) ) ) ) ) & ( ( ! [V7v19] : ( mem(V7v19,ty_2Esptree_2Espt(A_27a)) => ! [V8v20] : ( mem(V8v20,A_27a) => ! [V9v21] : ( mem(V9v21,ty_2Esptree_2Espt(A_27a)) => ! [V10x] : ( mem(V10x,A_27a) => p(ap(ap(ap(V0P,ap(ap(ap(c_2Esptree_2EBS(A_27a),V7v19),V8v20),V9v21)),V10x),c_2Esptree_2ELN(A_27a))) ) ) ) ) ) & ( ( ! [V11t1] : ( mem(V11t1,ty_2Esptree_2Espt(A_27a)) => ! [V12x] : ( mem(V12x,A_27a) => ! [V13v4] : ( mem(V13v4,A_27a) => p(ap(ap(ap(V0P,V11t1),V12x),ap(c_2Esptree_2ELS(A_27a),V13v4))) ) ) ) ) & ( ( ! [V14t1] : ( mem(V14t1,ty_2Esptree_2Espt(A_27a)) => ! [V15x] : ( mem(V15x,A_27a) => ! [V16v5] : ( mem(V16v5,ty_2Esptree_2Espt(A_27a)) => ! [V17v6] : ( mem(V17v6,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V14t1),V15x),ap(ap(c_2Esptree_2EBN(A_27a),V16v5),V17v6))) ) ) ) ) ) & ! [V18t1] : ( mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ! [V19x] : ( mem(V19x,A_27a) => ! [V20v7] : ( mem(V20v7,ty_2Esptree_2Espt(A_27a)) => ! [V21v8] : ( mem(V21v8,A_27a) => ! [V22v9] : ( mem(V22v9,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V18t1),V19x),ap(ap(ap(c_2Esptree_2EBS(A_27a),V20v7),V21v8),V22v9))) ) ) ) ) ) ) ) ) ) ) ) => ! [V23v] : ( mem(V23v,ty_2Esptree_2Espt(A_27a)) => ! [V24v1] : ( mem(V24v1,A_27a) => ! [V25v2] : ( mem(V25v2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V23v),V24v1),V25v2)) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Emk__BS__def,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1v16] : ( mem(V1v16,A_27a) => ! [V2v17] : ( mem(V2v17,ty_2Esptree_2Espt(A_27a)) => ! [V3v18] : ( mem(V3v18,ty_2Esptree_2Espt(A_27a)) => ! [V4v19] : ( mem(V4v19,ty_2Esptree_2Espt(A_27a)) => ! [V5v20] : ( mem(V5v20,A_27a) => ! [V6v21] : ( mem(V6v21,ty_2Esptree_2Espt(A_27a)) => ! [V7t1] : ( mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ! [V8v4] : ( mem(V8v4,A_27a) => ! [V9v5] : ( mem(V9v5,ty_2Esptree_2Espt(A_27a)) => ! [V10v6] : ( mem(V10v6,ty_2Esptree_2Espt(A_27a)) => ! [V11v7] : ( mem(V11v7,ty_2Esptree_2Espt(A_27a)) => ! [V12v8] : ( mem(V12v8,A_27a) => ! [V13v9] : ( mem(V13v9,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),c_2Esptree_2ELN(A_27a)),V0x),c_2Esptree_2ELN(A_27a)) = ap(c_2Esptree_2ELS(A_27a),V0x) ) & ( ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(c_2Esptree_2ELS(A_27a),V1v16)),V0x),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(c_2Esptree_2ELS(A_27a),V1v16)),V0x),c_2Esptree_2ELN(A_27a)) ) & ( ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V2v17),V3v18)),V0x),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V2v17),V3v18)),V0x),c_2Esptree_2ELN(A_27a)) ) & ( ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V4v19),V5v20),V6v21)),V0x),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V4v19),V5v20),V6v21)),V0x),c_2Esptree_2ELN(A_27a)) ) & ( ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V0x),ap(c_2Esptree_2ELS(A_27a),V8v4)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V0x),ap(c_2Esptree_2ELS(A_27a),V8v4)) ) & ( ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V0x),ap(ap(c_2Esptree_2EBN(A_27a),V9v5),V10v6)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V0x),ap(ap(c_2Esptree_2EBN(A_27a),V9v5),V10v6)) ) & ( ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V0x),ap(ap(ap(c_2Esptree_2EBS(A_27a),V11v7),V12v8),V13v9)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V0x),ap(ap(ap(c_2Esptree_2EBS(A_27a),V11v7),V12v8),V13v9)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Esptree_2Edelete__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Edelete(A_27a),V0k),c_2Esptree_2ELN(A_27a)) = c_2Esptree_2ELN(A_27a) ) ) ) & ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,A_27a) => ( ap(ap(c_2Esptree_2Edelete(A_27a),V1k),ap(c_2Esptree_2ELS(A_27a),V2a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),c_2Enum_2E0)),c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V2a)) ) ) ) ) & ( ( ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ! [V4t1] : ( mem(V4t1,ty_2Esptree_2Espt(A_27a)) => ! [V5t2] : ( mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Edelete(A_27a),V3k),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V5t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V3k),c_2Enum_2E0)),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V5t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V3k)),ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V3k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V4t1)),V5t2)),ap(ap(c_2Esptree_2Emk__BN(A_27a),V4t1),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V3k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V5t2)))) ) ) ) ) ) & ! [V6k] : ( mem(V6k,ty_2Enum_2Enum) => ! [V7t1] : ( mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ! [V8a] : ( mem(V8a,A_27a) => ! [V9t2] : ( mem(V9t2,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Edelete(A_27a),V6k),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V8a),V9t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V6k),c_2Enum_2E0)),ap(ap(c_2Esptree_2EBN(A_27a),V7t1),V9t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,V6k)),ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V6k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V7t1)),V8a),V9t2)),ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V8a),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V6k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V9t2)))) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Esptree_2EfromList__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Esptree_2EfromList(A_27a),V0l) = ap(c_2Epair_2ESND(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),ap(ap(ap(c_2Elist_2EFOLDL(A_27a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a))),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a),arr(A_27a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)))),f2348(A_27a))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),c_2Enum_2E0),c_2Esptree_2ELN(A_27a))),V0l)) ) ) ) )).
fof(ax_thm_2Esptree_2Esize__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Esptree_2Esize(A_27a),c_2Esptree_2ELN(A_27a)) = c_2Enum_2E0 ) & ( ( ! [V0a] : ( mem(V0a,A_27a) => ( ap(c_2Esptree_2Esize(A_27a),ap(c_2Esptree_2ELS(A_27a),V0a)) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) & ( ( ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Esize(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Esptree_2Esize(A_27a),V1t1)),ap(c_2Esptree_2Esize(A_27a),V2t2)) ) ) ) ) & ! [V3t1] : ( mem(V3t1,ty_2Esptree_2Espt(A_27a)) => ! [V4a] : ( mem(V4a,A_27a) => ! [V5t2] : ( mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Esize(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3t1),V4a),V5t2)) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Esptree_2Esize(A_27a),V3t1)),ap(c_2Esptree_2Esize(A_27a),V5t2))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Einsert__notEmpty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ~~ ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1a),V2t) = c_2Esptree_2ELN(A_27a) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Ewf__insert,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),V2t)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1a),V2t))) ) ) ) )))).
fof(conj_thm_2Esptree_2Ewf__delete,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),V1k),V0t))) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__insert1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0k),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1a),V2t)) = ap(c_2Eoption_2ESOME(A_27a),V1a) ) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__insert,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k2] : ( mem(V0k2,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ! [V3k1] : ( mem(V3k1,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V3k1),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k2),V1v),V2t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V3k1),V0k2)),ap(c_2Eoption_2ESOME(A_27a),V1v)),ap(ap(c_2Esptree_2Elookup(A_27a),V3k1),V2t)) ) ) ) ) )))).
fof(ax_thm_2Esptree_2Eunion__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Eunion(A_27a),c_2Esptree_2ELN(A_27a)),V0t) = V0t ) ) ) & ( ( ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Eunion(A_27a),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V2t),ap(c_2Esptree_2ELS(A_27a),V1a)),k(A_27a,ap(c_2Esptree_2ELS(A_27a),V1a))),f2350(A_27a,V1a)),f2352(A_27a,V1a)) ) ) ) ) & ( ( ! [V9t1] : ( mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ! [V10t2] : ( mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ! [V11t] : ( mem(V11t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V11t),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),f2353(A_27a,V9t1,V10t2)),f2355(A_27a,V9t1,V10t2)),f2358(A_27a,V9t1,V10t2)) ) ) ) ) ) & ! [V18t1] : ( mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ! [V19a] : ( mem(V19a,A_27a) => ! [V20t2] : ( mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ! [V21t] : ( mem(V21t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V21t),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),k(A_27a,ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2))),f2360(A_27a,V19a,V18t1,V20t2)),f2362(A_27a,V19a,V18t1,V20t2)) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2EisEmpty__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(c_2Esptree_2Eunion(A_27a),V0m1),V1m2) = c_2Esptree_2ELN(A_27a) ) <=> ( ( V0m1 = c_2Esptree_2ELN(A_27a) ) & ( V1m2 = c_2Esptree_2ELN(A_27a) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Ewf__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ( ( p(ap(c_2Esptree_2Ewf(A_27a),V0m1)) & p(ap(c_2Esptree_2Ewf(A_27a),V1m2)) ) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2Eunion(A_27a),V0m1),V1m2))) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V2k),ap(ap(c_2Esptree_2Eunion(A_27a),V0m1),V1m2)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),V2k),V0m1)),ap(ap(c_2Esptree_2Elookup(A_27a),V2k),V1m2)),f1905(A_27a)) ) ) ) )))).
fof(ax_thm_2Esptree_2Einter__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),c_2Esptree_2ELN(A_27a)),V0t) = c_2Esptree_2ELN(A_27a) ) ) ) & ( ( ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V2t),c_2Esptree_2ELN(A_27a)),k(A_27b,ap(c_2Esptree_2ELS(A_27a),V1a))),k(ty_2Esptree_2Espt(A_27b),k(ty_2Esptree_2Espt(A_27b),c_2Esptree_2ELN(A_27a)))),k(ty_2Esptree_2Espt(A_27b),k(A_27b,k(ty_2Esptree_2Espt(A_27b),ap(c_2Esptree_2ELS(A_27a),V1a))))) ) ) ) ) & ( ( ! [V9t1] : ( mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ! [V10t2] : ( mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ! [V11t] : ( mem(V11t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V11t),c_2Esptree_2ELN(A_27a)),k(A_27b,c_2Esptree_2ELN(A_27a))),f2364(A_27a,A_27b,V9t1,V10t2)),f2366(A_27a,A_27b,V9t1,V10t2)) ) ) ) ) ) & ! [V18t1] : ( mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ! [V19a] : ( mem(V19a,A_27a) => ! [V20t2] : ( mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ! [V21t] : ( mem(V21t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V21t),c_2Esptree_2ELN(A_27a)),k(A_27b,ap(c_2Esptree_2ELS(A_27a),V19a))),f2368(A_27a,A_27b,V18t1,V20t2)),f2370(A_27a,A_27b,V19a,V18t1,V20t2)) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Esptree_2Einter__eq__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Einter__eq(A_27a),c_2Esptree_2ELN(A_27a)),V0t) = c_2Esptree_2ELN(A_27a) ) ) ) & ( ( ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Einter__eq(A_27a),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V2t),c_2Esptree_2ELN(A_27a)),f2371(A_27a,V1a)),k(ty_2Esptree_2Espt(A_27a),k(ty_2Esptree_2Espt(A_27a),c_2Esptree_2ELN(A_27a)))),k(ty_2Esptree_2Espt(A_27a),f2372(A_27a,V1a))) ) ) ) ) & ( ( ! [V9t1] : ( mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ! [V10t2] : ( mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ! [V11t] : ( mem(V11t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Einter__eq(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V11t),c_2Esptree_2ELN(A_27a)),k(A_27a,c_2Esptree_2ELN(A_27a))),f2374(A_27a,V9t1,V10t2)),f2376(A_27a,V9t1,V10t2)) ) ) ) ) ) & ! [V18t1] : ( mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ! [V19a] : ( mem(V19a,A_27a) => ! [V20t2] : ( mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ! [V21t] : ( mem(V21t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Einter__eq(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V21t),c_2Esptree_2ELN(A_27a)),f2377(A_27a,V19a)),f2379(A_27a,V18t1,V20t2)),f2382(A_27a,V19a,V18t1,V20t2)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Esptree_2Edifference__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),c_2Esptree_2ELN(A_27a)),V0t) = c_2Esptree_2ELN(A_27a) ) ) ) & ( ( ! [V1a] : ( mem(V1a,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V2t),ap(c_2Esptree_2ELS(A_27a),V1a)),k(A_27b,c_2Esptree_2ELN(A_27a))),k(ty_2Esptree_2Espt(A_27b),k(ty_2Esptree_2Espt(A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)))),k(ty_2Esptree_2Espt(A_27b),k(A_27b,k(ty_2Esptree_2Espt(A_27b),c_2Esptree_2ELN(A_27a))))) ) ) ) ) & ( ( ! [V9t1] : ( mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ! [V10t2] : ( mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ! [V11t] : ( mem(V11t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V11t),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),k(A_27b,ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2))),f2384(A_27a,A_27b,V9t1,V10t2)),f2386(A_27a,A_27b,V9t1,V10t2)) ) ) ) ) ) & ! [V18t1] : ( mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ! [V19a] : ( mem(V19a,A_27a) => ! [V20t2] : ( mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ! [V21t] : ( mem(V21t,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V21t),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),k(A_27b,ap(ap(c_2Esptree_2EBN(A_27a),V18t1),V20t2))),f2388(A_27a,A_27b,V19a,V18t1,V20t2)),f2390(A_27a,A_27b,V18t1,V20t2)) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Ewf__inter,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27b)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0m1),V1m2))) ) ))))).
fof(conj_thm_2Esptree_2Elookup__inter,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27b)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V2k),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0m1),V1m2)) = ap(ap(c_2Epair_2Epair__CASE(ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Epair_2E_2C(ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Esptree_2Elookup(A_27a),V2k),V0m1)),ap(ap(c_2Esptree_2Elookup(A_27b),V2k),V1m2))),f2393(A_27b,A_27a)) ) ) ) ))))).
fof(conj_thm_2Esptree_2Elookup__inter__eq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V2k),ap(ap(c_2Esptree_2Einter__eq(A_27a),V0m1),V1m2)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),V2k),V0m1)),c_2Eoption_2ENONE(A_27a)),f2394(A_27a,V1m2,V2k)) ) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__inter__EQ,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27b)) => ! [V3y] : ( mem(V3y,A_27a) => ( ( ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)) = ap(c_2Eoption_2ESOME(A_27a),V3y) ) <=> ( ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),V1t1) = ap(c_2Eoption_2ESOME(A_27a),V3y) ) & ( ~~ ( ap(ap(c_2Esptree_2Elookup(A_27b),V0x),V2t2) = c_2Eoption_2ENONE(A_27b) ) ) ) ) & ( ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)) = c_2Eoption_2ENONE(A_27a) ) <=> ( ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),V1t1) = c_2Eoption_2ENONE(A_27a) ) | ( ap(ap(c_2Esptree_2Elookup(A_27b),V0x),V2t2) = c_2Eoption_2ENONE(A_27b) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Esptree_2Elookup__inter__assoc,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27b)) => ! [V3t3] : ( mem(V3t3,ty_2Esptree_2Espt(A_27c)) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),ap(ap(c_2Esptree_2Einter(A_27b,A_27c),V2t2),V3t3))) = ap(ap(c_2Esptree_2Elookup(A_27a),V0x),ap(ap(c_2Esptree_2Einter(A_27a,A_27c),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)),V3t3)) ) ) ) ) )))))).
fof(conj_thm_2Esptree_2Elookup__difference,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0m1] : ( mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ! [V1m2] : ( mem(V1m2,ty_2Esptree_2Espt(A_27b)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V2k),ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),V0m1),V1m2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Esptree_2Elookup(A_27b),V2k),V1m2)),c_2Eoption_2ENONE(A_27b))),ap(ap(c_2Esptree_2Elookup(A_27a),V2k),V0m1)),c_2Eoption_2ENONE(A_27a)) ) ) ) ))))).
fof(ax_thm_2Esptree_2Elrnext__primitive__def,axiom, ( c_2Esptree_2Elrnext = ap(ap(c_2Erelation_2EWFREC(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Emin_2E_40(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),f2396)),f2398) )).
fof(conj_thm_2Esptree_2Elrnext__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ( ~~ ( V1n = c_2Enum_2E0 ) ) => p(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V1n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) => p(ap(V0P,V1n)) ) ) ) => ! [V2v] : ( mem(V2v,ty_2Enum_2Enum) => p(ap(V0P,V2v)) ) ) ))).
fof(conj_thm_2Esptree_2Elrnext__def,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Esptree_2Elrnext,V0n) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V0n),c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ))).
fof(conj_thm_2Esptree_2Elrnext__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0a] : ( mem(V0a,A_27a) => ( ap(c_2Esptree_2Elrnext,c_2Enum_2E0) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,A_27b) => ( ap(c_2Esptree_2Elrnext,ap(c_2Earithmetic_2ENUMERAL,V1n)) = ap(c_2Esptree_2Elrnext,V1n) ) ) ) ) & ( ( ap(c_2Esptree_2Elrnext,c_2Earithmetic_2EZERO) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) & ( ( ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ap(c_2Esptree_2Elrnext,ap(c_2Earithmetic_2EBIT1,V3n)) = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V3n)) ) ) ) & ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( ap(c_2Esptree_2Elrnext,ap(c_2Earithmetic_2EBIT2,V4n)) = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V4n)) ) ) ) ) ) ))))).
fof(ax_thm_2Esptree_2Edomain__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Esptree_2Edomain(A_27a),c_2Esptree_2ELN(A_27a)) = c_2Epred__set_2EEMPTY(ty_2Enum_2Enum) ) & ( ( ! [V0v0] : ( mem(V0v0,A_27a) => ( ap(c_2Esptree_2Edomain(A_27a),ap(c_2Esptree_2ELS(A_27a),V0v0)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),c_2Enum_2E0),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) ) ) ) & ( ( ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2399),ap(c_2Esptree_2Edomain(A_27a),V1t1))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2400),ap(c_2Esptree_2Edomain(A_27a),V2t2))) ) ) ) ) & ! [V5t1] : ( mem(V5t1,ty_2Esptree_2Espt(A_27a)) => ! [V6v1] : ( mem(V6v1,A_27a) => ! [V7t2] : ( mem(V7t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V5t1),V6v1),V7t2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),c_2Enum_2E0),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2401),ap(c_2Esptree_2Edomain(A_27a),V5t1)))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2402),ap(c_2Esptree_2Edomain(A_27a),V7t2))) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2EFINITE__domain,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t))) )))).
fof(conj_thm_2Esptree_2Esize__insert,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,A_27a) => ! [V2m] : ( mem(V2m,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Esize(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1v),V2m)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0k),ap(c_2Esptree_2Edomain(A_27a),V2m))),ap(c_2Esptree_2Esize(A_27a),V2m)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Esptree_2Esize(A_27a),V2m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__fromList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0n),ap(c_2Esptree_2EfromList(A_27a),V1l)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))),ap(c_2Eoption_2ESOME(A_27a),ap(ap(c_2Elist_2EEL(A_27a),V0n),V1l))),c_2Eoption_2ENONE(A_27a)) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__lookup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1k),ap(c_2Esptree_2Edomain(A_27a),V0t))) <=> ? [V2v] : ( mem(V2v,A_27a) & ( ap(ap(c_2Esptree_2Elookup(A_27a),V1k),V0t) = ap(c_2Eoption_2ESOME(A_27a),V2v) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Elookup__inter__alt,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0x),ap(c_2Esptree_2Edomain(A_27b),V2t2))),ap(ap(c_2Esptree_2Elookup(A_27a),V0x),V1t1)),c_2Eoption_2ENONE(A_27a)) ) ) ) ))))).
fof(conj_thm_2Esptree_2Elookup__NONE__domain,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(c_2Esptree_2Elookup(A_27a),V0k),V1t) = c_2Eoption_2ENONE(A_27a) ) <=> ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0k),ap(c_2Esptree_2Edomain(A_27a),V1t))) ) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Eunion(A_27a),V0t1),V1t2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t1)),ap(c_2Esptree_2Edomain(A_27a),V1t2)) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__inter,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27b)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0t1),V1t2)) = ap(ap(c_2Epred__set_2EINTER(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t1)),ap(c_2Esptree_2Edomain(A_27b),V1t2)) ) ) ))))).
fof(conj_thm_2Esptree_2Edomain__insert,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1v),V2t)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),V0k),ap(c_2Esptree_2Edomain(A_27a),V2t)) ) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__difference,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27b)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),V0t1),V1t2)) = ap(ap(c_2Epred__set_2EDIFF(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t1)),ap(c_2Esptree_2Edomain(A_27b),V1t2)) ) ) ))))).
fof(conj_thm_2Esptree_2Edomain__sing,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,A_27a) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1v),c_2Esptree_2ELN(A_27a))) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),V0k),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__fromList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(c_2Esptree_2EfromList(A_27a),V0l)) = ap(c_2Epred__set_2Ecount,ap(c_2Elist_2ELENGTH(A_27a),V0l)) ) )))).
fof(conj_thm_2Esptree_2Elookup__delete,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1k1] : ( mem(V1k1,ty_2Enum_2Enum) => ! [V2k2] : ( mem(V2k2,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V1k1),ap(ap(c_2Esptree_2Edelete(A_27a),V2k2),V0t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k1),V2k2)),c_2Eoption_2ENONE(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),V1k1),V0t)) ) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__delete,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),V0k),V1t)) = ap(ap(c_2Epred__set_2EDELETE(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V1t)),V0k) ) ) )))).
fof(ax_thm_2Esptree_2Efoldi__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2acc] : ( mem(V2acc,A_27a) => ( ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V0f),V1i),V2acc),c_2Esptree_2ELN(A_27b)) = V2acc ) ) ) ) ) & ( ( ! [V3f] : ( mem(V3f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ! [V4i] : ( mem(V4i,ty_2Enum_2Enum) => ! [V5acc] : ( mem(V5acc,A_27a) => ! [V6a] : ( mem(V6a,A_27b) => ( ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V3f),V4i),V5acc),ap(c_2Esptree_2ELS(A_27b),V6a)) = ap(ap(ap(V3f,V4i),V6a),V5acc) ) ) ) ) ) ) & ( ( ! [V7f] : ( mem(V7f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ! [V8i] : ( mem(V8i,ty_2Enum_2Enum) => ! [V9acc] : ( mem(V9acc,A_27a) => ! [V10t1] : ( mem(V10t1,ty_2Esptree_2Espt(A_27b)) => ! [V11t2] : ( mem(V11t2,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V7f),V8i),V9acc),ap(ap(c_2Esptree_2EBN(A_27b),V10t1),V11t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,A_27a),f2403(A_27a,A_27b,V7f,V8i,V9acc,V10t1,V11t2)),ap(c_2Esptree_2Elrnext,V8i)) ) ) ) ) ) ) ) & ! [V13f] : ( mem(V13f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ! [V14i] : ( mem(V14i,ty_2Enum_2Enum) => ! [V15acc] : ( mem(V15acc,A_27a) => ! [V16t1] : ( mem(V16t1,ty_2Esptree_2Espt(A_27b)) => ! [V17a] : ( mem(V17a,A_27b) => ! [V18t2] : ( mem(V18t2,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V13f),V14i),V15acc),ap(ap(ap(c_2Esptree_2EBS(A_27b),V16t1),V17a),V18t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,A_27a),f2404(A_27a,A_27b,V13f,V14i,V16t1,V15acc,V17a,V18t2)),ap(c_2Esptree_2Elrnext,V14i)) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Espt__acc__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) => ( ( ( ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => p(ap(ap(V0P,V1i),c_2Enum_2E0)) ) ) & ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ( p(ap(ap(V0P,ap(ap(c_2Earithmetic_2E_2B,V2i),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Enum_2ESUC,V3k))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V2i))),ap(c_2Esptree_2Elrnext,V2i)))),ap(ap(c_2Earithmetic_2EDIV,V3k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) => p(ap(ap(V0P,V2i),ap(c_2Enum_2ESUC,V3k))) ) ) ) ) => ! [V4v] : ( mem(V4v,ty_2Enum_2Enum) => ! [V5v1] : ( mem(V5v1,ty_2Enum_2Enum) => p(ap(ap(V0P,V4v),V5v1)) ) ) ) ))).
fof(conj_thm_2Esptree_2Espt__acc__def,lemma,(( ( ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V0i),c_2Enum_2E0) = V0i ) ) ) & ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V2i),ap(c_2Enum_2ESUC,V1k)) = ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,V2i),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Enum_2ESUC,V1k))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V2i))),ap(c_2Esptree_2Elrnext,V2i)))),ap(ap(c_2Earithmetic_2EDIV,V1k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ) ) ))).
fof(conj_thm_2Esptree_2Espt__acc__def__compute,lemma,(( ( ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V0i),c_2Enum_2E0) = V0i ) ) ) & ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V2i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1k))) = ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,V2i),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1k)))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V2i))),ap(c_2Esptree_2Elrnext,V2i)))),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1k))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ) ) ) & ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ! [V4i] : ( mem(V4i,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V4i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3k))) = ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,V4i),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3k)))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V4i))),ap(c_2Esptree_2Elrnext,V4i)))),ap(ap(c_2Earithmetic_2EDIV,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3k))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ) ) ) ))).
fof(conj_thm_2Esptree_2Espt__acc__thm,lemma,(! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V0i),V1k) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),c_2Enum_2E0)),V0i),ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,V0i),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,V1k)),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Esptree_2Elrnext,V0i))),ap(c_2Esptree_2Elrnext,V0i)))),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,V1k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Esptree_2Espt__acc__eqn,lemma,(! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,V1i),V0k) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Esptree_2Elrnext,V1i)),V0k)),V1i) ) ) ))).
fof(conj_thm_2Esptree_2Espt__acc__0,lemma,(! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Espt__acc,c_2Enum_2E0),V0k) = V0k ) ))).
fof(conj_thm_2Esptree_2Eset__foldi__keys,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1a] : ( mem(V1a,arr(ty_2Enum_2Enum,bool)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( ap(ap(ap(ap(c_2Esptree_2Efoldi(arr(ty_2Enum_2Enum,bool),A_27a),f2406),V2i),V1a),V0t) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),V1a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2407(V2i)),ap(c_2Esptree_2Edomain(A_27a),V0t))) ) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__foldi,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),V0t) = ap(ap(ap(ap(c_2Esptree_2Efoldi(arr(ty_2Enum_2Enum,bool),A_27a),f2409),c_2Enum_2E0),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)),V0t) ) )))).
fof(ax_thm_2Esptree_2Emapi0__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V0f),V1i),c_2Esptree_2ELN(A_27b)) = c_2Esptree_2ELN(A_27a) ) ) ) ) & ( ( ! [V2f] : ( mem(V2f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ! [V3i] : ( mem(V3i,ty_2Enum_2Enum) => ! [V4a] : ( mem(V4a,A_27b) => ( ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V2f),V3i),ap(c_2Esptree_2ELS(A_27b),V4a)) = ap(c_2Esptree_2ELS(A_27a),ap(ap(V2f,V3i),V4a)) ) ) ) ) ) & ( ( ! [V5f] : ( mem(V5f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ! [V6i] : ( mem(V6i,ty_2Enum_2Enum) => ! [V7t1] : ( mem(V7t1,ty_2Esptree_2Espt(A_27b)) => ! [V8t2] : ( mem(V8t2,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V5f),V6i),ap(ap(c_2Esptree_2EBN(A_27b),V7t1),V8t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),f2410(A_27a,A_27b,V7t1,V5f,V6i,V8t2)),ap(c_2Esptree_2Elrnext,V6i)) ) ) ) ) ) ) & ! [V10f] : ( mem(V10f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ! [V11i] : ( mem(V11i,ty_2Enum_2Enum) => ! [V12t1] : ( mem(V12t1,ty_2Esptree_2Espt(A_27b)) => ! [V13a] : ( mem(V13a,A_27b) => ! [V14t2] : ( mem(V14t2,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V10f),V11i),ap(ap(ap(c_2Esptree_2EBS(A_27b),V12t1),V13a),V14t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),f2411(A_27a,A_27b,V13a,V12t1,V10f,V11i,V14t2)),ap(c_2Esptree_2Elrnext,V11i)) ) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Esptree_2Emapi__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ! [V1pt] : ( mem(V1pt,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Emapi(A_27a,A_27b),V0f),V1pt) = ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V0f),c_2Enum_2E0),V1pt) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Elookup__mapi0,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V1pt] : ( mem(V1pt,ty_2Esptree_2Espt(A_27a)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27b),V3k),ap(ap(ap(c_2Esptree_2Emapi0(A_27b,A_27a),V0f),V2i),V1pt)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Esptree_2Elookup(A_27a),V3k),V1pt)),c_2Eoption_2ENONE(A_27b)),f2412(A_27a,A_27b,V3k,V2i,V0f)) ) ) ) ) ))))).
fof(conj_thm_2Esptree_2Elookup__mapi,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ! [V2pt] : ( mem(V2pt,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0k),ap(ap(c_2Esptree_2Emapi(A_27a,A_27b),V1f),V2pt)) = ap(ap(c_2Eoption_2EOPTION__MAP(A_27b,A_27a),ap(V1f,V0k)),ap(ap(c_2Esptree_2Elookup(A_27b),V0k),V2pt)) ) ) ) ))))).
fof(ax_thm_2Esptree_2EtoAList__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Esptree_2EtoAList(A_27a) = ap(ap(ap(c_2Esptree_2Efoldi(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),A_27a),f2415(A_27a)),c_2Enum_2E0),c_2Elist_2ENIL(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a))) ) ) )).
fof(conj_thm_2Esptree_2EMEM__toAList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2v)),ap(c_2Elist_2ELIST__TO__SET(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ap(c_2Esptree_2EtoAList(A_27a),V0t)))) <=> ( ap(ap(c_2Esptree_2Elookup(A_27a),V1k),V0t) = ap(c_2Eoption_2ESOME(A_27a),V2v) ) ) ) ) )))).
fof(conj_thm_2Esptree_2EALOOKUP__toAList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Enum_2Enum) => ( ap(ap(c_2Ealist_2EALOOKUP(A_27a,ty_2Enum_2Enum),ap(c_2Esptree_2EtoAList(A_27a),V0t)),V1x) = ap(ap(c_2Esptree_2Elookup(A_27a),V1x),V0t) ) ) )))).
fof(conj_thm_2Esptree_2Einsert__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,A_27a) => ! [V2s] : ( mem(V2s,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1v),V2s) = ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0k),V1v),c_2Esptree_2ELN(A_27a))),V2s) ) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__empty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ( ( V0t = c_2Esptree_2ELN(A_27a) ) <=> ( ap(c_2Esptree_2Edomain(A_27a),V0t) = c_2Epred__set_2EEMPTY(ty_2Enum_2Enum) ) ) ) )))).
fof(conj_thm_2Esptree_2EALL__DISTINCT__MAP__FST__toAList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => p(ap(c_2Elist_2EALL__DISTINCT(ty_2Enum_2Enum),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),ty_2Enum_2Enum),c_2Epair_2EFST(ty_2Enum_2Enum,A_27a)),ap(c_2Esptree_2EtoAList(A_27a),V0t)))) )))).
fof(conj_thm_2Esptree_2Efoldi__FOLDR__toAList,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(A_27a,arr(A_27b,A_27b)))) => ! [V1a] : ( mem(V1a,A_27b) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27b,A_27a),V0f),c_2Enum_2E0),V1a),V2t) = ap(ap(ap(c_2Elist_2EFOLDR(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),A_27b),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,A_27a,arr(A_27b,A_27b)),V0f)),V1a),ap(c_2Esptree_2EtoAList(A_27a),V2t)) ) ) ) ))))).
fof(ax_thm_2Esptree_2EtoListA__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0acc] : ( mem(V0acc,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Esptree_2EtoListA(A_27a),V0acc),c_2Esptree_2ELN(A_27a)) = V0acc ) ) ) & ( ( ! [V1acc] : ( mem(V1acc,ty_2Elist_2Elist(A_27a)) => ! [V2a] : ( mem(V2a,A_27a) => ( ap(ap(c_2Esptree_2EtoListA(A_27a),V1acc),ap(c_2Esptree_2ELS(A_27a),V2a)) = ap(ap(c_2Elist_2ECONS(A_27a),V2a),V1acc) ) ) ) ) & ( ( ! [V3acc] : ( mem(V3acc,ty_2Elist_2Elist(A_27a)) => ! [V4t1] : ( mem(V4t1,ty_2Esptree_2Espt(A_27a)) => ! [V5t2] : ( mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2EtoListA(A_27a),V3acc),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V5t2)) = ap(ap(c_2Esptree_2EtoListA(A_27a),ap(ap(c_2Esptree_2EtoListA(A_27a),V3acc),V5t2)),V4t1) ) ) ) ) ) & ! [V6acc] : ( mem(V6acc,ty_2Elist_2Elist(A_27a)) => ! [V7t1] : ( mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ! [V8a] : ( mem(V8a,A_27a) => ! [V9t2] : ( mem(V9t2,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2EtoListA(A_27a),V6acc),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V8a),V9t2)) = ap(ap(c_2Esptree_2EtoListA(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V8a),ap(ap(c_2Esptree_2EtoListA(A_27a),V6acc),V9t2))),V7t1) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2EtoListA__append,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1acc] : ( mem(V1acc,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Esptree_2EtoListA(A_27a),V1acc),V0t) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Esptree_2EtoListA(A_27a),c_2Elist_2ENIL(A_27a)),V0t)),V1acc) ) ) )))).
fof(conj_thm_2Esptree_2EisEmpty__toListA,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ! [V1acc] : ( mem(V1acc,ty_2Elist_2Elist(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ( ( V0t = c_2Esptree_2ELN(A_27a) ) <=> ( ap(ap(c_2Esptree_2EtoListA(A_27a),V1acc),V0t) = V1acc ) ) ) ) )))).
fof(ax_thm_2Esptree_2EtoList__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2EtoList(A_27a),V0m) = ap(ap(c_2Esptree_2EtoListA(A_27a),c_2Elist_2ENIL(A_27a)),V0m) ) ) ) )).
fof(conj_thm_2Esptree_2EisEmpty__toList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ( ( V0t = c_2Esptree_2ELN(A_27a) ) <=> ( ap(c_2Esptree_2EtoList(A_27a),V0t) = c_2Elist_2ENIL(A_27a) ) ) ) )))).
fof(conj_thm_2Esptree_2EMEM__toList,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1t] : ( mem(V1t,ty_2Esptree_2Espt(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(c_2Esptree_2EtoList(A_27a),V1t)))) <=> ? [V2k] : ( mem(V2k,ty_2Enum_2Enum) & ( ap(ap(c_2Esptree_2Elookup(A_27a),V2k),V1t) = ap(c_2Eoption_2ESOME(A_27a),V0x) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Espt__eq__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ( ( p(ap(c_2Esptree_2Ewf(A_27a),V0t1)) & p(ap(c_2Esptree_2Ewf(A_27a),V1t2)) ) => ( ( V0t1 = V1t2 ) <=> ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V2n),V0t1) = ap(ap(c_2Esptree_2Elookup(A_27a),V2n),V1t2) ) ) ) ) ) )))).
fof(ax_thm_2Esptree_2Emk__wf__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Esptree_2Emk__wf(A_27a),c_2Esptree_2ELN(A_27a)) = c_2Esptree_2ELN(A_27a) ) & ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Esptree_2Emk__wf(A_27a),ap(c_2Esptree_2ELS(A_27a),V0x)) = ap(c_2Esptree_2ELS(A_27a),V0x) ) ) ) & ( ( ! [V1t1] : ( mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ! [V2t2] : ( mem(V2t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2)) = ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V1t1)),ap(c_2Esptree_2Emk__wf(A_27a),V2t2)) ) ) ) ) & ! [V3t1] : ( mem(V3t1,ty_2Esptree_2Espt(A_27a)) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5t2] : ( mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3t1),V4x),V5t2)) = ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V3t1)),V4x),ap(c_2Esptree_2Emk__wf(A_27a),V5t2)) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Esptree_2Ewf__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V0t))) )))).
fof(conj_thm_2Esptree_2Ewf__mk__id,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ( ap(c_2Esptree_2Emk__wf(A_27a),V0t) = V0t ) ) )))).
fof(conj_thm_2Esptree_2Elookup__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V0x),ap(c_2Esptree_2Emk__wf(A_27a),V1t)) = ap(ap(c_2Esptree_2Elookup(A_27a),V0x),V1t) ) ) )))).
fof(conj_thm_2Esptree_2Edomain__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ap(c_2Esptree_2Edomain(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V0t)) = ap(c_2Esptree_2Edomain(A_27a),V0t) ) )))).
fof(conj_thm_2Esptree_2Emk__wf__eq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ( ( ap(c_2Esptree_2Emk__wf(A_27a),V0t1) = ap(c_2Esptree_2Emk__wf(A_27a),V1t2) ) <=> ! [V2x] : ( mem(V2x,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V2x),V0t1) = ap(ap(c_2Esptree_2Elookup(A_27a),V2x),V1t2) ) ) ) ) )))).
fof(conj_thm_2Esptree_2Einter__eq,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27b)) => ! [V2t3] : ( mem(V2t3,ty_2Esptree_2Espt(A_27a)) => ! [V3t4] : ( mem(V3t4,ty_2Esptree_2Espt(A_27c)) => ( ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0t1),V1t2) = ap(ap(c_2Esptree_2Einter(A_27a,A_27c),V2t3),V3t4) ) <=> ! [V4x] : ( mem(V4x,ty_2Enum_2Enum) => ( ap(ap(c_2Esptree_2Elookup(A_27a),V4x),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0t1),V1t2)) = ap(ap(c_2Esptree_2Elookup(A_27a),V4x),ap(ap(c_2Esptree_2Einter(A_27a,A_27c),V2t3),V3t4)) ) ) ) ) ) ) )))))).
fof(conj_thm_2Esptree_2Eunion__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Eunion(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V0t1)),ap(c_2Esptree_2Emk__wf(A_27a),V1t2)) = ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(c_2Esptree_2Eunion(A_27a),V0t1),V1t2)) ) ) )))).
fof(conj_thm_2Esptree_2Einter__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27b)) => ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(c_2Esptree_2Emk__wf(A_27a),V0t1)),ap(c_2Esptree_2Emk__wf(A_27b),V1t2)) = ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0t1),V1t2)) ) ) ))))).
fof(conj_thm_2Esptree_2Einsert__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,A_27a) => ! [V2t] : ( mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0x),V1v),ap(c_2Esptree_2Emk__wf(A_27a),V2t)) = ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),V0x),V1v),V2t)) ) ) ) )))).
fof(conj_thm_2Esptree_2Edelete__mk__wf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Edelete(A_27a),V0x),ap(c_2Esptree_2Emk__wf(A_27a),V1t)) = ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),V0x),V1t)) ) ) )))).
fof(conj_thm_2Esptree_2Eunion__LN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(c_2Esptree_2Eunion(A_27a),V0t),c_2Esptree_2ELN(A_27a)) = V0t ) & ( ap(ap(c_2Esptree_2Eunion(A_27a),c_2Esptree_2ELN(A_27a)),V0t) = V0t ) ) )))).
fof(conj_thm_2Esptree_2Einter__LN,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0t] : ( mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ( ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0t),c_2Esptree_2ELN(A_27b)) = c_2Esptree_2ELN(A_27a) ) & ( ap(ap(c_2Esptree_2Einter(A_27c,A_27a),c_2Esptree_2ELN(A_27c)),V0t) = c_2Esptree_2ELN(A_27c) ) ) )))))).
fof(conj_thm_2Esptree_2Eunion__assoc,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0t1] : ( mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ! [V2t3] : ( mem(V2t3,ty_2Esptree_2Espt(A_27a)) => ( ap(ap(c_2Esptree_2Eunion(A_27a),V0t1),ap(ap(c_2Esptree_2Eunion(A_27a),V1t2),V2t3)) = ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(c_2Esptree_2Eunion(A_27a),V0t1),V1t2)),V2t3) ) ) ) )))).
