include('Axioms/veblen+2.ax').
fof(ne_ty_2Epatricia_2Eptree,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Epatricia_2Eptree(A0)) ) )).
fof(mem_c_2Epatricia_2EADD,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EADD(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),ty_2Epatricia_2Eptree(A_27a)))) ) )).
fof(mem_c_2Epatricia_2EADD__LIST,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EADD__LIST(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ty_2Epatricia_2Eptree(A_27a)))) ) )).
fof(mem_c_2Epatricia_2EBRANCH,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EBRANCH(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),ty_2Epatricia_2Eptree(A_27a))) ) )).
fof(mem_c_2Epatricia_2EBRANCHING__BIT,axiom,( mem(c_2Epatricia_2EBRANCHING__BIT,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Epatricia_2EBranch,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EBranch(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))))) ) )).
fof(mem_c_2Epatricia_2EDEPTH,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EDEPTH(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Epatricia_2EEVERY__LEAF,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EEVERY__LEAF(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Epatricia_2Eptree(A_27a),bool))) ) )).
fof(mem_c_2Epatricia_2EEXISTS__LEAF,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EEXISTS__LEAF(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Epatricia_2Eptree(A_27a),bool))) ) )).
fof(mem_c_2Epatricia_2EEmpty,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EEmpty(A_27a),ty_2Epatricia_2Eptree(A_27a)) ) )).
fof(mem_c_2Epatricia_2EFIND,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EFIND(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,A_27a))) ) )).
fof(mem_c_2Epatricia_2EINSERT__PTREE,axiom,( mem(c_2Epatricia_2EINSERT__PTREE,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),ty_2Epatricia_2Eptree(ty_2Eone_2Eone)))) )).
fof(mem_c_2Epatricia_2EIN__PTREE,axiom,( mem(c_2Epatricia_2EIN__PTREE,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),bool))) )).
fof(mem_c_2Epatricia_2EIS__EMPTY,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EIS__EMPTY(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),bool)) ) )).
fof(mem_c_2Epatricia_2EIS__PTREE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EIS__PTREE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),bool)) ) )).
fof(mem_c_2Epatricia_2EJOIN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EJOIN(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)))),ty_2Epatricia_2Eptree(A_27a))) ) )).
fof(mem_c_2Epatricia_2EKEYS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EKEYS(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))) ) )).
fof(mem_c_2Epatricia_2ELeaf,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2ELeaf(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,ty_2Epatricia_2Eptree(A_27a)))) ) )).
fof(mem_c_2Epatricia_2ENUMSET__OF__PTREE,axiom,( mem(c_2Epatricia_2ENUMSET__OF__PTREE,arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),arr(ty_2Enum_2Enum,bool))) )).
fof(mem_c_2Epatricia_2EPEEK,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EPEEK(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,ty_2Eoption_2Eoption(A_27a)))) ) )).
fof(mem_c_2Epatricia_2EPTREE__OF__NUMSET,axiom,( mem(c_2Epatricia_2EPTREE__OF__NUMSET,arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),arr(arr(ty_2Enum_2Enum,bool),ty_2Epatricia_2Eptree(ty_2Eone_2Eone)))) )).
fof(mem_c_2Epatricia_2EREMOVE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2EREMOVE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)))) ) )).
fof(mem_c_2Epatricia_2ESIZE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2ESIZE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Epatricia_2ETRANSFORM,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),arr(arr(A_27b,A_27a),arr(ty_2Epatricia_2Eptree(A_27b),ty_2Epatricia_2Eptree(A_27a)))) ) ) )).
fof(mem_c_2Epatricia_2ETRAVERSE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2ETRAVERSE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))) ) )).
fof(mem_c_2Epatricia_2ETRAVERSE__AUX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2ETRAVERSE__AUX(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Elist_2Elist(ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Epatricia_2EUNION__PTREE,axiom,( mem(c_2Epatricia_2EUNION__PTREE,arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),ty_2Epatricia_2Eptree(ty_2Eone_2Eone)))) )).
fof(mem_c_2Epatricia_2Eptree__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),arr(ty_2Epatricia_2Eptree(A_27a),arr(A_27b,arr(arr(ty_2Enum_2Enum,arr(A_27a,A_27b)),arr(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b)))),A_27b))))) ) ) )).
fof(mem_c_2Epatricia_2Eptree__size,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epatricia_2Eptree__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Enum_2Enum))) ) )).
fof(ax_thm_2Epatricia_2Eptree__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Epatricia_2Eptree(A_27a),ty_2Eind__type_2Erecspace(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(A_27a,ty_2Enum_2Enum))))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(A_27a,ty_2Enum_2Enum))),ty_2Epatricia_2Eptree(A_27a)),f2535(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Epatricia_2Eptree__case__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0v] : ( mem(V0v,A_27b) => ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V2f1] : ( mem(V2f1,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b))))) => ( ap(ap(ap(ap(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),c_2Epatricia_2EEmpty(A_27a)),V0v),V1f),V2f1) = V0v ) ) ) ) ) & ( ( ! [V3a0] : ( mem(V3a0,ty_2Enum_2Enum) => ! [V4a1] : ( mem(V4a1,A_27a) => ! [V5v] : ( mem(V5v,A_27b) => ! [V6f] : ( mem(V6f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V7f1] : ( mem(V7f1,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b))))) => ( ap(ap(ap(ap(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),ap(ap(c_2Epatricia_2ELeaf(A_27a),V3a0),V4a1)),V5v),V6f),V7f1) = ap(ap(V6f,V3a0),V4a1) ) ) ) ) ) ) ) & ! [V8a0] : ( mem(V8a0,ty_2Enum_2Enum) => ! [V9a1] : ( mem(V9a1,ty_2Enum_2Enum) => ! [V10a2] : ( mem(V10a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V11a3] : ( mem(V11a3,ty_2Epatricia_2Eptree(A_27a)) => ! [V12v] : ( mem(V12v,A_27b) => ! [V13f] : ( mem(V13f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V14f1] : ( mem(V14f1,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b))))) => ( ap(ap(ap(ap(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V8a0),V9a1),V10a2),V11a3)),V12v),V13f),V14f1) = ap(ap(ap(ap(V14f1,V8a0),V9a1),V10a2),V11a3) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2Eptree__size__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Epatricia_2Eptree__size(A_27a),V0f),c_2Epatricia_2EEmpty(A_27a)) = c_2Enum_2E0 ) ) ) & ( ( ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ! [V2a0] : ( mem(V2a0,ty_2Enum_2Enum) => ! [V3a1] : ( mem(V3a1,A_27a) => ( ap(ap(c_2Epatricia_2Eptree__size(A_27a),V1f),ap(ap(c_2Epatricia_2ELeaf(A_27a),V2a0),V3a1)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,V2a0),ap(V1f,V3a1))) ) ) ) ) ) & ! [V4f] : ( mem(V4f,arr(A_27a,ty_2Enum_2Enum)) => ! [V5a0] : ( mem(V5a0,ty_2Enum_2Enum) => ! [V6a1] : ( mem(V6a1,ty_2Enum_2Enum) => ! [V7a2] : ( mem(V7a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V8a3] : ( mem(V8a3,ty_2Epatricia_2Eptree(A_27a)) => ( ap(ap(c_2Epatricia_2Eptree__size(A_27a),V4f),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5a0),V6a1),V7a2),V8a3)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,V5a0),ap(ap(c_2Earithmetic_2E_2B,V6a1),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Epatricia_2Eptree__size(A_27a),V4f),V7a2)),ap(ap(c_2Epatricia_2Eptree__size(A_27a),V4f),V8a3))))) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epatricia_2Edatatype__ptree,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0ptree] : ( mem(V0ptree,arr(ty_2Epatricia_2Eptree(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,ty_2Epatricia_2Eptree(A_27a))),arr(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))))),bool)))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(V0ptree,c_2Epatricia_2EEmpty(A_27a)),c_2Epatricia_2ELeaf(A_27a)),c_2Epatricia_2EBranch(A_27a)))) )))).
fof(conj_thm_2Epatricia_2Eptree__11,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a0] : ( mem(V0a0,ty_2Enum_2Enum) => ! [V1a1] : ( mem(V1a1,A_27a) => ! [V2a0_27] : ( mem(V2a0_27,ty_2Enum_2Enum) => ! [V3a1_27] : ( mem(V3a1_27,A_27a) => ( ( ap(ap(c_2Epatricia_2ELeaf(A_27a),V0a0),V1a1) = ap(ap(c_2Epatricia_2ELeaf(A_27a),V2a0_27),V3a1_27) ) <=> ( ( V0a0 = V2a0_27 ) & ( V1a1 = V3a1_27 ) ) ) ) ) ) ) ) & ! [V4a0] : ( mem(V4a0,ty_2Enum_2Enum) => ! [V5a1] : ( mem(V5a1,ty_2Enum_2Enum) => ! [V6a2] : ( mem(V6a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V7a3] : ( mem(V7a3,ty_2Epatricia_2Eptree(A_27a)) => ! [V8a0_27] : ( mem(V8a0_27,ty_2Enum_2Enum) => ! [V9a1_27] : ( mem(V9a1_27,ty_2Enum_2Enum) => ! [V10a2_27] : ( mem(V10a2_27,ty_2Epatricia_2Eptree(A_27a)) => ! [V11a3_27] : ( mem(V11a3_27,ty_2Epatricia_2Eptree(A_27a)) => ( ( ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V4a0),V5a1),V6a2),V7a3) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V8a0_27),V9a1_27),V10a2_27),V11a3_27) ) <=> ( ( V4a0 = V8a0_27 ) & ( ( V5a1 = V9a1_27 ) & ( ( V6a2 = V10a2_27 ) & ( V7a3 = V11a3_27 ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2Eptree__distinct,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a1] : ( mem(V0a1,A_27a) => ! [V1a0] : ( mem(V1a0,ty_2Enum_2Enum) => ( ~~ ( c_2Epatricia_2EEmpty(A_27a) = ap(ap(c_2Epatricia_2ELeaf(A_27a),V1a0),V0a1) ) ) ) ) ) & ( ( ! [V2a3] : ( mem(V2a3,ty_2Epatricia_2Eptree(A_27a)) => ! [V3a2] : ( mem(V3a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V4a1] : ( mem(V4a1,ty_2Enum_2Enum) => ! [V5a0] : ( mem(V5a0,ty_2Enum_2Enum) => ( ~~ ( c_2Epatricia_2EEmpty(A_27a) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5a0),V4a1),V3a2),V2a3) ) ) ) ) ) ) ) & ! [V6a3] : ( mem(V6a3,ty_2Epatricia_2Eptree(A_27a)) => ! [V7a2] : ( mem(V7a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V8a1_27] : ( mem(V8a1_27,ty_2Enum_2Enum) => ! [V9a1] : ( mem(V9a1,A_27a) => ! [V10a0_27] : ( mem(V10a0_27,ty_2Enum_2Enum) => ! [V11a0] : ( mem(V11a0,ty_2Enum_2Enum) => ( ~~ ( ap(ap(c_2Epatricia_2ELeaf(A_27a),V11a0),V9a1) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V10a0_27),V8a1_27),V7a2),V6a3) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2Eptree__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0pp] : ( mem(V0pp,ty_2Epatricia_2Eptree(A_27a)) => ( ( V0pp = c_2Epatricia_2EEmpty(A_27a) ) | ( ( ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ? [V2a] : ( mem(V2a,A_27a) & ( V0pp = ap(ap(c_2Epatricia_2ELeaf(A_27a),V1n),V2a) ) ) ) ) | ? [V3n0] : ( mem(V3n0,ty_2Enum_2Enum) & ? [V4n] : ( mem(V4n,ty_2Enum_2Enum) & ? [V5p] : ( mem(V5p,ty_2Epatricia_2Eptree(A_27a)) & ? [V6p0] : ( mem(V6p0,ty_2Epatricia_2Eptree(A_27a)) & ( V0pp = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V3n0),V4n),V5p),V6p0) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2Eptree__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f0] : ( mem(V0f0,A_27b) => ! [V1f1] : ( mem(V1f1,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V2f2] : ( mem(V2f2,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(A_27b,arr(A_27b,A_27b))))))) => ? [V3fn] : ( mem(V3fn,arr(ty_2Epatricia_2Eptree(A_27a),A_27b)) & ( ( ap(V3fn,c_2Epatricia_2EEmpty(A_27a)) = V0f0 ) & ( ( ! [V4a0] : ( mem(V4a0,ty_2Enum_2Enum) => ! [V5a1] : ( mem(V5a1,A_27a) => ( ap(V3fn,ap(ap(c_2Epatricia_2ELeaf(A_27a),V4a0),V5a1)) = ap(ap(V1f1,V4a0),V5a1) ) ) ) ) & ! [V6a0] : ( mem(V6a0,ty_2Enum_2Enum) => ! [V7a1] : ( mem(V7a1,ty_2Enum_2Enum) => ! [V8a2] : ( mem(V8a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V9a3] : ( mem(V9a3,ty_2Epatricia_2Eptree(A_27a)) => ( ap(V3fn,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V6a0),V7a1),V8a2),V9a3)) = ap(ap(ap(ap(ap(ap(V2f2,V6a0),V7a1),V8a2),V9a3),ap(V3fn,V8a2)),ap(V3fn,V9a3)) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epatricia_2Eptree__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),bool)) => ( ( p(ap(V0P,c_2Epatricia_2EEmpty(A_27a))) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,A_27a) => p(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),V1n),V2a))) ) ) ) & ! [V3p] : ( mem(V3p,ty_2Epatricia_2Eptree(A_27a)) => ! [V4p0] : ( mem(V4p0,ty_2Epatricia_2Eptree(A_27a)) => ( ( p(ap(V0P,V3p)) & p(ap(V0P,V4p0)) ) => ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ! [V6n0] : ( mem(V6n0,ty_2Enum_2Enum) => p(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V6n0),V5n),V3p),V4p0))) ) ) ) ) ) ) ) => ! [V7p] : ( mem(V7p,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,V7p)) ) ) )))).
fof(conj_thm_2Epatricia_2Eptree__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(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V2f1_27] : ( mem(V2f1_27,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b))))) => ! [V3M] : ( mem(V3M,ty_2Epatricia_2Eptree(A_27a)) => ! [V4M_27] : ( mem(V4M_27,ty_2Epatricia_2Eptree(A_27a)) => ! [V5v] : ( mem(V5v,A_27b) => ! [V6f] : ( mem(V6f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V7f1] : ( mem(V7f1,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b))))) => ( ( ( V3M = V4M_27 ) & ( ( ( V4M_27 = c_2Epatricia_2EEmpty(A_27a) ) => ( V5v = V0v_27 ) ) & ( ( ! [V8a0] : ( mem(V8a0,ty_2Enum_2Enum) => ! [V9a1] : ( mem(V9a1,A_27a) => ( ( V4M_27 = ap(ap(c_2Epatricia_2ELeaf(A_27a),V8a0),V9a1) ) => ( ap(ap(V6f,V8a0),V9a1) = ap(ap(V1f_27,V8a0),V9a1) ) ) ) ) ) & ! [V10a0] : ( mem(V10a0,ty_2Enum_2Enum) => ! [V11a1] : ( mem(V11a1,ty_2Enum_2Enum) => ! [V12a2] : ( mem(V12a2,ty_2Epatricia_2Eptree(A_27a)) => ! [V13a3] : ( mem(V13a3,ty_2Epatricia_2Eptree(A_27a)) => ( ( V4M_27 = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V10a0),V11a1),V12a2),V13a3) ) => ( ap(ap(ap(ap(V7f1,V10a0),V11a1),V12a2),V13a3) = ap(ap(ap(ap(V2f1_27,V10a0),V11a1),V12a2),V13a3) ) ) ) ) ) ) ) ) ) => ( ap(ap(ap(ap(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),V3M),V5v),V6f),V7f1) = ap(ap(ap(ap(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),V4M_27),V0v_27),V1f_27),V2f1_27) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epatricia_2Eptree__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Epatricia_2Eptree(A_27a)) => ! [V1v] : ( mem(V1v,A_27b) => ! [V2f] : ( mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ! [V3f1] : ( mem(V3f1,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),A_27b))))) => ! [V4v_27] : ( mem(V4v_27,A_27b) => ( ( ap(ap(ap(ap(c_2Epatricia_2Eptree__CASE(A_27a,A_27b),V0x),V1v),V2f),V3f1) = V4v_27 ) <=> ( ( ( V0x = c_2Epatricia_2EEmpty(A_27a) ) & ( V1v = V4v_27 ) ) | ( ( ? [V5n] : ( mem(V5n,ty_2Enum_2Enum) & ? [V6a] : ( mem(V6a,A_27a) & ( ( V0x = ap(ap(c_2Epatricia_2ELeaf(A_27a),V5n),V6a) ) & ( ap(ap(V2f,V5n),V6a) = V4v_27 ) ) ) ) ) | ? [V7n0] : ( mem(V7n0,ty_2Enum_2Enum) & ? [V8n] : ( mem(V8n,ty_2Enum_2Enum) & ? [V9p] : ( mem(V9p,ty_2Epatricia_2Eptree(A_27a)) & ? [V10p0] : ( mem(V10p0,ty_2Epatricia_2Eptree(A_27a)) & ( ( V0x = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V7n0),V8n),V9p),V10p0) ) & ( ap(ap(ap(ap(V3f1,V7n0),V8n),V9p),V10p0) = V4v_27 ) ) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epatricia_2EBRANCHING__BIT__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) => ( ( ! [V1p0] : ( mem(V1p0,ty_2Enum_2Enum) => ! [V2p1] : ( mem(V2p1,ty_2Enum_2Enum) => ( ( ( ~~ ( ( p(ap(c_2Earithmetic_2EODD,V1p0)) <=> p(ap(c_2Earithmetic_2EEVEN,V2p1)) ) | ( V1p0 = V2p1 ) ) ) => p(ap(ap(V0P,ap(c_2Earithmetic_2EDIV2,V1p0)),ap(c_2Earithmetic_2EDIV2,V2p1))) ) => p(ap(ap(V0P,V1p0),V2p1)) ) ) ) ) => ! [V3v] : ( mem(V3v,ty_2Enum_2Enum) => ! [V4v1] : ( mem(V4v1,ty_2Enum_2Enum) => p(ap(ap(V0P,V3v),V4v1)) ) ) ) ))).
fof(conj_thm_2Epatricia_2EBRANCHING__BIT__def,lemma,(! [V0p1] : ( mem(V0p1,ty_2Enum_2Enum) => ! [V1p0] : ( mem(V1p0,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EBRANCHING__BIT,V1p0),V0p1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Emin_2E_3D(bool),ap(c_2Earithmetic_2EODD,V1p0)),ap(c_2Earithmetic_2EEVEN,V0p1))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1p0),V0p1))),c_2Enum_2E0),ap(c_2Enum_2ESUC,ap(ap(c_2Epatricia_2EBRANCHING__BIT,ap(c_2Earithmetic_2EDIV2,V1p0)),ap(c_2Earithmetic_2EDIV2,V0p1)))) ) ) ))).
fof(conj_thm_2Epatricia_2EPEEK__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,bool))) => ( ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => p(ap(ap(V0P,c_2Epatricia_2EEmpty(A_27a)),V1k)) ) ) & ( ( ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ! [V4k] : ( mem(V4k,ty_2Enum_2Enum) => p(ap(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),V2j),V3d)),V4k)) ) ) ) ) & ! [V5p] : ( mem(V5p,ty_2Enum_2Enum) => ! [V6m] : ( mem(V6m,ty_2Enum_2Enum) => ! [V7l] : ( mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ! [V8r] : ( mem(V8r,ty_2Epatricia_2Eptree(A_27a)) => ! [V9k] : ( mem(V9k,ty_2Enum_2Enum) => ( p(ap(ap(V0P,ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,V6m),V9k)),V7l),V8r)),V9k)) => p(ap(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5p),V6m),V7l),V8r)),V9k)) ) ) ) ) ) ) ) ) => ! [V10v] : ( mem(V10v,ty_2Epatricia_2Eptree(A_27a)) => ! [V11v1] : ( mem(V11v1,ty_2Enum_2Enum) => p(ap(ap(V0P,V10v),V11v1)) ) ) ) )))).
fof(conj_thm_2Epatricia_2EPEEK__def,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),c_2Epatricia_2EEmpty(A_27a)),V0k) = c_2Eoption_2ENONE(A_27a) ) ) ) & ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V2j),V3d)),V1k) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),V2j)),ap(c_2Eoption_2ESOME(A_27a),V3d)),c_2Eoption_2ENONE(A_27a)) ) ) ) ) ) & ! [V4r] : ( mem(V4r,ty_2Epatricia_2Eptree(A_27a)) => ! [V5p] : ( mem(V5p,ty_2Enum_2Enum) => ! [V6m] : ( mem(V6m,ty_2Enum_2Enum) => ! [V7l] : ( mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ! [V8k] : ( mem(V8k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5p),V6m),V7l),V4r)),V8k) = ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,V6m),V8k)),V7l),V4r)),V8k) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Epatricia_2EJOIN__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0p0] : ( mem(V0p0,ty_2Enum_2Enum) => ! [V1t0] : ( mem(V1t0,ty_2Epatricia_2Eptree(A_27a)) => ! [V2p1] : ( mem(V2p1,ty_2Enum_2Enum) => ! [V3t1] : ( mem(V3t1,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2EJOIN(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)))),V0p0),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a))),V1t0),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)),V2p1),V3t1)))) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)),f2536(A_27a,V3t1,V0p0,V1t0)),ap(ap(c_2Epatricia_2EBRANCHING__BIT,V0p0),V2p1)) ) ) ) ) ) ) )).
fof(conj_thm_2Epatricia_2EADD__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),bool))) => ( ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2e] : ( mem(V2e,A_27a) => p(ap(ap(V0P,c_2Epatricia_2EEmpty(A_27a)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2e))) ) ) ) & ( ( ! [V3j] : ( mem(V3j,ty_2Enum_2Enum) => ! [V4d] : ( mem(V4d,A_27a) => ! [V5k] : ( mem(V5k,ty_2Enum_2Enum) => ! [V6e] : ( mem(V6e,A_27a) => p(ap(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),V3j),V4d)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V5k),V6e))) ) ) ) ) ) & ! [V7p] : ( mem(V7p,ty_2Enum_2Enum) => ! [V8m] : ( mem(V8m,ty_2Enum_2Enum) => ! [V9l] : ( mem(V9l,ty_2Epatricia_2Eptree(A_27a)) => ! [V10r] : ( mem(V10r,ty_2Epatricia_2Eptree(A_27a)) => ! [V11k] : ( mem(V11k,ty_2Enum_2Enum) => ! [V12e] : ( mem(V12e,A_27a) => ( ( ( ( p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,V8m),V11k),V7p)) & ( ~~ p(ap(ap(c_2Ebit_2EBIT,V8m),V11k)) ) ) => p(ap(ap(V0P,V10r),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V11k),V12e))) ) & ( ( p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,V8m),V11k),V7p)) & p(ap(ap(c_2Ebit_2EBIT,V8m),V11k)) ) => p(ap(ap(V0P,V9l),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V11k),V12e))) ) ) => p(ap(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V7p),V8m),V9l),V10r)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V11k),V12e))) ) ) ) ) ) ) ) ) ) => ! [V13v] : ( mem(V13v,ty_2Epatricia_2Eptree(A_27a)) => ! [V14v1] : ( mem(V14v1,ty_2Enum_2Enum) => ! [V15v2] : ( mem(V15v2,A_27a) => p(ap(ap(V0P,V13v),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V14v1),V15v2))) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EADD__def,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1e] : ( mem(V1e,A_27a) => ( ap(ap(c_2Epatricia_2EADD(A_27a),c_2Epatricia_2EEmpty(A_27a)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V0k),V1e)) = ap(ap(c_2Epatricia_2ELeaf(A_27a),V0k),V1e) ) ) ) ) & ( ( ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ! [V3j] : ( mem(V3j,ty_2Enum_2Enum) => ! [V4e] : ( mem(V4e,A_27a) => ! [V5d] : ( mem(V5d,A_27a) => ( ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V3j),V5d)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V2k),V4e)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V3j),V2k)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V2k),V4e)),ap(c_2Epatricia_2EJOIN(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)))),V2k),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a))),ap(ap(c_2Epatricia_2ELeaf(A_27a),V2k),V4e)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)),V3j),ap(ap(c_2Epatricia_2ELeaf(A_27a),V3j),V5d)))))) ) ) ) ) ) ) & ! [V6r] : ( mem(V6r,ty_2Epatricia_2Eptree(A_27a)) => ! [V7p] : ( mem(V7p,ty_2Enum_2Enum) => ! [V8m] : ( mem(V8m,ty_2Enum_2Enum) => ! [V9l] : ( mem(V9l,ty_2Epatricia_2Eptree(A_27a)) => ! [V10k] : ( mem(V10k,ty_2Enum_2Enum) => ! [V11e] : ( mem(V11e,A_27a) => ( ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V7p),V8m),V9l),V6r)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V10k),V11e)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,V8m),V10k),V7p)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,V8m),V10k)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V7p),V8m),ap(ap(c_2Epatricia_2EADD(A_27a),V9l),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V10k),V11e))),V6r)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V7p),V8m),V9l),ap(ap(c_2Epatricia_2EADD(A_27a),V6r),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V10k),V11e))))),ap(c_2Epatricia_2EJOIN(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)))),V10k),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a))),ap(ap(c_2Epatricia_2ELeaf(A_27a),V10k),V11e)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)),V7p),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V7p),V8m),V9l),V6r)))))) ) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Epatricia_2EBRANCH__primitive__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Epatricia_2EBRANCH(A_27a) = ap(ap(c_2Erelation_2EWFREC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),ty_2Epatricia_2Eptree(A_27a)),ap(c_2Emin_2E_40(arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),bool))),f2537(A_27a))),k(arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),ty_2Epatricia_2Eptree(A_27a)),f2562(A_27a))) ) ) )).
fof(conj_thm_2Epatricia_2EBRANCH__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),bool)) => ( ( ( ! [V1p] : ( mem(V1p,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3t] : ( mem(V3t,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V1p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V2m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),c_2Epatricia_2EEmpty(A_27a)),V3t))))) ) ) ) ) & ( ( ! [V4p] : ( mem(V4p,ty_2Enum_2Enum) => ! [V5m] : ( mem(V5m,ty_2Enum_2Enum) => ! [V6v6] : ( mem(V6v6,ty_2Enum_2Enum) => ! [V7v7] : ( mem(V7v7,A_27a) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V4p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V5m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V6v6),V7v7)),c_2Epatricia_2EEmpty(A_27a)))))) ) ) ) ) ) & ( ( ! [V8p] : ( mem(V8p,ty_2Enum_2Enum) => ! [V9m] : ( mem(V9m,ty_2Enum_2Enum) => ! [V10v8] : ( mem(V10v8,ty_2Enum_2Enum) => ! [V11v9] : ( mem(V11v9,ty_2Enum_2Enum) => ! [V12v10] : ( mem(V12v10,ty_2Epatricia_2Eptree(A_27a)) => ! [V13v11] : ( mem(V13v11,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V8p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V9m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V10v8),V11v9),V12v10),V13v11)),c_2Epatricia_2EEmpty(A_27a)))))) ) ) ) ) ) ) ) & ( ( ! [V14p] : ( mem(V14p,ty_2Enum_2Enum) => ! [V15m] : ( mem(V15m,ty_2Enum_2Enum) => ! [V16v12] : ( mem(V16v12,ty_2Enum_2Enum) => ! [V17v13] : ( mem(V17v13,A_27a) => ! [V18v24] : ( mem(V18v24,ty_2Enum_2Enum) => ! [V19v25] : ( mem(V19v25,A_27a) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V14p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V15m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V16v12),V17v13)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V18v24),V19v25)))))) ) ) ) ) ) ) ) & ( ( ! [V20p] : ( mem(V20p,ty_2Enum_2Enum) => ! [V21m] : ( mem(V21m,ty_2Enum_2Enum) => ! [V22v12] : ( mem(V22v12,ty_2Enum_2Enum) => ! [V23v13] : ( mem(V23v13,A_27a) => ! [V24v26] : ( mem(V24v26,ty_2Enum_2Enum) => ! [V25v27] : ( mem(V25v27,ty_2Enum_2Enum) => ! [V26v28] : ( mem(V26v28,ty_2Epatricia_2Eptree(A_27a)) => ! [V27v29] : ( mem(V27v29,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V20p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V21m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V22v12),V23v13)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V24v26),V25v27),V26v28),V27v29)))))) ) ) ) ) ) ) ) ) ) & ( ( ! [V28p] : ( mem(V28p,ty_2Enum_2Enum) => ! [V29m] : ( mem(V29m,ty_2Enum_2Enum) => ! [V30v14] : ( mem(V30v14,ty_2Enum_2Enum) => ! [V31v15] : ( mem(V31v15,ty_2Enum_2Enum) => ! [V32v16] : ( mem(V32v16,ty_2Epatricia_2Eptree(A_27a)) => ! [V33v17] : ( mem(V33v17,ty_2Epatricia_2Eptree(A_27a)) => ! [V34v36] : ( mem(V34v36,ty_2Enum_2Enum) => ! [V35v37] : ( mem(V35v37,A_27a) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V28p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V29m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V30v14),V31v15),V32v16),V33v17)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V34v36),V35v37)))))) ) ) ) ) ) ) ) ) ) & ! [V36p] : ( mem(V36p,ty_2Enum_2Enum) => ! [V37m] : ( mem(V37m,ty_2Enum_2Enum) => ! [V38v14] : ( mem(V38v14,ty_2Enum_2Enum) => ! [V39v15] : ( mem(V39v15,ty_2Enum_2Enum) => ! [V40v16] : ( mem(V40v16,ty_2Epatricia_2Eptree(A_27a)) => ! [V41v17] : ( mem(V41v17,ty_2Epatricia_2Eptree(A_27a)) => ! [V42v38] : ( mem(V42v38,ty_2Enum_2Enum) => ! [V43v39] : ( mem(V43v39,ty_2Enum_2Enum) => ! [V44v40] : ( mem(V44v40,ty_2Epatricia_2Eptree(A_27a)) => ! [V45v41] : ( mem(V45v41,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V36p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V37m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V38v14),V39v15),V40v16),V41v17)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V42v38),V43v39),V44v40),V45v41)))))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => ! [V46v] : ( mem(V46v,ty_2Enum_2Enum) => ! [V47v1] : ( mem(V47v1,ty_2Enum_2Enum) => ! [V48v2] : ( mem(V48v2,ty_2Epatricia_2Eptree(A_27a)) => ! [V49v3] : ( mem(V49v3,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V46v),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V47v1),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V48v2),V49v3))))) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EBRANCH__def,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2t] : ( mem(V2t,ty_2Epatricia_2Eptree(A_27a)) => ! [V3v6] : ( mem(V3v6,ty_2Enum_2Enum) => ! [V4v7] : ( mem(V4v7,A_27a) => ! [V5v8] : ( mem(V5v8,ty_2Enum_2Enum) => ! [V6v9] : ( mem(V6v9,ty_2Enum_2Enum) => ! [V7v10] : ( mem(V7v10,ty_2Epatricia_2Eptree(A_27a)) => ! [V8v11] : ( mem(V8v11,ty_2Epatricia_2Eptree(A_27a)) => ! [V9v12] : ( mem(V9v12,ty_2Enum_2Enum) => ! [V10v13] : ( mem(V10v13,A_27a) => ! [V11v24] : ( mem(V11v24,ty_2Enum_2Enum) => ! [V12v25] : ( mem(V12v25,A_27a) => ! [V13v26] : ( mem(V13v26,ty_2Enum_2Enum) => ! [V14v27] : ( mem(V14v27,ty_2Enum_2Enum) => ! [V15v28] : ( mem(V15v28,ty_2Epatricia_2Eptree(A_27a)) => ! [V16v29] : ( mem(V16v29,ty_2Epatricia_2Eptree(A_27a)) => ! [V17v14] : ( mem(V17v14,ty_2Enum_2Enum) => ! [V18v15] : ( mem(V18v15,ty_2Enum_2Enum) => ! [V19v16] : ( mem(V19v16,ty_2Epatricia_2Eptree(A_27a)) => ! [V20v17] : ( mem(V20v17,ty_2Epatricia_2Eptree(A_27a)) => ! [V21v36] : ( mem(V21v36,ty_2Enum_2Enum) => ! [V22v37] : ( mem(V22v37,A_27a) => ! [V23v38] : ( mem(V23v38,ty_2Enum_2Enum) => ! [V24v39] : ( mem(V24v39,ty_2Enum_2Enum) => ! [V25v40] : ( mem(V25v40,ty_2Epatricia_2Eptree(A_27a)) => ! [V26v41] : ( mem(V26v41,ty_2Epatricia_2Eptree(A_27a)) => ( ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),c_2Epatricia_2EEmpty(A_27a)),V2t)))) = V2t ) & ( ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V3v6),V4v7)),c_2Epatricia_2EEmpty(A_27a))))) = ap(ap(c_2Epatricia_2ELeaf(A_27a),V3v6),V4v7) ) & ( ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5v8),V6v9),V7v10),V8v11)),c_2Epatricia_2EEmpty(A_27a))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5v8),V6v9),V7v10),V8v11) ) & ( ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V9v12),V10v13)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V11v24),V12v25))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V0p),V1m),ap(ap(c_2Epatricia_2ELeaf(A_27a),V9v12),V10v13)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V11v24),V12v25)) ) & ( ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V9v12),V10v13)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V13v26),V14v27),V15v28),V16v29))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V0p),V1m),ap(ap(c_2Epatricia_2ELeaf(A_27a),V9v12),V10v13)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V13v26),V14v27),V15v28),V16v29)) ) & ( ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V17v14),V18v15),V19v16),V20v17)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V21v36),V22v37))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V0p),V1m),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V17v14),V18v15),V19v16),V20v17)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V21v36),V22v37)) ) & ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V17v14),V18v15),V19v16),V20v17)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V23v38),V24v39),V25v40),V26v41))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V0p),V1m),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V17v14),V18v15),V19v16),V20v17)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V23v38),V24v39),V25v40),V26v41)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Epatricia_2EREMOVE__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EREMOVE(A_27a),c_2Epatricia_2EEmpty(A_27a)),V0k) = c_2Epatricia_2EEmpty(A_27a) ) ) ) & ( ( ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V1j),V2d)),V3k) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1j),V3k)),c_2Epatricia_2EEmpty(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),V1j),V2d)) ) ) ) ) ) & ! [V4p] : ( mem(V4p,ty_2Enum_2Enum) => ! [V5m] : ( mem(V5m,ty_2Enum_2Enum) => ! [V6l] : ( mem(V6l,ty_2Epatricia_2Eptree(A_27a)) => ! [V7r] : ( mem(V7r,ty_2Epatricia_2Eptree(A_27a)) => ! [V8k] : ( mem(V8k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V4p),V5m),V6l),V7r)),V8k) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,V5m),V8k),V4p)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,V5m),V8k)),ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V4p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V5m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V6l),V8k)),V7r))))),ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V4p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V5m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V6l),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V7r),V8k))))))),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V4p),V5m),V6l),V7r)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2ETRAVERSE__AUX__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),c_2Epatricia_2EEmpty(A_27a)),V0a) = V0a ) ) ) & ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ! [V3a] : ( mem(V3a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V1k),V2d)),V3a) = ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),V1k),V3a) ) ) ) ) ) & ! [V4p] : ( mem(V4p,ty_2Enum_2Enum) => ! [V5m] : ( mem(V5m,ty_2Enum_2Enum) => ! [V6l] : ( mem(V6l,ty_2Epatricia_2Eptree(A_27a)) => ! [V7r] : ( mem(V7r,ty_2Epatricia_2Eptree(A_27a)) => ! [V8a] : ( mem(V8a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V4p),V5m),V6l),V7r)),V8a) = ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),V6l),ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),V7r),V8a)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2ETRAVERSE__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Epatricia_2ETRAVERSE(A_27a),c_2Epatricia_2EEmpty(A_27a)) = c_2Elist_2ENIL(ty_2Enum_2Enum) ) & ( ( ! [V0j] : ( mem(V0j,ty_2Enum_2Enum) => ! [V1d] : ( mem(V1d,A_27a) => ( ap(c_2Epatricia_2ETRAVERSE(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V0j),V1d)) = ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),V0j),c_2Elist_2ENIL(ty_2Enum_2Enum)) ) ) ) ) & ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Epatricia_2Eptree(A_27a)) => ! [V5r] : ( mem(V5r,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2ETRAVERSE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V2p),V3m),V4l),V5r)) = ap(ap(c_2Elist_2EAPPEND(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(A_27a),V4l)),ap(c_2Epatricia_2ETRAVERSE(A_27a),V5r)) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2EKEYS__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2EKEYS(A_27a),V0t) = ap(ap(c_2Esorting_2EQSORT(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C),ap(c_2Epatricia_2ETRAVERSE(A_27a),V0t)) ) ) ) )).
fof(ax_thm_2Epatricia_2ETRANSFORM__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(A_27b,A_27a)) => ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V0f),c_2Epatricia_2EEmpty(A_27b)) = c_2Epatricia_2EEmpty(A_27a) ) ) ) & ( ( ! [V1f] : ( mem(V1f,arr(A_27b,A_27a)) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27b) => ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V1f),ap(ap(c_2Epatricia_2ELeaf(A_27b),V2j),V3d)) = ap(ap(c_2Epatricia_2ELeaf(A_27a),V2j),ap(V1f,V3d)) ) ) ) ) ) & ! [V4f] : ( mem(V4f,arr(A_27b,A_27a)) => ! [V5p] : ( mem(V5p,ty_2Enum_2Enum) => ! [V6m] : ( mem(V6m,ty_2Enum_2Enum) => ! [V7l] : ( mem(V7l,ty_2Epatricia_2Eptree(A_27b)) => ! [V8r] : ( mem(V8r,ty_2Epatricia_2Eptree(A_27b)) => ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V4f),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27b),V5p),V6m),V7l),V8r)) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5p),V6m),ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V4f),V7l)),ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V4f),V8r)) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2EEVERY__LEAF__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),c_2Epatricia_2EEmpty(A_27a))) <=> $true ) ) ) & ( ( ! [V1P] : ( mem(V1P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V1P),ap(ap(c_2Epatricia_2ELeaf(A_27a),V2j),V3d))) <=> p(ap(ap(V1P,V2j),V3d)) ) ) ) ) ) & ! [V4P] : ( mem(V4P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V5p] : ( mem(V5p,ty_2Enum_2Enum) => ! [V6m] : ( mem(V6m,ty_2Enum_2Enum) => ! [V7l] : ( mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ! [V8r] : ( mem(V8r,ty_2Epatricia_2Eptree(A_27a)) => ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V4P),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5p),V6m),V7l),V8r))) <=> ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V4P),V7l)) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V4P),V8r)) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2EEXISTS__LEAF__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( p(ap(ap(c_2Epatricia_2EEXISTS__LEAF(A_27a),V0P),c_2Epatricia_2EEmpty(A_27a))) <=> $false ) ) ) & ( ( ! [V1P] : ( mem(V1P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ( p(ap(ap(c_2Epatricia_2EEXISTS__LEAF(A_27a),V1P),ap(ap(c_2Epatricia_2ELeaf(A_27a),V2j),V3d))) <=> p(ap(ap(V1P,V2j),V3d)) ) ) ) ) ) & ! [V4P] : ( mem(V4P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V5p] : ( mem(V5p,ty_2Enum_2Enum) => ! [V6m] : ( mem(V6m,ty_2Enum_2Enum) => ! [V7l] : ( mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ! [V8r] : ( mem(V8r,ty_2Epatricia_2Eptree(A_27a)) => ( p(ap(ap(c_2Epatricia_2EEXISTS__LEAF(A_27a),V4P),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V5p),V6m),V7l),V8r))) <=> ( p(ap(ap(c_2Epatricia_2EEXISTS__LEAF(A_27a),V4P),V7l)) | p(ap(ap(c_2Epatricia_2EEXISTS__LEAF(A_27a),V4P),V8r)) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2ESIZE__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2ESIZE(A_27a),V0t) = ap(c_2Elist_2ELENGTH(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(A_27a),V0t)) ) ) ) )).
fof(ax_thm_2Epatricia_2EDEPTH__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Epatricia_2EDEPTH(A_27a),c_2Epatricia_2EEmpty(A_27a)) = c_2Enum_2E0 ) & ( ( ! [V0j] : ( mem(V0j,ty_2Enum_2Enum) => ! [V1d] : ( mem(V1d,A_27a) => ( ap(c_2Epatricia_2EDEPTH(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V0j),V1d)) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) ) & ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Epatricia_2Eptree(A_27a)) => ! [V5r] : ( mem(V5r,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2EDEPTH(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V2p),V3m),V4l),V5r)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2EMAX,ap(c_2Epatricia_2EDEPTH(A_27a),V4l)),ap(c_2Epatricia_2EDEPTH(A_27a),V5r))) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2EIS__PTREE__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),c_2Epatricia_2EEmpty(A_27a))) <=> $true ) & ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1d] : ( mem(V1d,A_27a) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V0k),V1d))) <=> $true ) ) ) ) & ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Epatricia_2Eptree(A_27a)) => ! [V5r] : ( mem(V5r,ty_2Epatricia_2Eptree(A_27a)) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V2p),V3m),V4l),V5r))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,V2p),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V3m))) & ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V4l)) & ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V5r)) & ( ( ~~ ( V4l = c_2Epatricia_2EEmpty(A_27a) ) ) & ( ( ~~ ( V5r = c_2Epatricia_2EEmpty(A_27a) ) ) & ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),f2563(V2p,V3m)),V4l)) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),f2564(V2p,V3m)),V5r)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Epatricia_2EIN__PTREE__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V0n),V1t)) <=> p(ap(c_2Eoption_2EIS__SOME(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EPEEK(ty_2Eone_2Eone),V1t),V0n))) ) ) )).
fof(ax_thm_2Epatricia_2EINSERT__PTREE__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ap(ap(c_2Epatricia_2EINSERT__PTREE,V0n),V1t) = ap(ap(c_2Epatricia_2EADD(ty_2Eone_2Eone),V1t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eone_2Eone),V0n),c_2Eone_2Eone)) ) ) )).
fof(ax_thm_2Epatricia_2EPTREE__OF__NUMSET__def,axiom, ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),V1s) = ap(ap(ap(c_2Elist_2EFOLDL(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)),ap(c_2Ecombin_2EC(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(ty_2Eone_2Eone),ty_2Epatricia_2Eptree(ty_2Eone_2Eone)),c_2Epatricia_2EINSERT__PTREE)),V0t),ap(c_2Elist_2ESET__TO__LIST(ty_2Enum_2Enum),V1s)) ) ) )).
fof(ax_thm_2Epatricia_2ENUMSET__OF__PTREE__def,axiom, ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t) = ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),V0t)) ) )).
fof(ax_thm_2Epatricia_2EUNION__PTREE__def,axiom, ! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ap(ap(c_2Epatricia_2EUNION__PTREE,V0t1),V1t2) = ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t1),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V1t2)) ) ) )).
fof(ax_thm_2Epatricia_2EIS__EMPTY__primitive__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Epatricia_2EIS__EMPTY(A_27a) = ap(ap(c_2Erelation_2EWFREC(ty_2Epatricia_2Eptree(A_27a),bool),ap(c_2Emin_2E_40(arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),bool))),f2565(A_27a))),k(arr(ty_2Epatricia_2Eptree(A_27a),bool),f2566(A_27a))) ) ) )).
fof(conj_thm_2Epatricia_2EIS__EMPTY__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),bool)) => ( ( p(ap(V0P,c_2Epatricia_2EEmpty(A_27a))) & ( ( ! [V1v] : ( mem(V1v,ty_2Enum_2Enum) => ! [V2v1] : ( mem(V2v1,A_27a) => p(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),V1v),V2v1))) ) ) ) & ! [V3v2] : ( mem(V3v2,ty_2Enum_2Enum) => ! [V4v3] : ( mem(V4v3,ty_2Enum_2Enum) => ! [V5v4] : ( mem(V5v4,ty_2Epatricia_2Eptree(A_27a)) => ! [V6v5] : ( mem(V6v5,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V3v2),V4v3),V5v4),V6v5))) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,V7v)) ) ) )))).
fof(conj_thm_2Epatricia_2EIS__EMPTY__def,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Enum_2Enum) => ! [V1v1] : ( mem(V1v1,A_27a) => ! [V2v2] : ( mem(V2v2,ty_2Enum_2Enum) => ! [V3v3] : ( mem(V3v3,ty_2Enum_2Enum) => ! [V4v4] : ( mem(V4v4,ty_2Epatricia_2Eptree(A_27a)) => ! [V5v5] : ( mem(V5v5,ty_2Epatricia_2Eptree(A_27a)) => ( ( p(ap(c_2Epatricia_2EIS__EMPTY(A_27a),c_2Epatricia_2EEmpty(A_27a))) <=> $true ) & ( ( p(ap(c_2Epatricia_2EIS__EMPTY(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),V0v),V1v1))) <=> $false ) & ( p(ap(c_2Epatricia_2EIS__EMPTY(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V2v2),V3v3),V4v4),V5v5))) <=> $false ) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Epatricia_2EFIND__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EFIND(A_27a),V0t),V1k) = ap(c_2Eoption_2ETHE(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),V1k)) ) ) ) ) )).
fof(ax_thm_2Epatricia_2EADD__LIST__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Epatricia_2EADD__LIST(A_27a) = ap(c_2Elist_2EFOLDL(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),ty_2Epatricia_2Eptree(A_27a)),c_2Epatricia_2EADD(A_27a)) ) ) )).
fof(conj_thm_2Epatricia_2EBRANCHING__BIT,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( ( ~~ ( V0a = V1b ) ) => ( ~~ ( p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Epatricia_2EBRANCHING__BIT,V0a),V1b)),V0a)) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Epatricia_2EBRANCHING__BIT,V0a),V1b)),V1b)) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EBRANCHING__BIT__ZERO,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( ( ap(ap(c_2Epatricia_2EBRANCHING__BIT,V0a),V1b) = c_2Enum_2E0 ) <=> ( ( p(ap(c_2Earithmetic_2EODD,V0a)) <=> p(ap(c_2Earithmetic_2EEVEN,V1b)) ) | ( V0a = V1b ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EBRANCHING__BIT__SYM,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EBRANCHING__BIT,V0a),V1b) = ap(ap(c_2Epatricia_2EBRANCHING__BIT,V1b),V0a) ) ) ))).
fof(conj_thm_2Epatricia_2EEVERY__LEAF__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ( ( p(ap(ap(V0P,V2k),V3d)) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V1t)) ) => p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),ap(ap(c_2Epatricia_2EADD(A_27a),V1t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V2k),V3d)))) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EMONO__EVERY__LEAF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1Q] : ( mem(V1Q,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V2t] : ( mem(V2t,ty_2Epatricia_2Eptree(A_27a)) => ( ( ( ! [V3k] : ( mem(V3k,ty_2Enum_2Enum) => ! [V4d] : ( mem(V4d,A_27a) => ( p(ap(ap(V0P,V3k),V4d)) => p(ap(ap(V1Q,V3k),V4d)) ) ) ) ) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V2t)) ) => p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V1Q),V2t)) ) ) ) )))).
fof(conj_thm_2Epatricia_2ENOT__ADD__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ( ~~ ( ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2d)) = c_2Epatricia_2EEmpty(A_27a) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EEMPTY__IS__PTREE,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Epatricia_2EIS__PTREE(A_27a),c_2Epatricia_2EEmpty(A_27a)))))).
fof(conj_thm_2Epatricia_2EADD__IS__PTREE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),V1x))) ) ) )))).
fof(conj_thm_2Epatricia_2EEVERY__LEAF__BRANCH,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1p] : ( mem(V1p,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3l] : ( mem(V3l,ty_2Epatricia_2Eptree(A_27a)) => ! [V4r] : ( mem(V4r,ty_2Epatricia_2Eptree(A_27a)) => ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V1p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V2m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V3l),V4r)))))) <=> ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V3l)) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V4r)) ) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EEVERY__LEAF__REMOVE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V1t)) => p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V1t),V2k))) ) ) ) )))).
fof(conj_thm_2Epatricia_2EIS__PTREE__BRANCH,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Epatricia_2Eptree(A_27a)) => ! [V3r] : ( mem(V3r,ty_2Epatricia_2Eptree(A_27a)) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0p),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V1m))) & ( ( ~~ ( ( V2l = c_2Epatricia_2EEmpty(A_27a) ) & ( V3r = c_2Epatricia_2EEmpty(A_27a) ) ) ) & ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),f2567(V0p,V1m)),V2l)) & ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),f2568(V0p,V1m)),V3r)) & ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V2l)) & p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V3r)) ) ) ) ) ) => p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V2l),V3r)))))) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EREMOVE__IS__PTREE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V1k))) ) ) )))).
fof(conj_thm_2Epatricia_2EPEEK__NONE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ( ( ! [V3d] : ( mem(V3d,A_27a) => ( ~~ p(ap(ap(V0P,V2k),V3d)) ) ) ) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V1t)) ) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),V2k) = c_2Eoption_2ENONE(A_27a) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EPEEK__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ! [V3j] : ( mem(V3j,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2d))),V3j) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),V3j)),ap(c_2Eoption_2ESOME(A_27a),V2d)),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),V3j)) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EBRANCH,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Epatricia_2Eptree(A_27a)) => ! [V3r] : ( mem(V3r,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V0p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V1m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V2l),V3r)))) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Epatricia_2Eptree(A_27a)),V2l),c_2Epatricia_2EEmpty(A_27a))),V3r),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Epatricia_2Eptree(A_27a)),V3r),c_2Epatricia_2EEmpty(A_27a))),V2l),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V0p),V1m),V2l),V3r))) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EPEEK__REMOVE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V1k)),V2j) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),V2j)),c_2Eoption_2ENONE(A_27a)),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),V2j)) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EEVERY__LEAF__TRANSFORM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1Q] : ( mem(V1Q,arr(ty_2Enum_2Enum,arr(A_27b,bool))) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ! [V3t] : ( mem(V3t,ty_2Epatricia_2Eptree(A_27a)) => ( ( ( ! [V4k] : ( mem(V4k,ty_2Enum_2Enum) => ! [V5d] : ( mem(V5d,A_27a) => ( p(ap(ap(V0P,V4k),V5d)) => p(ap(ap(V1Q,V4k),ap(V2f,V5d))) ) ) ) ) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V3t)) ) => p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27b),V1Q),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V2f),V3t))) ) ) ) ) ))))).
fof(conj_thm_2Epatricia_2ETRANSFORM__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t) = c_2Epatricia_2EEmpty(A_27b) ) <=> ( V1t = c_2Epatricia_2EEmpty(A_27a) ) ) ) ))))).
fof(conj_thm_2Epatricia_2ETRANSFORM__IS__PTREE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V1t)) => p(ap(c_2Epatricia_2EIS__PTREE(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t))) ) ) ))))).
fof(conj_thm_2Epatricia_2EPEEK__TRANSFORM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EPEEK(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t)),V2k) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),V2k)),c_2Eoption_2ENONE(A_27b)),f2569(A_27a,A_27b,V0f)) ) ) ) ))))).
fof(conj_thm_2Epatricia_2EADD__TRANSFORM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),ap(ap(c_2Epatricia_2EADD(A_27a),V1t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V2k),V3d))) = ap(ap(c_2Epatricia_2EADD(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27b),V2k),ap(V0f,V3d))) ) ) ) ) ))))).
fof(conj_thm_2Epatricia_2ETRANSFORM__BRANCH,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1p] : ( mem(V1p,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3l] : ( mem(V3l,ty_2Epatricia_2Eptree(A_27a)) => ! [V4r] : ( mem(V4r,ty_2Epatricia_2Eptree(A_27a)) => ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),ap(c_2Epatricia_2EBRANCH(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)))),V1p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),V2m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V3l),V4r))))) = ap(c_2Epatricia_2EBRANCH(A_27b),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27b),ty_2Epatricia_2Eptree(A_27b)))),V1p),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27b),ty_2Epatricia_2Eptree(A_27b))),V2m),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27b),ty_2Epatricia_2Eptree(A_27b)),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V3l)),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V4r))))) ) ) ) ) ) ))))).
fof(conj_thm_2Epatricia_2EREMOVE__TRANSFORM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V1t),V2k)) = ap(ap(c_2Epatricia_2EREMOVE(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t)),V2k) ) ) ) ))))).
fof(conj_thm_2Epatricia_2EREMOVE__ADD__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ( ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2d))),V1k) = ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V1k) ) ) ) )))).
fof(conj_thm_2Epatricia_2EADD__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ! [V3e] : ( mem(V3e,A_27a) => ( ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2d))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V3e)) = ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V3e)) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EEVERY__LEAF__PEEK,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V1t)) & p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),V2k))) ) => p(ap(ap(V0P,V2k),ap(c_2Eoption_2ETHE(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),V2k)))) ) ) ) )))).
fof(conj_thm_2Epatricia_2EIS__PTREE__PEEK,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ~~ p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),c_2Epatricia_2EEmpty(A_27a)),V0k))) ) ) ) & ( ( ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3b] : ( mem(V3b,A_27b) => ( p(ap(c_2Eoption_2EIS__SOME(A_27b),ap(ap(c_2Epatricia_2EPEEK(A_27b),ap(ap(c_2Epatricia_2ELeaf(A_27b),V2j),V3b)),V1k))) <=> ( V2j = V1k ) ) ) ) ) ) & ! [V4p] : ( mem(V4p,ty_2Enum_2Enum) => ! [V5m] : ( mem(V5m,ty_2Enum_2Enum) => ! [V6l] : ( mem(V6l,ty_2Epatricia_2Eptree(A_27c)) => ! [V7r] : ( mem(V7r,ty_2Epatricia_2Eptree(A_27c)) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27c),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27c),V4p),V5m),V6l),V7r))) => ( ( ? [V8k] : ( mem(V8k,ty_2Enum_2Enum) & ( p(ap(ap(c_2Ebit_2EBIT,V5m),V8k)) & p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V6l),V8k))) ) ) ) & ( ( ? [V9k] : ( mem(V9k,ty_2Enum_2Enum) & ( ( ~~ p(ap(ap(c_2Ebit_2EBIT,V5m),V9k)) ) & p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V7r),V9k))) ) ) ) & ! [V10k] : ( mem(V10k,ty_2Enum_2Enum) => ! [V11n] : ( mem(V11n,ty_2Enum_2Enum) => ( ( ( ~~ p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,V5m),V10k),V4p)) ) | ( p(ap(ap(c_2Eprim__rec_2E_3C,V11n),V5m)) & ( ~~ ( p(ap(ap(c_2Ebit_2EBIT,V11n),V4p)) <=> p(ap(ap(c_2Ebit_2EBIT,V11n),V10k)) ) ) ) ) => ( ( ~~ p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V6l),V10k))) ) & ( ~~ p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V7r),V10k))) ) ) ) ) ) ) ) ) ) ) ) ) ) )))))).
fof(conj_thm_2Epatricia_2EPTREE__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(A_27a)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(A_27a)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t1)) & p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V1t2)) ) => ( ( ! [V2k] : ( mem(V2k,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t1),V2k) = ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t2),V2k) ) ) ) <=> ( V0t1 = V1t2 ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EREMOVE__REMOVE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => ( ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V1k)),V1k) = ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V1k) ) ) ) )))).
fof(conj_thm_2Epatricia_2EREMOVE__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2d] : ( mem(V2d,A_27a) => ! [V3j] : ( mem(V3j,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => ( ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2d))),V3j) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),V3j)),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V3j)),ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),V3j)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V2d))) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EADD__ADD__SYM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,A_27a) => ! [V4e] : ( mem(V4e,A_27a) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) & ( ~~ ( V1k = V2j ) ) ) => ( ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V3d))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V2j),V4e)) = ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V2j),V4e))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V1k),V3d)) ) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EFILTER__ALL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ( ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ~~ p(ap(V0P,ap(ap(c_2Elist_2EEL(A_27a),V2n),V1l))) ) ) ) ) <=> ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = c_2Elist_2ENIL(A_27a) ) ) ) )))).
fof(conj_thm_2Epatricia_2ETRAVERSE__TRANSFORM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ap(c_2Epatricia_2ETRAVERSE(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t)) = ap(c_2Epatricia_2ETRAVERSE(A_27a),V1t) ) ) ))))).
fof(conj_thm_2Epatricia_2EMEM__TRAVERSE__PEEK,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1k),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(A_27a),V0t)))) <=> p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),V1k))) ) ) ) )))).
fof(conj_thm_2Epatricia_2EIN__NUMSET__OF__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1n),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t))) <=> p(ap(ap(c_2Epatricia_2EIN__PTREE,V1n),V0t)) ) ) ) ))).
fof(conj_thm_2Epatricia_2EADD__LIST__IS__PTREE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a))) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(c_2Epatricia_2EADD__LIST(A_27a),V0t),V1l))) ) ) )))).
fof(conj_thm_2Epatricia_2EADD__LIST__TO__EMPTY__IS__PTREE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a))) => p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(c_2Epatricia_2EADD__LIST(A_27a),c_2Epatricia_2EEmpty(A_27a)),V0l))) )))).
fof(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__IS__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),V1s))) ) ) ))).
fof(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__IS__PTREE__EMPTY,lemma,(! [V0s] : ( mem(V0s,arr(ty_2Enum_2Enum,bool)) => p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)),V0s))) ))).
fof(conj_thm_2Epatricia_2ENOT__KEY__LEFT__AND__RIGHT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Epatricia_2Eptree(A_27a)) => ! [V3r] : ( mem(V3r,ty_2Epatricia_2Eptree(A_27a)) => ! [V4k] : ( mem(V4k,ty_2Enum_2Enum) => ! [V5j] : ( mem(V5j,ty_2Enum_2Enum) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),V0p),V1m),V2l),V3r))) & ( p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V2l),V4k))) & p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V3r),V5j))) ) ) => ( ~~ ( V4k = V5j ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Epatricia_2EALL__DISTINCT__TRAVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => p(ap(c_2Elist_2EALL__DISTINCT(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(A_27a),V0t))) ) )))).
fof(conj_thm_2Epatricia_2EMEM__ALL__DISTINCT__IMP__PERM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V0l1)) & ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1l2)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l1))) <=> p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l2))) ) ) ) ) => p(ap(ap(c_2Esorting_2EPERM(A_27a),V0l1),V1l2)) ) ) )))).
fof(conj_thm_2Epatricia_2EMEM__TRAVERSE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1k),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),V0t)))) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1k),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t))) ) ) ) ))).
fof(conj_thm_2Epatricia_2EINSERT__PTREE__IS__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1x] : ( mem(V1x,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EINSERT__PTREE,V1x),V0t))) ) ) ))).
fof(conj_thm_2Epatricia_2EFINITE__NUMSET__OF__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t))) ))).
fof(conj_thm_2Epatricia_2EADD__INSERT,lemma,(! [V0v] : ( mem(V0v,ty_2Eone_2Eone) => ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Epatricia_2EADD(ty_2Eone_2Eone),V1t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eone_2Eone),V2n),V0v)) = ap(ap(c_2Epatricia_2EINSERT__PTREE,V2n),V1t) ) ) ) ))).
fof(conj_thm_2Epatricia_2EPEEK__INSERT__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( ap(ap(c_2Epatricia_2EPEEK(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EINSERT__PTREE,V1k),V0t)),V2j) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Eone_2Eone)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1k),V2j)),ap(c_2Eoption_2ESOME(ty_2Eone_2Eone),c_2Eone_2Eone)),ap(ap(c_2Epatricia_2EPEEK(ty_2Eone_2Eone),V0t),V2j)) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EMEM__TRAVERSE__INSERT__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1x] : ( mem(V1x,ty_2Enum_2Enum) => ! [V2h] : ( mem(V2h,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1x),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EINSERT__PTREE,V2h),V0t))))) <=> ( ( V1x = V2h ) | ( ( ~~ ( V1x = V2h ) ) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1x),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),V0t)))) ) ) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EPERM__INSERT__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s)) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => p(ap(ap(c_2Esorting_2EPERM(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),ap(ap(ap(c_2Elist_2EFOLDL(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)),ap(c_2Ecombin_2EC(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(ty_2Eone_2Eone),ty_2Epatricia_2Eptree(ty_2Eone_2Eone)),c_2Epatricia_2EINSERT__PTREE)),V0t),ap(c_2Elist_2ESET__TO__LIST(ty_2Enum_2Enum),V1s)))),ap(c_2Elist_2ESET__TO__LIST(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t)),V1s)))) ) ) ) ))).
fof(conj_thm_2Epatricia_2EIN__PTREE__OF__NUMSET,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) & p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s)) ) => ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),V1s))) <=> ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),V0t)) | p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2n),V1s)) ) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EIN__PTREE__EMPTY,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ~~ p(ap(ap(c_2Epatricia_2EIN__PTREE,V0n),c_2Epatricia_2EEmpty(ty_2Eone_2Eone))) ) ))).
fof(conj_thm_2Epatricia_2EIN__PTREE__OF__NUMSET__EMPTY,lemma,(! [V0s] : ( mem(V0s,arr(ty_2Enum_2Enum,bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V0s)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1n),V0s)) <=> p(ap(ap(c_2Epatricia_2EIN__PTREE,V1n),ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)),V0s))) ) ) ) ))).
fof(conj_thm_2Epatricia_2EPTREE__EXTENSION,lemma,(! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t1)) & p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V1t2)) ) => ( ( V0t1 = V1t2 ) <=> ! [V2x] : ( mem(V2x,ty_2Enum_2Enum) => ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2x),V0t1)) <=> p(ap(ap(c_2Epatricia_2EIN__PTREE,V2x),V1t2)) ) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__NUMSET__OF__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) & p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s)) ) => ( ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)),ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t)),V1s)) = ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),V1s) ) ) ) ))).
fof(conj_thm_2Epatricia_2ENUMSET__OF__PTREE__PTREE__OF__NUMSET,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) & p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s)) ) => ( ap(c_2Epatricia_2ENUMSET__OF__PTREE,ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),V1s)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(c_2Epatricia_2ENUMSET__OF__PTREE,V0t)),V1s) ) ) ) ))).
fof(conj_thm_2Epatricia_2ENUMSET__OF__PTREE__EMPTY,lemma,(( ap(c_2Epatricia_2ENUMSET__OF__PTREE,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)) = c_2Epred__set_2EEMPTY(ty_2Enum_2Enum) ))).
fof(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__EMPTY,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) = V0t ) ))).
fof(conj_thm_2Epatricia_2ENUMSET__OF__PTREE__PTREE__OF__NUMSET__EMPTY,lemma,(! [V0s] : ( mem(V0s,arr(ty_2Enum_2Enum,bool)) => ( p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V0s)) => ( ap(c_2Epatricia_2ENUMSET__OF__PTREE,ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)),V0s)) = V0s ) ) ))).
fof(conj_thm_2Epatricia_2EIN__PTREE__INSERT__PTREE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),ap(ap(c_2Epatricia_2EINSERT__PTREE,V1m),V0t))) <=> ( ( V1m = V2n ) | p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),V0t)) ) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EIN__PTREE__REMOVE,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),ap(ap(c_2Epatricia_2EREMOVE(ty_2Eone_2Eone),V0t),V1m))) <=> ( ( ~~ ( V2n = V1m ) ) & p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),V0t)) ) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EIN__PTREE__UNION__PTREE,lemma,(! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t1)) & p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V1t2)) ) => ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),ap(ap(c_2Epatricia_2EUNION__PTREE,V0t1),V1t2))) <=> ( p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),V0t1)) | p(ap(ap(c_2Epatricia_2EIN__PTREE,V2n),V1t2)) ) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EUNION__PTREE__IS__PTREE,lemma,(! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t1)) & p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V1t2)) ) => p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EUNION__PTREE,V0t1),V1t2))) ) ) ))).
fof(conj_thm_2Epatricia_2EUNION__PTREE__COMM,lemma,(! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t1)) & p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V1t2)) ) => ( ap(ap(c_2Epatricia_2EUNION__PTREE,V0t1),V1t2) = ap(ap(c_2Epatricia_2EUNION__PTREE,V1t2),V0t1) ) ) ) ))).
fof(conj_thm_2Epatricia_2EUNION__PTREE__COMM__EMPTY,lemma,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) => ( ap(ap(c_2Epatricia_2EUNION__PTREE,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)),V0t) = ap(ap(c_2Epatricia_2EUNION__PTREE,V0t),c_2Epatricia_2EEmpty(ty_2Eone_2Eone)) ) ) ))).
fof(conj_thm_2Epatricia_2EUNION__PTREE__EMPTY,lemma,(( ( ! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ap(ap(c_2Epatricia_2EUNION__PTREE,V0t),c_2Epatricia_2EEmpty(ty_2Eone_2Eone)) = V0t ) ) ) & ! [V1t] : ( mem(V1t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V1t)) => ( ap(ap(c_2Epatricia_2EUNION__PTREE,c_2Epatricia_2EEmpty(ty_2Eone_2Eone)),V1t) = V1t ) ) ) ))).
fof(conj_thm_2Epatricia_2EUNION__PTREE__ASSOC,lemma,(! [V0t1] : ( mem(V0t1,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1t2] : ( mem(V1t2,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V2t3] : ( mem(V2t3,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t1)) & ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V1t2)) & p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V2t3)) ) ) => ( ap(ap(c_2Epatricia_2EUNION__PTREE,V0t1),ap(ap(c_2Epatricia_2EUNION__PTREE,V1t2),V2t3)) = ap(ap(c_2Epatricia_2EUNION__PTREE,ap(ap(c_2Epatricia_2EUNION__PTREE,V0t1),V1t2)),V2t3) ) ) ) ) ))).
fof(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__UNION,conjecture,(! [V0t] : ( mem(V0t,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => ! [V1s1] : ( mem(V1s1,arr(ty_2Enum_2Enum,bool)) => ! [V2s2] : ( mem(V2s2,arr(ty_2Enum_2Enum,bool)) => ( ( p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),V0t)) & ( p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s1)) & p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V2s2)) ) ) => ( ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),V1s1),V2s2)) = ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,V0t),V1s1)),V2s2) ) ) ) ) ))).
