include('Axioms/veblen_2.ax').
tff(tp_ty_2Epatricia_2Eptree,type,( ty_2Epatricia_2Eptree: del > del )).
tff(tp_c_2Epatricia_2EADD,type,(c_2Epatricia_2EADD:del > $i)).
tff(mem_c_2Epatricia_2EADD,axiom,( ! [A_27a:del] : 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)))))).
tff(tp_c_2Epatricia_2EADD__LIST,type,(c_2Epatricia_2EADD__LIST:del > $i)).
tff(mem_c_2Epatricia_2EADD__LIST,axiom,( ! [A_27a:del] : 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)))))).
tff(tp_c_2Epatricia_2EBRANCH,type,(c_2Epatricia_2EBRANCH:del > $i)).
tff(mem_c_2Epatricia_2EBRANCH,axiom,( ! [A_27a:del] : 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))))).
tff(tp_c_2Epatricia_2EBRANCHING__BIT,type,(c_2Epatricia_2EBRANCHING__BIT:$i)).
tff(mem_c_2Epatricia_2EBRANCHING__BIT,axiom,mem(c_2Epatricia_2EBRANCHING__BIT,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Epatricia_2EBRANCHING__BIT,type,(fo__c_2Epatricia_2EBRANCHING__BIT:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Epatricia_2EBRANCHING__BIT,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Epatricia_2EBRANCHING__BIT(X0,X1)) = ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Epatricia_2EBranch,type,(c_2Epatricia_2EBranch:del > $i)).
tff(mem_c_2Epatricia_2EBranch,axiom,( ! [A_27a:del] : 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)))))))).
tff(tp_c_2Epatricia_2EDEPTH,type,(c_2Epatricia_2EDEPTH:del > $i)).
tff(mem_c_2Epatricia_2EDEPTH,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EDEPTH(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Enum_2Enum)))).
tff(tp_c_2Epatricia_2EEVERY__LEAF,type,(c_2Epatricia_2EEVERY__LEAF:del > $i)).
tff(mem_c_2Epatricia_2EEVERY__LEAF,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EEVERY__LEAF(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Epatricia_2Eptree(A_27a),bool))))).
tff(tp_c_2Epatricia_2EEXISTS__LEAF,type,(c_2Epatricia_2EEXISTS__LEAF:del > $i)).
tff(mem_c_2Epatricia_2EEXISTS__LEAF,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EEXISTS__LEAF(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Epatricia_2Eptree(A_27a),bool))))).
tff(tp_c_2Epatricia_2EEmpty,type,(c_2Epatricia_2EEmpty:del > $i)).
tff(mem_c_2Epatricia_2EEmpty,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EEmpty(A_27a),ty_2Epatricia_2Eptree(A_27a)))).
tff(tp_c_2Epatricia_2EFIND,type,(c_2Epatricia_2EFIND:del > $i)).
tff(mem_c_2Epatricia_2EFIND,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EFIND(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,A_27a))))).
tff(stp_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,type,(tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone : $tType)).
tff(stp_inj_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,type,(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone : tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone > $i)).
tff(stp_surj_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,type,(surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone : $i > tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone)).
tff(stp_inj_surj_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(X)) = X))).
tff(stp_inj_mem_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (mem(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(X),ty_2Epatricia_2Eptree(ty_2Eone_2Eone))))).
tff(stp_iso_mem_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,axiom,( ! [X:$i] : (mem(X,ty_2Epatricia_2Eptree(ty_2Eone_2Eone)) => (X = inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(X)))))).
tff(tp_c_2Epatricia_2EINSERT__PTREE,type,(c_2Epatricia_2EINSERT__PTREE:$i)).
tff(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))))).
tff(tp_c_2Epatricia_2EIN__PTREE,type,(c_2Epatricia_2EIN__PTREE:$i)).
tff(mem_c_2Epatricia_2EIN__PTREE,axiom,mem(c_2Epatricia_2EIN__PTREE,arr(ty_2Enum_2Enum,arr(ty_2Epatricia_2Eptree(ty_2Eone_2Eone),bool)))).
tff(stp_fo_c_2Epatricia_2EIN__PTREE,type,(fo__c_2Epatricia_2EIN__PTREE:(tp__ty_2Enum_2Enum * tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone) > tp__o)).
tff(stp_eq_fo_c_2Epatricia_2EIN__PTREE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (inj__o(fo__c_2Epatricia_2EIN__PTREE(X0,X1)) = ap(ap(c_2Epatricia_2EIN__PTREE,inj__ty_2Enum_2Enum(X0)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(X1)))))).
tff(tp_c_2Epatricia_2EIS__EMPTY,type,(c_2Epatricia_2EIS__EMPTY:del > $i)).
tff(mem_c_2Epatricia_2EIS__EMPTY,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EIS__EMPTY(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),bool)))).
tff(tp_c_2Epatricia_2EIS__PTREE,type,(c_2Epatricia_2EIS__PTREE:del > $i)).
tff(mem_c_2Epatricia_2EIS__PTREE,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EIS__PTREE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),bool)))).
tff(tp_c_2Epatricia_2EJOIN,type,(c_2Epatricia_2EJOIN:del > $i)).
tff(mem_c_2Epatricia_2EJOIN,axiom,( ! [A_27a:del] : 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))))).
tff(tp_c_2Epatricia_2EKEYS,type,(c_2Epatricia_2EKEYS:del > $i)).
tff(mem_c_2Epatricia_2EKEYS,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EKEYS(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))))).
tff(tp_c_2Epatricia_2ELeaf,type,(c_2Epatricia_2ELeaf:del > $i)).
tff(mem_c_2Epatricia_2ELeaf,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2ELeaf(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,ty_2Epatricia_2Eptree(A_27a)))))).
tff(tp_c_2Epatricia_2ENUMSET__OF__PTREE,type,(c_2Epatricia_2ENUMSET__OF__PTREE:$i)).
tff(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)))).
tff(stp_fo_c_2Epatricia_2ENUMSET__OF__PTREE,type,(fo__c_2Epatricia_2ENUMSET__OF__PTREE:(tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Epatricia_2ENUMSET__OF__PTREE,axiom,( ! [X0:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Epatricia_2ENUMSET__OF__PTREE(X0,X1)) = ap(ap(c_2Epatricia_2ENUMSET__OF__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Epatricia_2EPEEK,type,(c_2Epatricia_2EPEEK:del > $i)).
tff(mem_c_2Epatricia_2EPEEK,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EPEEK(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,ty_2Eoption_2Eoption(A_27a)))))).
tff(tp_c_2Epatricia_2EPTREE__OF__NUMSET,type,(c_2Epatricia_2EPTREE__OF__NUMSET:$i)).
tff(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))))).
tff(tp_c_2Epatricia_2EREMOVE,type,(c_2Epatricia_2EREMOVE:del > $i)).
tff(mem_c_2Epatricia_2EREMOVE,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2EREMOVE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)))))).
tff(tp_c_2Epatricia_2ESIZE,type,(c_2Epatricia_2ESIZE:del > $i)).
tff(mem_c_2Epatricia_2ESIZE,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2ESIZE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Enum_2Enum)))).
tff(tp_c_2Epatricia_2ETRANSFORM,type,(c_2Epatricia_2ETRANSFORM:(del * del) > $i)).
tff(mem_c_2Epatricia_2ETRANSFORM,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Epatricia_2ETRAVERSE,type,(c_2Epatricia_2ETRAVERSE:del > $i)).
tff(mem_c_2Epatricia_2ETRAVERSE,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2ETRAVERSE(A_27a),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))))).
tff(tp_c_2Epatricia_2ETRAVERSE__AUX,type,(c_2Epatricia_2ETRAVERSE__AUX:del > $i)).
tff(mem_c_2Epatricia_2ETRAVERSE__AUX,axiom,( ! [A_27a:del] : 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)))))).
tff(tp_c_2Epatricia_2EUNION__PTREE,type,(c_2Epatricia_2EUNION__PTREE:$i)).
tff(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))))).
tff(tp_c_2Epatricia_2Eptree__CASE,type,(c_2Epatricia_2Eptree__CASE:(del * del) > $i)).
tff(mem_c_2Epatricia_2Eptree__CASE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Epatricia_2Eptree__size,type,(c_2Epatricia_2Eptree__size:del > $i)).
tff(mem_c_2Epatricia_2Eptree__size,axiom,( ! [A_27a:del] : mem(c_2Epatricia_2Eptree__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Epatricia_2Eptree(A_27a),ty_2Enum_2Enum))))).
tff(ax_thm_2Epatricia_2Eptree__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : (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)))))).
tff(ax_thm_2Epatricia_2Eptree__case__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : (mem(V0v,A_27b) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V2f1:$i] : (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:tp__ty_2Enum_2Enum] : ( ! [V4a1:$i] : (mem(V4a1,A_27a) => ( ! [V5v:$i] : (mem(V5v,A_27b) => ( ! [V6f:$i] : (mem(V6f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V7f1:$i] : (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),inj__ty_2Enum_2Enum(V3a0)),V4a1)),V5v),V6f),V7f1) = ap(ap(V6f,inj__ty_2Enum_2Enum(V3a0)),V4a1))))))))))) & ( ! [V8a0:tp__ty_2Enum_2Enum] : ( ! [V9a1:tp__ty_2Enum_2Enum] : ( ! [V10a2:$i] : (mem(V10a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V11a3:$i] : (mem(V11a3,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V12v:$i] : (mem(V12v,A_27b) => ( ! [V13f:$i] : (mem(V13f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V14f1:$i] : (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),inj__ty_2Enum_2Enum(V8a0)),inj__ty_2Enum_2Enum(V9a1)),V10a2),V11a3)),V12v),V13f),V14f1) = ap(ap(ap(ap(V14f1,inj__ty_2Enum_2Enum(V8a0)),inj__ty_2Enum_2Enum(V9a1)),V10a2),V11a3))))))))))))))))))).
tff(ax_thm_2Epatricia_2Eptree__size__def,axiom,( ! [A_27a:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2Eptree__size(A_27a),V0f),c_2Epatricia_2EEmpty(A_27a))) = fo__c_2Enum_2E0))) & (( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V2a0:tp__ty_2Enum_2Enum] : ( ! [V3a1:$i] : (mem(V3a1,A_27a) => (surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2Eptree__size(A_27a),V1f),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2a0)),V3a1))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2a0)),ap(V1f,V3a1)))))))))) & ( ! [V4f:$i] : (mem(V4f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V5a0:tp__ty_2Enum_2Enum] : ( ! [V6a1:tp__ty_2Enum_2Enum] : ( ! [V7a2:$i] : (mem(V7a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8a3:$i] : (mem(V8a3,ty_2Epatricia_2Eptree(A_27a)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2Eptree__size(A_27a),V4f),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V5a0)),inj__ty_2Enum_2Enum(V6a1)),V7a2),V8a3))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V5a0)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(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))))))))))))))))))).
tff(conj_thm_2Epatricia_2Edatatype__ptree,lemma,(( ! [A_27a:del]: ( ! [V0ptree:$i] : (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))))))))).
tff(conj_thm_2Epatricia_2Eptree__11,lemma,(( ! [A_27a:del]: (( ! [V0a0:tp__ty_2Enum_2Enum] : ( ! [V1a1:$i] : (mem(V1a1,A_27a) => ( ! [V2a0_27:tp__ty_2Enum_2Enum] : ( ! [V3a1_27:$i] : (mem(V3a1_27,A_27a) => ((ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V0a0)),V1a1) = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2a0_27)),V3a1_27)) <=> ((V0a0 = V2a0_27) & (V1a1 = V3a1_27))))))))) & ( ! [V4a0:tp__ty_2Enum_2Enum] : ( ! [V5a1:tp__ty_2Enum_2Enum] : ( ! [V6a2:$i] : (mem(V6a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V7a3:$i] : (mem(V7a3,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8a0_27:tp__ty_2Enum_2Enum] : ( ! [V9a1_27:tp__ty_2Enum_2Enum] : ( ! [V10a2_27:$i] : (mem(V10a2_27,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V11a3_27:$i] : (mem(V11a3_27,ty_2Epatricia_2Eptree(A_27a)) => ((ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V4a0)),inj__ty_2Enum_2Enum(V5a1)),V6a2),V7a3) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V8a0_27)),inj__ty_2Enum_2Enum(V9a1_27)),V10a2_27),V11a3_27)) <=> ((V4a0 = V8a0_27) & ((V5a1 = V9a1_27) & ((V6a2 = V10a2_27) & (V7a3 = V11a3_27))))))))))))))))))))).
tff(conj_thm_2Epatricia_2Eptree__distinct,lemma,(( ! [A_27a:del]: (( ! [V0a1:$i] : (mem(V0a1,A_27a) => ( ! [V1a0:tp__ty_2Enum_2Enum] : (~~ (c_2Epatricia_2EEmpty(A_27a) = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1a0)),V0a1)))))) & (( ! [V2a3:$i] : (mem(V2a3,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V3a2:$i] : (mem(V3a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V4a1:tp__ty_2Enum_2Enum] : ( ! [V5a0:tp__ty_2Enum_2Enum] : (~~ (c_2Epatricia_2EEmpty(A_27a) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V5a0)),inj__ty_2Enum_2Enum(V4a1)),V3a2),V2a3))))))))) & ( ! [V6a3:$i] : (mem(V6a3,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V7a2:$i] : (mem(V7a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8a1_27:tp__ty_2Enum_2Enum] : ( ! [V9a1:$i] : (mem(V9a1,A_27a) => ( ! [V10a0_27:tp__ty_2Enum_2Enum] : ( ! [V11a0:tp__ty_2Enum_2Enum] : (~~ (ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V11a0)),V9a1) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V10a0_27)),inj__ty_2Enum_2Enum(V8a1_27)),V7a2),V6a3))))))))))))))))).
tff(conj_thm_2Epatricia_2Eptree__nchotomy,lemma,(( ! [A_27a:del]: ( ! [V0pp:$i] : (mem(V0pp,ty_2Epatricia_2Eptree(A_27a)) => ((V0pp = c_2Epatricia_2EEmpty(A_27a)) | ((? [V1n:tp__ty_2Enum_2Enum] : (? [V2a:$i] : (mem(V2a,A_27a) & (V0pp = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1n)),V2a))))) | (? [V3n0:tp__ty_2Enum_2Enum] : (? [V4n:tp__ty_2Enum_2Enum] : (? [V5p:$i] : (mem(V5p,ty_2Epatricia_2Eptree(A_27a)) & (? [V6p0:$i] : (mem(V6p0,ty_2Epatricia_2Eptree(A_27a)) & (V0pp = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V3n0)),inj__ty_2Enum_2Enum(V4n)),V5p),V6p0))))))))))))))).
tff(conj_thm_2Epatricia_2Eptree__Axiom,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f0:$i] : (mem(V0f0,A_27b) => ( ! [V1f1:$i] : (mem(V1f1,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V2f2:$i] : (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:$i] : (mem(V3fn,arr(ty_2Epatricia_2Eptree(A_27a),A_27b)) & ((ap(V3fn,c_2Epatricia_2EEmpty(A_27a)) = V0f0) & (( ! [V4a0:tp__ty_2Enum_2Enum] : ( ! [V5a1:$i] : (mem(V5a1,A_27a) => (ap(V3fn,ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V4a0)),V5a1)) = ap(ap(V1f1,inj__ty_2Enum_2Enum(V4a0)),V5a1))))) & ( ! [V6a0:tp__ty_2Enum_2Enum] : ( ! [V7a1:tp__ty_2Enum_2Enum] : ( ! [V8a2:$i] : (mem(V8a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V9a3:$i] : (mem(V9a3,ty_2Epatricia_2Eptree(A_27a)) => (ap(V3fn,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V6a0)),inj__ty_2Enum_2Enum(V7a1)),V8a2),V9a3)) = ap(ap(ap(ap(ap(ap(V2f2,inj__ty_2Enum_2Enum(V6a0)),inj__ty_2Enum_2Enum(V7a1)),V8a2),V9a3),ap(V3fn,V8a2)),ap(V3fn,V9a3))))))))))))))))))))))).
tff(conj_thm_2Epatricia_2Eptree__induction,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),bool)) => ((p(ap(V0P,c_2Epatricia_2EEmpty(A_27a))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,A_27a) => p(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1n)),V2a)))))) & ( ! [V3p:$i] : (mem(V3p,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V4p0:$i] : (mem(V4p0,ty_2Epatricia_2Eptree(A_27a)) => ((p(ap(V0P,V3p)) & p(ap(V0P,V4p0))) => ( ! [V5n:tp__ty_2Enum_2Enum] : ( ! [V6n0:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V6n0)),inj__ty_2Enum_2Enum(V5n)),V3p),V4p0)))))))))))) => ( ! [V7p:$i] : (mem(V7p,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,V7p)))))))))).
tff(conj_thm_2Epatricia_2Eptree__case__cong,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v_27:$i] : (mem(V0v_27,A_27b) => ( ! [V1f_27:$i] : (mem(V1f_27,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V2f1_27:$i] : (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:$i] : (mem(V3M,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V4M_27:$i] : (mem(V4M_27,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V5v:$i] : (mem(V5v,A_27b) => ( ! [V6f:$i] : (mem(V6f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V7f1:$i] : (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:tp__ty_2Enum_2Enum] : ( ! [V9a1:$i] : (mem(V9a1,A_27a) => ((V4M_27 = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V8a0)),V9a1)) => (ap(ap(V6f,inj__ty_2Enum_2Enum(V8a0)),V9a1) = ap(ap(V1f_27,inj__ty_2Enum_2Enum(V8a0)),V9a1)))))) & ( ! [V10a0:tp__ty_2Enum_2Enum] : ( ! [V11a1:tp__ty_2Enum_2Enum] : ( ! [V12a2:$i] : (mem(V12a2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V13a3:$i] : (mem(V13a3,ty_2Epatricia_2Eptree(A_27a)) => ((V4M_27 = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V10a0)),inj__ty_2Enum_2Enum(V11a1)),V12a2),V13a3)) => (ap(ap(ap(ap(V7f1,inj__ty_2Enum_2Enum(V10a0)),inj__ty_2Enum_2Enum(V11a1)),V12a2),V13a3) = ap(ap(ap(ap(V2f1_27,inj__ty_2Enum_2Enum(V10a0)),inj__ty_2Enum_2Enum(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))))))))))))))))))))))).
tff(conj_thm_2Epatricia_2Eptree__case__eq,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V3f1:$i] : (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:$i] : (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:tp__ty_2Enum_2Enum] : (? [V6a:$i] : (mem(V6a,A_27a) & ((V0x = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V5n)),V6a)) & (ap(ap(V2f,inj__ty_2Enum_2Enum(V5n)),V6a) = V4v_27))))) | (? [V7n0:tp__ty_2Enum_2Enum] : (? [V8n:tp__ty_2Enum_2Enum] : (? [V9p:$i] : (mem(V9p,ty_2Epatricia_2Eptree(A_27a)) & (? [V10p0:$i] : (mem(V10p0,ty_2Epatricia_2Eptree(A_27a)) & ((V0x = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V7n0)),inj__ty_2Enum_2Enum(V8n)),V9p),V10p0)) & (ap(ap(ap(ap(V3f1,inj__ty_2Enum_2Enum(V7n0)),inj__ty_2Enum_2Enum(V8n)),V9p),V10p0) = V4v_27))))))))))))))))))))))))).
tff(conj_thm_2Epatricia_2EBRANCHING__BIT__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) => (( ! [V1p0:tp__ty_2Enum_2Enum] : ( ! [V2p1:tp__ty_2Enum_2Enum] : (((~~ ((p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V1p0))) <=> p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V2p1)))) | (V1p0 = V2p1))) => p(ap(ap(V0P,ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(V1p0))),ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(V2p1))))) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V1p0)),inj__ty_2Enum_2Enum(V2p1)))))) => ( ! [V3v:tp__ty_2Enum_2Enum] : ( ! [V4v1:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,inj__ty_2Enum_2Enum(V3v)),inj__ty_2Enum_2Enum(V4v1)))))))))).
tff(conj_thm_2Epatricia_2EBRANCHING__BIT__def,lemma,(( ! [V0p1:tp__ty_2Enum_2Enum] : ( ! [V1p0:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(V1p0)),inj__ty_2Enum_2Enum(V0p1))) = surj__ty_2Enum_2Enum(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,inj__ty_2Enum_2Enum(V1p0))),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0p1)))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1p0)),inj__ty_2Enum_2Enum(V0p1)))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Enum_2ESUC,ap(ap(c_2Epatricia_2EBRANCHING__BIT,ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(V1p0))),ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(V0p1))))))))))).
tff(conj_thm_2Epatricia_2EPEEK__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Enum_2Enum,bool))) => ((( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,c_2Epatricia_2EEmpty(A_27a)),inj__ty_2Enum_2Enum(V1k)))) & (( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27a) => ( ! [V4k:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2j)),V3d)),inj__ty_2Enum_2Enum(V4k))))))) & ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : (mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8r:$i] : (mem(V8r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V9k:tp__ty_2Enum_2Enum] : (p(ap(ap(V0P,ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V6m)),inj__ty_2Enum_2Enum(V9k))),V7l),V8r)),inj__ty_2Enum_2Enum(V9k))) => p(ap(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V5p)),inj__ty_2Enum_2Enum(V6m)),V7l),V8r)),inj__ty_2Enum_2Enum(V9k))))))))))))) => ( ! [V10v:$i] : (mem(V10v,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V11v1:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,V10v),inj__ty_2Enum_2Enum(V11v1)))))))))))).
tff(conj_thm_2Epatricia_2EPEEK__def,lemma,(( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EPEEK(A_27a),c_2Epatricia_2EEmpty(A_27a)),inj__ty_2Enum_2Enum(V0k)) = c_2Eoption_2ENONE(A_27a))) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27a) => (ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2j)),V3d)),inj__ty_2Enum_2Enum(V1k)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V2j))),ap(c_2Eoption_2ESOME(A_27a),V3d)),c_2Eoption_2ENONE(A_27a))))))) & ( ! [V4r:$i] : (mem(V4r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : (mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V5p)),inj__ty_2Enum_2Enum(V6m)),V7l),V4r)),inj__ty_2Enum_2Enum(V8k)) = ap(ap(c_2Epatricia_2EPEEK(A_27a),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V6m)),inj__ty_2Enum_2Enum(V8k))),V7l),V4r)),inj__ty_2Enum_2Enum(V8k))))))))))))))).
tff(ax_thm_2Epatricia_2EJOIN__def,axiom,( ! [A_27a:del]: ( ! [V0p0:tp__ty_2Enum_2Enum] : ( ! [V1t0:$i] : (mem(V1t0,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2p1:tp__ty_2Enum_2Enum] : ( ! [V3t1:$i] : (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)))),inj__ty_2Enum_2Enum(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)),inj__ty_2Enum_2Enum(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,inj__ty_2Enum_2Enum(V0p0)),inj__ty_2Enum_2Enum(V2p1)))))))))))).
tff(conj_thm_2Epatricia_2EADD__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),bool))) => ((( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2e:$i] : (mem(V2e,A_27a) => p(ap(ap(V0P,c_2Epatricia_2EEmpty(A_27a)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V2e)))))) & (( ! [V3j:tp__ty_2Enum_2Enum] : ( ! [V4d:$i] : (mem(V4d,A_27a) => ( ! [V5k:tp__ty_2Enum_2Enum] : ( ! [V6e:$i] : (mem(V6e,A_27a) => p(ap(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V3j)),V4d)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V5k)),V6e))))))))) & ( ! [V7p:tp__ty_2Enum_2Enum] : ( ! [V8m:tp__ty_2Enum_2Enum] : ( ! [V9l:$i] : (mem(V9l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V10r:$i] : (mem(V10r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V11k:tp__ty_2Enum_2Enum] : ( ! [V12e:$i] : (mem(V12e,A_27a) => ((((p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(V8m)),inj__ty_2Enum_2Enum(V11k)),inj__ty_2Enum_2Enum(V7p))) & (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V8m)),inj__ty_2Enum_2Enum(V11k))))) => p(ap(ap(V0P,V10r),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V11k)),V12e)))) & ((p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(V8m)),inj__ty_2Enum_2Enum(V11k)),inj__ty_2Enum_2Enum(V7p))) & p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V8m)),inj__ty_2Enum_2Enum(V11k)))) => p(ap(ap(V0P,V9l),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V11k)),V12e))))) => p(ap(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V7p)),inj__ty_2Enum_2Enum(V8m)),V9l),V10r)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V11k)),V12e))))))))))))))) => ( ! [V13v:$i] : (mem(V13v,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V14v1:tp__ty_2Enum_2Enum] : ( ! [V15v2:$i] : (mem(V15v2,A_27a) => p(ap(ap(V0P,V13v),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V14v1)),V15v2)))))))))))))).
tff(conj_thm_2Epatricia_2EADD__def,lemma,(( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1e:$i] : (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),inj__ty_2Enum_2Enum(V0k)),V1e)) = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V0k)),V1e))))) & (( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3j:tp__ty_2Enum_2Enum] : ( ! [V4e:$i] : (mem(V4e,A_27a) => ( ! [V5d:$i] : (mem(V5d,A_27a) => (ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V3j)),V5d)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V2k)),V4e)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V3j)),inj__ty_2Enum_2Enum(V2k))),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V2k)),V4e)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)),inj__ty_2Enum_2Enum(V3j)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V3j)),V5d))))))))))))) & ( ! [V6r:$i] : (mem(V6r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V7p:tp__ty_2Enum_2Enum] : ( ! [V8m:tp__ty_2Enum_2Enum] : ( ! [V9l:$i] : (mem(V9l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V10k:tp__ty_2Enum_2Enum] : ( ! [V11e:$i] : (mem(V11e,A_27a) => (ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V7p)),inj__ty_2Enum_2Enum(V8m)),V9l),V6r)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V10k)),V11e)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(V8m)),inj__ty_2Enum_2Enum(V10k)),inj__ty_2Enum_2Enum(V7p))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V8m)),inj__ty_2Enum_2Enum(V10k))),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V7p)),inj__ty_2Enum_2Enum(V8m)),ap(ap(c_2Epatricia_2EADD(A_27a),V9l),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V10k)),V11e))),V6r)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V7p)),inj__ty_2Enum_2Enum(V8m)),V9l),ap(ap(c_2Epatricia_2EADD(A_27a),V6r),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V10k)),V11e)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epatricia_2Eptree(A_27a)),inj__ty_2Enum_2Enum(V7p)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V7p)),inj__ty_2Enum_2Enum(V8m)),V9l),V6r))))))))))))))))))))).
tff(ax_thm_2Epatricia_2EBRANCH__primitive__def,axiom,( ! [A_27a:del]: (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)))))).
tff(conj_thm_2Epatricia_2EBRANCH__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (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:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3t:$i] : (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)))),inj__ty_2Enum_2Enum(V1p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V2m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),c_2Epatricia_2EEmpty(A_27a)),V3t))))))))) & (( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6v6:tp__ty_2Enum_2Enum] : ( ! [V7v7:$i] : (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)))),inj__ty_2Enum_2Enum(V4p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V5m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V6v6)),V7v7)),c_2Epatricia_2EEmpty(A_27a))))))))))) & (( ! [V8p:tp__ty_2Enum_2Enum] : ( ! [V9m:tp__ty_2Enum_2Enum] : ( ! [V10v8:tp__ty_2Enum_2Enum] : ( ! [V11v9:tp__ty_2Enum_2Enum] : ( ! [V12v10:$i] : (mem(V12v10,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V13v11:$i] : (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)))),inj__ty_2Enum_2Enum(V8p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V10v8)),inj__ty_2Enum_2Enum(V11v9)),V12v10),V13v11)),c_2Epatricia_2EEmpty(A_27a)))))))))))))) & (( ! [V14p:tp__ty_2Enum_2Enum] : ( ! [V15m:tp__ty_2Enum_2Enum] : ( ! [V16v12:tp__ty_2Enum_2Enum] : ( ! [V17v13:$i] : (mem(V17v13,A_27a) => ( ! [V18v24:tp__ty_2Enum_2Enum] : ( ! [V19v25:$i] : (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)))),inj__ty_2Enum_2Enum(V14p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V15m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V16v12)),V17v13)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V18v24)),V19v25)))))))))))))) & (( ! [V20p:tp__ty_2Enum_2Enum] : ( ! [V21m:tp__ty_2Enum_2Enum] : ( ! [V22v12:tp__ty_2Enum_2Enum] : ( ! [V23v13:$i] : (mem(V23v13,A_27a) => ( ! [V24v26:tp__ty_2Enum_2Enum] : ( ! [V25v27:tp__ty_2Enum_2Enum] : ( ! [V26v28:$i] : (mem(V26v28,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V27v29:$i] : (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)))),inj__ty_2Enum_2Enum(V20p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V21m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V22v12)),V23v13)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V24v26)),inj__ty_2Enum_2Enum(V25v27)),V26v28),V27v29))))))))))))))))) & (( ! [V28p:tp__ty_2Enum_2Enum] : ( ! [V29m:tp__ty_2Enum_2Enum] : ( ! [V30v14:tp__ty_2Enum_2Enum] : ( ! [V31v15:tp__ty_2Enum_2Enum] : ( ! [V32v16:$i] : (mem(V32v16,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V33v17:$i] : (mem(V33v17,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V34v36:tp__ty_2Enum_2Enum] : ( ! [V35v37:$i] : (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)))),inj__ty_2Enum_2Enum(V28p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V30v14)),inj__ty_2Enum_2Enum(V31v15)),V32v16),V33v17)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V34v36)),V35v37))))))))))))))))) & ( ! [V36p:tp__ty_2Enum_2Enum] : ( ! [V37m:tp__ty_2Enum_2Enum] : ( ! [V38v14:tp__ty_2Enum_2Enum] : ( ! [V39v15:tp__ty_2Enum_2Enum] : ( ! [V40v16:$i] : (mem(V40v16,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V41v17:$i] : (mem(V41v17,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V42v38:tp__ty_2Enum_2Enum] : ( ! [V43v39:tp__ty_2Enum_2Enum] : ( ! [V44v40:$i] : (mem(V44v40,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V45v41:$i] : (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)))),inj__ty_2Enum_2Enum(V36p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V38v14)),inj__ty_2Enum_2Enum(V39v15)),V40v16),V41v17)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V42v38)),inj__ty_2Enum_2Enum(V43v39)),V44v40),V45v41)))))))))))))))))))))))))) => ( ! [V46v:tp__ty_2Enum_2Enum] : ( ! [V47v1:tp__ty_2Enum_2Enum] : ( ! [V48v2:$i] : (mem(V48v2,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V49v3:$i] : (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)))),inj__ty_2Enum_2Enum(V46v)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V47v1)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V48v2),V49v3))))))))))))))))).
tff(conj_thm_2Epatricia_2EBRANCH__def,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2t:$i] : (mem(V2t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V3v6:tp__ty_2Enum_2Enum] : ( ! [V4v7:$i] : (mem(V4v7,A_27a) => ( ! [V5v8:tp__ty_2Enum_2Enum] : ( ! [V6v9:tp__ty_2Enum_2Enum] : ( ! [V7v10:$i] : (mem(V7v10,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8v11:$i] : (mem(V8v11,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V9v12:tp__ty_2Enum_2Enum] : ( ! [V10v13:$i] : (mem(V10v13,A_27a) => ( ! [V11v24:tp__ty_2Enum_2Enum] : ( ! [V12v25:$i] : (mem(V12v25,A_27a) => ( ! [V13v26:tp__ty_2Enum_2Enum] : ( ! [V14v27:tp__ty_2Enum_2Enum] : ( ! [V15v28:$i] : (mem(V15v28,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V16v29:$i] : (mem(V16v29,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V17v14:tp__ty_2Enum_2Enum] : ( ! [V18v15:tp__ty_2Enum_2Enum] : ( ! [V19v16:$i] : (mem(V19v16,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V20v17:$i] : (mem(V20v17,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V21v36:tp__ty_2Enum_2Enum] : ( ! [V22v37:$i] : (mem(V22v37,A_27a) => ( ! [V23v38:tp__ty_2Enum_2Enum] : ( ! [V24v39:tp__ty_2Enum_2Enum] : ( ! [V25v40:$i] : (mem(V25v40,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V26v41:$i] : (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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V3v6)),V4v7)),c_2Epatricia_2EEmpty(A_27a))))) = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V5v8)),inj__ty_2Enum_2Enum(V6v9)),V7v10),V8v11)),c_2Epatricia_2EEmpty(A_27a))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V5v8)),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V9v12)),V10v13)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V11v24)),V12v25))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V9v12)),V10v13)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V9v12)),V10v13)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V13v26)),inj__ty_2Enum_2Enum(V14v27)),V15v28),V16v29))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V9v12)),V10v13)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V13v26)),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V17v14)),inj__ty_2Enum_2Enum(V18v15)),V19v16),V20v17)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V21v36)),V22v37))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V17v14)),inj__ty_2Enum_2Enum(V18v15)),V19v16),V20v17)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V17v14)),inj__ty_2Enum_2Enum(V18v15)),V19v16),V20v17)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V23v38)),inj__ty_2Enum_2Enum(V24v39)),V25v40),V26v41))))) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V17v14)),inj__ty_2Enum_2Enum(V18v15)),V19v16),V20v17)),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V23v38)),inj__ty_2Enum_2Enum(V24v39)),V25v40),V26v41)))))))))))))))))))))))))))))))))))))))))))))))))))).
tff(ax_thm_2Epatricia_2EREMOVE__def,axiom,( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EREMOVE(A_27a),c_2Epatricia_2EEmpty(A_27a)),inj__ty_2Enum_2Enum(V0k)) = c_2Epatricia_2EEmpty(A_27a))) & (( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,A_27a) => ( ! [V3k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1j)),V2d)),inj__ty_2Enum_2Enum(V3k)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1j)),inj__ty_2Enum_2Enum(V3k))),c_2Epatricia_2EEmpty(A_27a)),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1j)),V2d))))))) & ( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6l:$i] : (mem(V6l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V7r:$i] : (mem(V7r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EREMOVE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V4p)),inj__ty_2Enum_2Enum(V5m)),V6l),V7r)),inj__ty_2Enum_2Enum(V8k)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(V5m)),inj__ty_2Enum_2Enum(V8k)),inj__ty_2Enum_2Enum(V4p))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V5m)),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V4p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V4p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V8k)))))))),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V4p)),inj__ty_2Enum_2Enum(V5m)),V6l),V7r)))))))))))))).
tff(ax_thm_2Epatricia_2ETRAVERSE__AUX__def,axiom,( ! [A_27a:del]: (( ! [V0a:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),c_2Epatricia_2EEmpty(A_27a)),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V0a))) = V0a)) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,A_27a) => ( ! [V3a:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1k)),V2d)),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V3a))) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V3a)))))))) & ( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6l:$i] : (mem(V6l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V7r:$i] : (mem(V7r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8a:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V4p)),inj__ty_2Enum_2Enum(V5m)),V6l),V7r)),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V8a))) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),V6l),ap(ap(c_2Epatricia_2ETRAVERSE__AUX(A_27a),V7r),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V8a)))))))))))))))).
tff(ax_thm_2Epatricia_2ETRAVERSE__def,axiom,( ! [A_27a:del]: ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(c_2Epatricia_2ETRAVERSE(A_27a),c_2Epatricia_2EEmpty(A_27a))) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(c_2Elist_2ENIL(ty_2Enum_2Enum))) & (( ! [V0j:tp__ty_2Enum_2Enum] : ( ! [V1d:$i] : (mem(V1d,A_27a) => (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(c_2Epatricia_2ETRAVERSE(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V0j)),V1d))) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0j)),c_2Elist_2ENIL(ty_2Enum_2Enum))))))) & ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : (mem(V4l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V5r:$i] : (mem(V5r,ty_2Epatricia_2Eptree(A_27a)) => (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(c_2Epatricia_2ETRAVERSE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V3m)),V4l),V5r))) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Elist_2EAPPEND(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(A_27a),V4l)),ap(c_2Epatricia_2ETRAVERSE(A_27a),V5r)))))))))))))).
tff(ax_thm_2Epatricia_2EKEYS__def,axiom,( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(c_2Epatricia_2EKEYS(A_27a),V0t)) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(ap(c_2Esorting_2EQSORT(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C),ap(c_2Epatricia_2ETRAVERSE(A_27a),V0t)))))))).
tff(ax_thm_2Epatricia_2ETRANSFORM__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (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:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27b) => (ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V1f),ap(ap(c_2Epatricia_2ELeaf(A_27b),inj__ty_2Enum_2Enum(V2j)),V3d)) = ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2j)),ap(V1f,V3d)))))))) & ( ! [V4f:$i] : (mem(V4f,arr(A_27b,A_27a)) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : (mem(V7l,ty_2Epatricia_2Eptree(A_27b)) => ( ! [V8r:$i] : (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),inj__ty_2Enum_2Enum(V5p)),inj__ty_2Enum_2Enum(V6m)),V7l),V8r)) = ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V5p)),inj__ty_2Enum_2Enum(V6m)),ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V4f),V7l)),ap(ap(c_2Epatricia_2ETRANSFORM(A_27a,A_27b),V4f),V8r)))))))))))))))).
tff(ax_thm_2Epatricia_2EEVERY__LEAF__def,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : (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:$i] : (mem(V1P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27a) => (p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V1P),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2j)),V3d))) <=> p(ap(ap(V1P,inj__ty_2Enum_2Enum(V2j)),V3d)))))))) & ( ! [V4P:$i] : (mem(V4P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : (mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8r:$i] : (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),inj__ty_2Enum_2Enum(V5p)),inj__ty_2Enum_2Enum(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)))))))))))))))).
tff(ax_thm_2Epatricia_2EEXISTS__LEAF__def,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : (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:$i] : (mem(V1P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27a) => (p(ap(ap(c_2Epatricia_2EEXISTS__LEAF(A_27a),V1P),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V2j)),V3d))) <=> p(ap(ap(V1P,inj__ty_2Enum_2Enum(V2j)),V3d)))))))) & ( ! [V4P:$i] : (mem(V4P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : (mem(V7l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V8r:$i] : (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),inj__ty_2Enum_2Enum(V5p)),inj__ty_2Enum_2Enum(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)))))))))))))))).
tff(ax_thm_2Epatricia_2ESIZE__def,axiom,( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Epatricia_2ESIZE(A_27a),V0t)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(A_27a),V0t)))))))).
tff(ax_thm_2Epatricia_2EDEPTH__def,axiom,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum(ap(c_2Epatricia_2EDEPTH(A_27a),c_2Epatricia_2EEmpty(A_27a))) = fo__c_2Enum_2E0) & (( ! [V0j:tp__ty_2Enum_2Enum] : ( ! [V1d:$i] : (mem(V1d,A_27a) => (surj__ty_2Enum_2Enum(ap(c_2Epatricia_2EDEPTH(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V0j)),V1d))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : (mem(V4l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V5r:$i] : (mem(V5r,ty_2Epatricia_2Eptree(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Epatricia_2EDEPTH(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V3m)),V4l),V5r))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2EMAX,ap(c_2Epatricia_2EDEPTH(A_27a),V4l)),ap(c_2Epatricia_2EDEPTH(A_27a),V5r))))))))))))))).
tff(ax_thm_2Epatricia_2EIS__PTREE__def,axiom,( ! [A_27a:del]: ((p(ap(c_2Epatricia_2EIS__PTREE(A_27a),c_2Epatricia_2EEmpty(A_27a))) <=> $true) & (( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1d:$i] : (mem(V1d,A_27a) => (p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V0k)),V1d))) <=> $true)))) & ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : (mem(V4l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V5r:$i] : (mem(V5r,ty_2Epatricia_2Eptree(A_27a)) => (p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V3m)),V4l),V5r))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2p)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(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))))))))))))))))))).
tff(ax_thm_2Epatricia_2EIN__PTREE__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (p(ap(ap(c_2Epatricia_2EIN__PTREE,inj__ty_2Enum_2Enum(V0n)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t))) <=> p(ap(c_2Eoption_2EIS__SOME(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EPEEK(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t)),inj__ty_2Enum_2Enum(V0n)))))))).
tff(ax_thm_2Epatricia_2EINSERT__PTREE__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EINSERT__PTREE,inj__ty_2Enum_2Enum(V0n)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t))) = surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EADD(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eone_2Eone),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Eone_2Eone(fo__c_2Eone_2Eone)))))))).
tff(ax_thm_2Epatricia_2EPTREE__OF__NUMSET__def,axiom,( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Enum_2Enum,bool)) => (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)),V1s)) = surj__c_ty_2Epatricia_2Eptree_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)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)),ap(c_2Elist_2ESET__TO__LIST(ty_2Enum_2Enum),V1s)))))))).
tff(ax_thm_2Epatricia_2ENUMSET__OF__PTREE__def,axiom,( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (ap(c_2Epatricia_2ENUMSET__OF__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)) = ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)))))).
tff(ax_thm_2Epatricia_2EUNION__PTREE__def,axiom,( ! [V0t1:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1t2:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EUNION__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t1)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t2))) = surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t1)),ap(c_2Epatricia_2ENUMSET__OF__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t2)))))))).
tff(ax_thm_2Epatricia_2EIS__EMPTY__primitive__def,axiom,( ! [A_27a:del]: (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)))))).
tff(conj_thm_2Epatricia_2EIS__EMPTY__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epatricia_2Eptree(A_27a),bool)) => ((p(ap(V0P,c_2Epatricia_2EEmpty(A_27a))) & (( ! [V1v:tp__ty_2Enum_2Enum] : ( ! [V2v1:$i] : (mem(V2v1,A_27a) => p(ap(V0P,ap(ap(c_2Epatricia_2ELeaf(A_27a),inj__ty_2Enum_2Enum(V1v)),V2v1)))))) & ( ! [V3v2:tp__ty_2Enum_2Enum] : ( ! [V4v3:tp__ty_2Enum_2Enum] : ( ! [V5v4:$i] : (mem(V5v4,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V6v5:$i] : (mem(V6v5,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V3v2)),inj__ty_2Enum_2Enum(V4v3)),V5v4),V6v5))))))))))) => ( ! [V7v:$i] : (mem(V7v,ty_2Epatricia_2Eptree(A_27a)) => p(ap(V0P,V7v)))))))))).
tff(conj_thm_2Epatricia_2EIS__EMPTY__def,lemma,(( ! [A_27a:del]: ( ! [V0v:tp__ty_2Enum_2Enum] : ( ! [V1v1:$i] : (mem(V1v1,A_27a) => ( ! [V2v2:tp__ty_2Enum_2Enum] : ( ! [V3v3:tp__ty_2Enum_2Enum] : ( ! [V4v4:$i] : (mem(V4v4,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V5v5:$i] : (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),inj__ty_2Enum_2Enum(V0v)),V1v1))) <=> $false) & (p(ap(c_2Epatricia_2EIS__EMPTY(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V2v2)),inj__ty_2Enum_2Enum(V3v3)),V4v4),V5v5))) <=> $false))))))))))))))).
tff(ax_thm_2Epatricia_2EFIND__def,axiom,( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EFIND(A_27a),V0t),inj__ty_2Enum_2Enum(V1k)) = ap(c_2Eoption_2ETHE(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),inj__ty_2Enum_2Enum(V1k))))))))).
tff(ax_thm_2Epatricia_2EADD__LIST__def,axiom,( ! [A_27a:del]: (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))))).
tff(conj_thm_2Epatricia_2EBRANCHING__BIT,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((~~ (V0a = V1b)) => (~~ (p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))),inj__ty_2Enum_2Enum(V0a))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))),inj__ty_2Enum_2Enum(V1b)))))))))).
tff(conj_thm_2Epatricia_2EBRANCHING__BIT__ZERO,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) = fo__c_2Enum_2E0) <=> ((p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0a))) <=> p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1b)))) | (V0a = V1b))))))).
tff(conj_thm_2Epatricia_2EBRANCHING__BIT__SYM,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) = surj__ty_2Enum_2Enum(ap(ap(c_2Epatricia_2EBRANCHING__BIT,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V0a)))))))).
tff(conj_thm_2Epatricia_2EEVERY__LEAF__ADD,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27a) => ((p(ap(ap(V0P,inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V2k)),V3d))))))))))))))).
tff(conj_thm_2Epatricia_2EMONO__EVERY__LEAF,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1Q:$i] : (mem(V1Q,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2t:$i] : (mem(V2t,ty_2Epatricia_2Eptree(A_27a)) => ((( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4d:$i] : (mem(V4d,A_27a) => (p(ap(ap(V0P,inj__ty_2Enum_2Enum(V3k)),V4d)) => p(ap(ap(V1Q,inj__ty_2Enum_2Enum(V3k)),V4d)))))) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V2t))) => p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V1Q),V2t)))))))))))).
tff(conj_thm_2Epatricia_2ENOT__ADD__EMPTY,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,A_27a) => (~~ (ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V2d)) = c_2Epatricia_2EEmpty(A_27a))))))))))).
tff(conj_thm_2Epatricia_2EEMPTY__IS__PTREE,lemma,(( ! [A_27a:del]: p(ap(c_2Epatricia_2EIS__PTREE(A_27a),c_2Epatricia_2EEmpty(A_27a)))))).
tff(conj_thm_2Epatricia_2EADD__IS__PTREE,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1x:$i] : (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))))))))))).
tff(conj_thm_2Epatricia_2EEVERY__LEAF__BRANCH,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:$i] : (mem(V3l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V4r:$i] : (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)))),inj__ty_2Enum_2Enum(V1p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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))))))))))))))).
tff(conj_thm_2Epatricia_2EEVERY__LEAF__REMOVE,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__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),inj__ty_2Enum_2Enum(V2k))))))))))))).
tff(conj_thm_2Epatricia_2EIS__PTREE__BRANCH,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : (mem(V2l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V3r:$i] : (mem(V3r,ty_2Epatricia_2Eptree(A_27a)) => ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Epair_2E_2C(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a)),V2l),V3r)))))))))))))))).
tff(conj_thm_2Epatricia_2EREMOVE__IS__PTREE,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__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),inj__ty_2Enum_2Enum(V1k))))))))))).
tff(conj_thm_2Epatricia_2EPEEK__NONE,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ((( ! [V3d:$i] : (mem(V3d,A_27a) => (~~ p(ap(ap(V0P,inj__ty_2Enum_2Enum(V2k)),V3d))))) & p(ap(ap(c_2Epatricia_2EEVERY__LEAF(A_27a),V0P),V1t))) => (ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),inj__ty_2Enum_2Enum(V2k)) = c_2Eoption_2ENONE(A_27a))))))))))).
tff(conj_thm_2Epatricia_2EPEEK__ADD,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,A_27a) => ( ! [V3j:tp__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),inj__ty_2Enum_2Enum(V1k)),V2d))),inj__ty_2Enum_2Enum(V3j)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V3j))),ap(c_2Eoption_2ESOME(A_27a),V2d)),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),inj__ty_2Enum_2Enum(V3j)))))))))))))).
tff(conj_thm_2Epatricia_2EBRANCH,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : (mem(V2l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V3r:$i] : (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)))),inj__ty_2Enum_2Enum(V0p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m)),V2l),V3r))))))))))))).
tff(conj_thm_2Epatricia_2EPEEK__REMOVE,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__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),inj__ty_2Enum_2Enum(V1k))),inj__ty_2Enum_2Enum(V2j)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V2j))),c_2Eoption_2ENONE(A_27a)),ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t),inj__ty_2Enum_2Enum(V2j)))))))))))).
tff(conj_thm_2Epatricia_2EEVERY__LEAF__TRANSFORM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1Q:$i] : (mem(V1Q,arr(ty_2Enum_2Enum,arr(A_27b,bool))) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27b)) => ( ! [V3t:$i] : (mem(V3t,ty_2Epatricia_2Eptree(A_27a)) => ((( ! [V4k:tp__ty_2Enum_2Enum] : ( ! [V5d:$i] : (mem(V5d,A_27a) => (p(ap(ap(V0P,inj__ty_2Enum_2Enum(V4k)),V5d)) => p(ap(ap(V1Q,inj__ty_2Enum_2Enum(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)))))))))))))))).
tff(conj_thm_2Epatricia_2ETRANSFORM__EMPTY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1t:$i] : (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))))))))))).
tff(conj_thm_2Epatricia_2ETRANSFORM__IS__PTREE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1t:$i] : (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)))))))))))).
tff(conj_thm_2Epatricia_2EPEEK__TRANSFORM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EPEEK(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t)),inj__ty_2Enum_2Enum(V2k)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),inj__ty_2Enum_2Enum(V2k))),c_2Eoption_2ENONE(A_27b)),f2569(A_27a,A_27b,V0f)))))))))))).
tff(conj_thm_2Epatricia_2EADD__TRANSFORM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (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),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V2k)),ap(V0f,V3d))))))))))))))).
tff(conj_thm_2Epatricia_2ETRANSFORM__BRANCH,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:$i] : (mem(V3l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V4r:$i] : (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)))),inj__ty_2Enum_2Enum(V1p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27a),ty_2Epatricia_2Eptree(A_27a))),inj__ty_2Enum_2Enum(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)))),inj__ty_2Enum_2Enum(V1p)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epatricia_2Eptree(A_27b),ty_2Epatricia_2Eptree(A_27b))),inj__ty_2Enum_2Enum(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)))))))))))))))))).
tff(conj_thm_2Epatricia_2EREMOVE__TRANSFORM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V1t),inj__ty_2Enum_2Enum(V2k))) = ap(ap(c_2Epatricia_2EREMOVE(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t)),inj__ty_2Enum_2Enum(V2k)))))))))))).
tff(conj_thm_2Epatricia_2EREMOVE__ADD__EQ,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (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),inj__ty_2Enum_2Enum(V1k)),V2d))),inj__ty_2Enum_2Enum(V1k)) = ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),inj__ty_2Enum_2Enum(V1k))))))))))).
tff(conj_thm_2Epatricia_2EADD__ADD,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,A_27a) => ( ! [V3e:$i] : (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),inj__ty_2Enum_2Enum(V1k)),V2d))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V3e)) = ap(ap(c_2Epatricia_2EADD(A_27a),V0t),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V3e))))))))))))).
tff(conj_thm_2Epatricia_2EEVERY__LEAF__PEEK,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V2k:tp__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),inj__ty_2Enum_2Enum(V2k))))) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V2k)),ap(c_2Eoption_2ETHE(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t),inj__ty_2Enum_2Enum(V2k)))))))))))))).
tff(conj_thm_2Epatricia_2EIS__PTREE__PEEK,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : (~~ p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),c_2Epatricia_2EEmpty(A_27a)),inj__ty_2Enum_2Enum(V0k)))))) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3b:$i] : (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),inj__ty_2Enum_2Enum(V2j)),V3b)),inj__ty_2Enum_2Enum(V1k)))) <=> (V2j = V1k)))))) & ( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6l:$i] : (mem(V6l,ty_2Epatricia_2Eptree(A_27c)) => ( ! [V7r:$i] : (mem(V7r,ty_2Epatricia_2Eptree(A_27c)) => (p(ap(c_2Epatricia_2EIS__PTREE(A_27c),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27c),inj__ty_2Enum_2Enum(V4p)),inj__ty_2Enum_2Enum(V5m)),V6l),V7r))) => ((? [V8k:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V5m)),inj__ty_2Enum_2Enum(V8k))) & p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V6l),inj__ty_2Enum_2Enum(V8k)))))) & ((? [V9k:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V5m)),inj__ty_2Enum_2Enum(V9k)))) & p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V7r),inj__ty_2Enum_2Enum(V9k)))))) & ( ! [V10k:tp__ty_2Enum_2Enum] : ( ! [V11n:tp__ty_2Enum_2Enum] : (((~~ p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(V5m)),inj__ty_2Enum_2Enum(V10k)),inj__ty_2Enum_2Enum(V4p)))) | (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V11n)),inj__ty_2Enum_2Enum(V5m))) & (~~ (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V11n)),inj__ty_2Enum_2Enum(V4p))) <=> p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V11n)),inj__ty_2Enum_2Enum(V10k))))))) => ((~~ p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V6l),inj__ty_2Enum_2Enum(V10k))))) & (~~ p(ap(c_2Eoption_2EIS__SOME(A_27c),ap(ap(c_2Epatricia_2EPEEK(A_27c),V7r),inj__ty_2Enum_2Enum(V10k))))))))))))))))))))))))).
tff(conj_thm_2Epatricia_2EPTREE__EQ,lemma,(( ! [A_27a:del]: ( ! [V0t1:$i] : (mem(V0t1,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1t2:$i] : (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:tp__ty_2Enum_2Enum] : (ap(ap(c_2Epatricia_2EPEEK(A_27a),V0t1),inj__ty_2Enum_2Enum(V2k)) = ap(ap(c_2Epatricia_2EPEEK(A_27a),V1t2),inj__ty_2Enum_2Enum(V2k)))) <=> (V0t1 = V1t2)))))))))).
tff(conj_thm_2Epatricia_2EREMOVE__REMOVE,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__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),inj__ty_2Enum_2Enum(V1k))),inj__ty_2Enum_2Enum(V1k)) = ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),inj__ty_2Enum_2Enum(V1k)))))))))).
tff(conj_thm_2Epatricia_2EREMOVE__ADD,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : (mem(V2d,A_27a) => ( ! [V3j:tp__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),inj__ty_2Enum_2Enum(V1k)),V2d))),inj__ty_2Enum_2Enum(V3j)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epatricia_2Eptree(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V3j))),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),inj__ty_2Enum_2Enum(V3j))),ap(ap(c_2Epatricia_2EADD(A_27a),ap(ap(c_2Epatricia_2EREMOVE(A_27a),V0t),inj__ty_2Enum_2Enum(V3j))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V2d)))))))))))))).
tff(conj_thm_2Epatricia_2EADD__ADD__SYM,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : (mem(V3d,A_27a) => ( ! [V4e:$i] : (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),inj__ty_2Enum_2Enum(V1k)),V3d))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V2j)),V4e))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V3d))))))))))))))).
tff(conj_thm_2Epatricia_2EFILTER__ALL,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => (~~ p(ap(V0P,ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n)),V1l)))))) <=> (ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = c_2Elist_2ENIL(A_27a)))))))))).
tff(conj_thm_2Epatricia_2ETRAVERSE__TRANSFORM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1t:$i] : (mem(V1t,ty_2Epatricia_2Eptree(A_27a)) => (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(c_2Epatricia_2ETRAVERSE(A_27b),ap(ap(c_2Epatricia_2ETRANSFORM(A_27b,A_27a),V0f),V1t))) = surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(ap(c_2Epatricia_2ETRAVERSE(A_27a),V1t))))))))))).
tff(conj_thm_2Epatricia_2EMEM__TRAVERSE__PEEK,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : (p(ap(c_2Epatricia_2EIS__PTREE(A_27a),V0t)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__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),inj__ty_2Enum_2Enum(V1k)))))))))))).
tff(conj_thm_2Epatricia_2EIN__NUMSET__OF__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epatricia_2ENUMSET__OF__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)))) <=> p(ap(ap(c_2Epatricia_2EIN__PTREE,inj__ty_2Enum_2Enum(V1n)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))))))))).
tff(conj_thm_2Epatricia_2EADD__LIST__IS__PTREE,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V1l:$i] : (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))))))))))).
tff(conj_thm_2Epatricia_2EADD__LIST__TO__EMPTY__IS__PTREE,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (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)))))))).
tff(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__IS__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Enum_2Enum,bool)) => (p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) => p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)),V1s))))))))).
tff(conj_thm_2Epatricia_2EPTREE__OF__NUMSET__IS__PTREE__EMPTY,lemma,(( ! [V0s:$i] : (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))))))).
tff(conj_thm_2Epatricia_2ENOT__KEY__LEFT__AND__RIGHT,lemma,(( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : (mem(V2l,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V3r:$i] : (mem(V3r,ty_2Epatricia_2Eptree(A_27a)) => ( ! [V4k:tp__ty_2Enum_2Enum] : ( ! [V5j:tp__ty_2Enum_2Enum] : ((p(ap(c_2Epatricia_2EIS__PTREE(A_27a),ap(ap(ap(ap(c_2Epatricia_2EBranch(A_27a),inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m)),V2l),V3r))) & (p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V2l),inj__ty_2Enum_2Enum(V4k)))) & p(ap(c_2Eoption_2EIS__SOME(A_27a),ap(ap(c_2Epatricia_2EPEEK(A_27a),V3r),inj__ty_2Enum_2Enum(V5j)))))) => (~~ (V4k = V5j)))))))))))))).
tff(conj_thm_2Epatricia_2EALL__DISTINCT__TRAVERSE,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (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))))))))).
tff(conj_thm_2Epatricia_2EMEM__ALL__DISTINCT__IMP__PERM,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (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:$i] : (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)))))))))).
tff(conj_thm_2Epatricia_2EMEM__TRAVERSE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1k:tp__ty_2Enum_2Enum] : (p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))))) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),ap(c_2Epatricia_2ENUMSET__OF__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)))))))))).
tff(conj_thm_2Epatricia_2EINSERT__PTREE__IS__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1x:tp__ty_2Enum_2Enum] : (p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) => p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EINSERT__PTREE,inj__ty_2Enum_2Enum(V1x)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))))))))).
tff(conj_thm_2Epatricia_2EFINITE__NUMSET__OF__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),ap(c_2Epatricia_2ENUMSET__OF__PTREE,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))))))).
tff(conj_thm_2Epatricia_2EADD__INSERT,lemma,(( ! [V0v:tp__ty_2Eone_2Eone] : ( ! [V1t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EADD(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Eone_2Eone),inj__ty_2Enum_2Enum(V2n)),inj__ty_2Eone_2Eone(V0v)))) = surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EINSERT__PTREE,inj__ty_2Enum_2Enum(V2n)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V1t))))))))).
tff(conj_thm_2Epatricia_2EPEEK__INSERT__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : (p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) => (surj__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone(ap(ap(c_2Epatricia_2EPEEK(ty_2Eone_2Eone),ap(ap(c_2Epatricia_2EINSERT__PTREE,inj__ty_2Enum_2Enum(V1k)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))),inj__ty_2Enum_2Enum(V2j))) = surj__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Eone_2Eone)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V2j))),ap(c_2Eoption_2ESOME(ty_2Eone_2Eone),inj__ty_2Eone_2Eone(fo__c_2Eone_2Eone))),ap(ap(c_2Epatricia_2EPEEK(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)),inj__ty_2Enum_2Enum(V2j))))))))))).
tff(conj_thm_2Epatricia_2EMEM__TRAVERSE__INSERT__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2h:tp__ty_2Enum_2Enum] : (p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__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,inj__ty_2Enum_2Enum(V2h)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)))))) <=> ((V1x = V2h) | ((~~ (V1x = V2h)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),ap(c_2Epatricia_2ETRAVERSE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)))))))))))))).
tff(conj_thm_2Epatricia_2EPERM__INSERT__PTREE,lemma,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1s:$i] : (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),inj__c_ty_2Epatricia_2Eptree_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)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(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,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))),V1s))))))))))).
tff(conj_thm_2Epatricia_2EIN__PTREE__OF__NUMSET,conjecture,(( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Enum_2Enum,bool)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(c_2Epatricia_2EIS__PTREE(ty_2Eone_2Eone),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) & p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1s))) => (p(ap(ap(c_2Epatricia_2EIN__PTREE,inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Epatricia_2EPTREE__OF__NUMSET,inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t)),V1s))) <=> (p(ap(ap(c_2Epatricia_2EIN__PTREE,inj__ty_2Enum_2Enum(V2n)),inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone(V0t))) | p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2n)),V1s))))))))))).
