include('Axioms/HL4001_2.ax').
tff(stp_o,type,(tp__o : $tType)).
tff(stp_inj_o,type,(inj__o : tp__o > $i)).
tff(stp_surj_o,type,(surj__o : $i > tp__o)).
tff(stp_inj_surj_o,axiom,( ! [X:tp__o] : (surj__o(inj__o(X)) = X))).
tff(stp_inj_mem_o,axiom,( ! [X:tp__o] : (mem(inj__o(X),bool)))).
tff(stp_iso_mem_o,axiom,( ! [X:$i] : (mem(X,bool) => (X = inj__o(surj__o(X)))))).
tff(tp_ty_2Efcp_2Ecart,type,( ty_2Efcp_2Ecart: ( del * del ) > del )).
tff(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum: del )).
tff(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
tff(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : tp__ty_2Enum_2Enum > $i)).
tff(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : $i > tp__ty_2Enum_2Enum)).
tff(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem(inj__ty_2Enum_2Enum(X),ty_2Enum_2Enum)))).
tff(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Enum_2Enum) => (X = inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(X)))))).
tff(tp_c_2Ealignment_2Ealigned,type,(c_2Ealignment_2Ealigned:del > $i)).
tff(mem_c_2Ealignment_2Ealigned,axiom,( ! [A_27a:del] : mem(c_2Ealignment_2Ealigned(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),bool))))).
tff(tp_c_2Ebool_2E_5C_2F,type,(c_2Ebool_2E_5C_2F:$i)).
tff(mem_c_2Ebool_2E_5C_2F,axiom,mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Ebool_2E_5C_2F,type,(fo__c_2Ebool_2E_5C_2F:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_5C_2F,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Ebool_2E_5C_2F(X0,X1)) = ap(ap(c_2Ebool_2E_5C_2F,inj__o(X0)),inj__o(X1)))))).
tff(ax_or_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Ebool_2E_5C_2F,Q),R)) <=> (p(Q) | p(R)))))))).
tff(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
tff(mem_c_2Emin_2E_3D_3D_3E,axiom,mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Emin_2E_3D_3D_3E,type,(fo__c_2Emin_2E_3D_3D_3E:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Emin_2E_3D_3D_3E,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Emin_2E_3D_3D_3E(X0,X1)) = ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(X0)),inj__o(X1)))))).
tff(ax_imp_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Emin_2E_3D_3D_3E,Q),R)) <=> (p(Q) => p(R)))))))).
tff(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
tff(mem_c_2Earithmetic_2E_3E_3D,axiom,mem(c_2Earithmetic_2E_3E_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E_3D,type,(fo__c_2Earithmetic_2E_3E_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
tff(mem_c_2Earithmetic_2E_3E,axiom,mem(c_2Earithmetic_2E_3E,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E,type,(fo__c_2Earithmetic_2E_3E:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Eprim__rec_2E_3C,type,(c_2Eprim__rec_2E_3C:$i)).
tff(mem_c_2Eprim__rec_2E_3C,axiom,mem(c_2Eprim__rec_2E_3C,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Eprim__rec_2E_3C,type,(fo__c_2Eprim__rec_2E_3C:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eprim__rec_2E_3C,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Eprim__rec_2E_3C(X0,X1)) = ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
tff(mem_c_2Earithmetic_2EEXP,axiom,mem(c_2Earithmetic_2EEXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EEXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EEXP(X0,X1)) = ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
tff(mem_c_2Earithmetic_2E_2D,axiom,mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2D(X0,X1)) = ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
tff(mem_c_2Enum_2E0,axiom,mem(c_2Enum_2E0,ty_2Enum_2Enum)).
tff(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enum_2E0,axiom,(inj__ty_2Enum_2Enum(fo__c_2Enum_2E0) = c_2Enum_2E0)).
tff(tp_c_2Enumeral_2EiiSUC,type,(c_2Enumeral_2EiiSUC:$i)).
tff(mem_c_2Enumeral_2EiiSUC,axiom,mem(c_2Enumeral_2EiiSUC,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2EiiSUC,type,(fo__c_2Enumeral_2EiiSUC:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2EiiSUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2EiiSUC(X0)) = ap(c_2Enumeral_2EiiSUC,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
tff(mem_c_2Ebool_2EF,axiom,mem(c_2Ebool_2EF,bool)).
tff(stp_fo_c_2Ebool_2EF,type,(fo__c_2Ebool_2EF:tp__o)).
tff(stp_eq_fo_c_2Ebool_2EF,axiom,(inj__o(fo__c_2Ebool_2EF) = c_2Ebool_2EF)).
tff(ax_false_p,axiom,(~ p(c_2Ebool_2EF))).
tff(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
tff(mem_c_2Ebool_2ET,axiom,mem(c_2Ebool_2ET,bool)).
tff(stp_fo_c_2Ebool_2ET,type,(fo__c_2Ebool_2ET:tp__o)).
tff(stp_eq_fo_c_2Ebool_2ET,axiom,(inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET)).
tff(ax_true_p,axiom,p(c_2Ebool_2ET)).
tff(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
tff(mem_c_2Earithmetic_2E_3C_3D,axiom,mem(c_2Earithmetic_2E_3C_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3C_3D,type,(fo__c_2Earithmetic_2E_3C_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3C_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3C_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
tff(mem_c_2Ebool_2E_7E,axiom,mem(c_2Ebool_2E_7E,arr(bool,bool))).
tff(stp_fo_c_2Ebool_2E_7E,type,(fo__c_2Ebool_2E_7E:(tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_7E,axiom,( ! [X0:tp__o] : (inj__o(fo__c_2Ebool_2E_7E(X0)) = ap(c_2Ebool_2E_7E,inj__o(X0))))).
tff(ax_neg_p,axiom,( ! [Q:$i] : (mem(Q,bool) => (p(ap(c_2Ebool_2E_7E,Q)) <=> (~ p(Q)))))).
tff(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
tff(mem_c_2Earithmetic_2EEVEN,axiom,mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EEVEN,type,(fo__c_2Earithmetic_2EEVEN:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EEVEN,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EEVEN(X0)) = ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enum_2ESUC,type,(c_2Enum_2ESUC:$i)).
tff(mem_c_2Enum_2ESUC,axiom,mem(c_2Enum_2ESUC,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enum_2ESUC,type,(fo__c_2Enum_2ESUC:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enum_2ESUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0)) = ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enumeral_2Eonecount,type,(c_2Enumeral_2Eonecount:$i)).
tff(mem_c_2Enumeral_2Eonecount,axiom,mem(c_2Enumeral_2Eonecount,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Enumeral_2Eonecount,type,(fo__c_2Enumeral_2Eonecount:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2Eonecount,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2Eonecount(X0,X1)) = ap(ap(c_2Enumeral_2Eonecount,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Enumeral_2Eexactlog,type,(c_2Enumeral_2Eexactlog:$i)).
tff(mem_c_2Enumeral_2Eexactlog,axiom,mem(c_2Enumeral_2Eexactlog,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2Eexactlog,type,(fo__c_2Enumeral_2Eexactlog:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2Eexactlog,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2Eexactlog(X0)) = ap(c_2Enumeral_2Eexactlog,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eprim__rec_2EPRE,type,(c_2Eprim__rec_2EPRE:$i)).
tff(mem_c_2Eprim__rec_2EPRE,axiom,mem(c_2Eprim__rec_2EPRE,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eprim__rec_2EPRE,type,(fo__c_2Eprim__rec_2EPRE:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Eprim__rec_2EPRE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Eprim__rec_2EPRE(X0)) = ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EDIV2,type,(c_2Earithmetic_2EDIV2:$i)).
tff(mem_c_2Earithmetic_2EDIV2,axiom,mem(c_2Earithmetic_2EDIV2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EDIV2,type,(fo__c_2Earithmetic_2EDIV2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EDIV2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EDIV2(X0)) = ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enumeral_2Etexp__help,type,(c_2Enumeral_2Etexp__help:$i)).
tff(mem_c_2Enumeral_2Etexp__help,axiom,mem(c_2Enumeral_2Etexp__help,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Enumeral_2Etexp__help,type,(fo__c_2Enumeral_2Etexp__help:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2Etexp__help,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2Etexp__help(X0,X1)) = ap(ap(c_2Enumeral_2Etexp__help,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
tff(mem_c_2Earithmetic_2EODD,axiom,mem(c_2Earithmetic_2EODD,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EODD,type,(fo__c_2Earithmetic_2EODD:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EODD,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EODD(X0)) = ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:del > $i)).
tff(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : mem(c_2Ebool_2ECOND(A_27a),arr(bool,arr(A_27a,arr(A_27a,A_27a)))))).
tff(tp_c_2Ebool_2ELET,type,(c_2Ebool_2ELET:(del * del) > $i)).
tff(mem_c_2Ebool_2ELET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebool_2ELET(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(A_27a,A_27b)))))).
tff(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
tff(mem_c_2Earithmetic_2EBIT2,axiom,mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(X0)) = ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enumeral_2EiDUB,type,(c_2Enumeral_2EiDUB:$i)).
tff(mem_c_2Enumeral_2EiDUB,axiom,mem(c_2Enumeral_2EiDUB,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2EiDUB,type,(fo__c_2Enumeral_2EiDUB:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2EiDUB,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2EiDUB(X0)) = ap(c_2Enumeral_2EiDUB,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enumeral_2EiZ,type,(c_2Enumeral_2EiZ:$i)).
tff(mem_c_2Enumeral_2EiZ,axiom,mem(c_2Enumeral_2EiZ,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2EiZ,type,(fo__c_2Enumeral_2EiZ:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2EiZ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2EiZ(X0)) = ap(c_2Enumeral_2EiZ,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enumeral_2Einternal__mult,type,(c_2Enumeral_2Einternal__mult:$i)).
tff(mem_c_2Enumeral_2Einternal__mult,axiom,mem(c_2Enumeral_2Einternal__mult,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Enumeral_2Einternal__mult,type,(fo__c_2Enumeral_2Einternal__mult:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2Einternal__mult,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2Einternal__mult(X0,X1)) = ap(ap(c_2Enumeral_2Einternal__mult,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
tff(mem_c_2Ebool_2E_2F_5C,axiom,mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Ebool_2E_2F_5C,type,(fo__c_2Ebool_2E_2F_5C:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_2F_5C,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Ebool_2E_2F_5C(X0,X1)) = ap(ap(c_2Ebool_2E_2F_5C,inj__o(X0)),inj__o(X1)))))).
tff(ax_and_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Ebool_2E_2F_5C,Q),R)) <=> (p(Q) & p(R)))))))).
tff(tp_c_2Ewords_2Eword__sub,type,(c_2Ewords_2Eword__sub:del > $i)).
tff(mem_c_2Ewords_2Eword__sub,axiom,( ! [A_27a:del] : mem(c_2Ewords_2Eword__sub(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))))).
tff(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
tff(mem_c_2Earithmetic_2E_2B,axiom,mem(c_2Earithmetic_2E_2B,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2B,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,X1)) = ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
tff(mem_c_2Earithmetic_2E_2A,axiom,mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2A,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1)) = ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ewords_2Eword__add,type,(c_2Ewords_2Eword__add:del > $i)).
tff(mem_c_2Ewords_2Eword__add,axiom,( ! [A_27a:del] : mem(c_2Ewords_2Eword__add(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))))).
tff(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
tff(mem_c_2Earithmetic_2EZERO,axiom,mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum)).
tff(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
tff(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
tff(mem_c_2Earithmetic_2EBIT1,axiom,mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT1,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(X0)) = ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
tff(mem_c_2Earithmetic_2ENUMERAL,axiom,mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2ENUMERAL,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(X0)) = ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ewords_2En2w,type,(c_2Ewords_2En2w:del > $i)).
tff(mem_c_2Ewords_2En2w,axiom,( ! [A_27a:del] : mem(c_2Ewords_2En2w(A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a))))).
tff(tp_c_2Ewords_2Eword__mul,type,(c_2Ewords_2Eword__mul:del > $i)).
tff(mem_c_2Ewords_2Eword__mul,axiom,( ! [A_27a:del] : mem(c_2Ewords_2Eword__mul(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))))).
tff(tp_c_2Ewords_2Eword__2comp,type,(c_2Ewords_2Eword__2comp:del > $i)).
tff(mem_c_2Ewords_2Eword__2comp,axiom,( ! [A_27a:del] : mem(c_2Ewords_2Eword__2comp(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))))).
tff(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:del > $i)).
tff(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : mem(c_2Emin_2E_3D(A_27a),arr(A_27a,arr(A_27a,bool))))).
tff(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : (mem(X,A) => ( ! [Y:$i] : (mem(Y,A) => (p(ap(ap(c_2Emin_2E_3D(A),X),Y)) <=> (X = Y)))))))).
tff(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:del > $i)).
tff(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool)))).
tff(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : (mem(Q,arr(A,bool)) => (p(ap(c_2Ebool_2E_21(A),Q)) <=> ( ! [X:$i] : (mem(X,A) => p(ap(Q,X))))))))).
tff(conj_thm_2Ealignment_2Ealigned__add__sub__123,lemma,(( ! [A_27a:del]: (( ! [V0w:$i] : (mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V1x:$i] : (mem(V1x,ty_2Efcp_2Ecart(bool,A_27a)) => ((p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a),V0w),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V1x)))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V0w))) & (p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a),V0w),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V1x)))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V0w)))))))) & (( ! [V2x:$i] : (mem(V2x,ty_2Efcp_2Ecart(bool,A_27a)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V2x))) & p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),V2x)))))) & (( ! [V3w:$i] : (mem(V3w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V4x:$i] : (mem(V4x,ty_2Efcp_2Ecart(bool,A_27a)) => ((p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a),V3w),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),V4x)))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V3w))) & (p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a),V3w),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),V4x)))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V3w)))))))) & (( ! [V5x:$i] : (mem(V5x,ty_2Efcp_2Ecart(bool,A_27a)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),V5x))) & p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),V5x)))))) & (( ! [V6w:$i] : (mem(V6w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V7x:$i] : (mem(V7x,ty_2Efcp_2Ecart(bool,A_27a)) => ((p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27a),V6w),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),V7x)))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V6w))) & (p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a),V6w),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),V7x)))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V6w)))))))) & ( ! [V8x:$i] : (mem(V8x,ty_2Efcp_2Ecart(bool,A_27a)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),V8x))) & p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))),V8x)))))))))))))).
tff(ax_thm_2Earithmetic_2ENUMERAL__DEF,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V0x))) = V0x))).
tff(ax_thm_2Earithmetic_2EBIT1,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(ax_thm_2Earithmetic_2EBIT2,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Earithmetic_2EONE,lemma,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2ETWO,lemma,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Earithmetic_2EADD__SYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EADD__ASSOC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2EMULT__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n)))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))))).
tff(conj_thm_2Earithmetic_2ERIGHT__ADD__DISTRIB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELEFT__ADD__DISTRIB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ETIMES2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2EADD__MONO__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ENOT__NUM__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ (V0m = V1n)) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2ESUC__ONE__ADD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))) = 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)))),inj__ty_2Enum_2Enum(V0n))))))).
tff(ax_thm_2Ebool_2ELET__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (c_2Ebool_2ELET(A_27a,A_27b) = f14(A_27b,A_27a))))).
tff(ax_thm_2Ebool_2EETA__AX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : (mem(V0t,arr(A_27a,A_27b)) => (f31(A_27b,A_27a,V0t) = V0t)))))).
tff(conj_thm_2Ebool_2ETRUTH,lemma,($true)).
tff(conj_thm_2Ebool_2EIMP__ANTISYM__AX,lemma,(( ! [V0t1:tp__o] : ( ! [V1t2:tp__o] : ((p(inj__o(V0t1)) => p(inj__o(V1t2))) => ((p(inj__o(V1t2)) => p(inj__o(V0t1))) => (p(inj__o(V0t1)) <=> p(inj__o(V1t2))))))))).
tff(conj_thm_2Ebool_2EFALSITY,lemma,(( ! [V0t:tp__o] : ($false => p(inj__o(V0t)))))).
tff(conj_thm_2Ebool_2EFORALL__SIMP,lemma,(( ! [A_27a:del]: ( ! [V0t:tp__o] : (( ! [V1x:$i] : (mem(V1x,A_27a) => p(inj__o(V0t)))) <=> p(inj__o(V0t))))))).
tff(conj_thm_2Ebool_2EOR__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true | p(inj__o(V0t))) <=> $true) & (((p(inj__o(V0t)) | $true) <=> $true) & ((($false | p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) | $false) <=> p(inj__o(V0t))) & ((p(inj__o(V0t)) | p(inj__o(V0t))) <=> p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,((( ! [V0t:tp__o] : ((~~ (~~ p(inj__o(V0t)))) <=> p(inj__o(V0t)))) & (((~~ ($true)) <=> $false) & ((~~ ($false)) <=> $true))))).
tff(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ((V0x = V0x) <=> $true)))))).
tff(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ((V0x = V1y) <=> (V1y = V0x))))))))).
tff(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true <=> p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) <=> $true) <=> p(inj__o(V0t))) & ((($false <=> p(inj__o(V0t))) <=> (~~ p(inj__o(V0t)))) & ((p(inj__o(V0t)) <=> $false) <=> (~~ p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2ECOND__CLAUSES,lemma,(( ! [A_27a:del]: ( ! [V0t1:$i] : (mem(V0t1,A_27a) => ( ! [V1t2:$i] : (mem(V1t2,A_27a) => ((ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2ET)),V0t1),V1t2) = V0t1) & (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2EF)),V0t1),V1t2) = V1t2))))))))).
tff(conj_thm_2Ebool_2EIMP__F__EQ__F,lemma,(( ! [V0t:tp__o] : ((p(inj__o(V0t)) => $false) <=> (p(inj__o(V0t)) <=> $false))))).
tff(conj_thm_2Enumeral_2Enumeral__suc,lemma,(((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) & (( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))))) & ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Enumeral_2Enumeral__distrib,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = V0n)) & (( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V1n)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V3m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V3m)))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V4n))) = fo__c_2Enum_2E0)) & (( ! [V5n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V5n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V6n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V7m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V6n)),inj__ty_2Enum_2Enum(V7m))))))) & (( ! [V8n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V8n))) = fo__c_2Enum_2E0)) & (( ! [V9n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V9n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V9n)) & (( ! [V10n:tp__ty_2Enum_2Enum] : ( ! [V11m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V10n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V11m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V10n)),inj__ty_2Enum_2Enum(V11m))))))) & (( ! [V12n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V12n))))) = fo__c_2Enum_2E0)) & (( ! [V13n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V13n))))) = fo__c_2Enum_2E0)) & (( ! [V14n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V14n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & (( ! [V15n:tp__ty_2Enum_2Enum] : ( ! [V16m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V15n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V16m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V15n)),inj__ty_2Enum_2Enum(V16m))))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V17n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V17n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V17n)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & (( ! [V18n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V18n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V18n)))))) & (( ! [V19n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V19n))) = fo__c_2Enum_2E0) <=> (V19n = fo__c_2Earithmetic_2EZERO))) & (( ! [V20n:tp__ty_2Enum_2Enum] : ((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V20n)))) <=> (V20n = fo__c_2Earithmetic_2EZERO))) & (( ! [V21n:tp__ty_2Enum_2Enum] : ( ! [V22m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V21n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V22m)))) <=> (V21n = V22m)))) & (( ! [V23n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V23n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $false)) & (( ! [V24n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V24n)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V24n))))) & (( ! [V25n:tp__ty_2Enum_2Enum] : ( ! [V26m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V25n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V26m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V25n)),inj__ty_2Enum_2Enum(V26m)))))) & (( ! [V27n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V27n))) <=> $false)) & (( ! [V28n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V28n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V28n))))) & (( ! [V29n:tp__ty_2Enum_2Enum] : ( ! [V30m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V29n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V30m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V30m)),inj__ty_2Enum_2Enum(V29n)))))) & (( ! [V31n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V31n))) <=> $true)) & (( ! [V32n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V32n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V32n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V33n:tp__ty_2Enum_2Enum] : ( ! [V34m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V33n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V34m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V33n)),inj__ty_2Enum_2Enum(V34m)))))) & (( ! [V35n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V35n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $true)) & (( ! [V36n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V36n))) <=> (V36n = fo__c_2Enum_2E0))) & (( ! [V37n:tp__ty_2Enum_2Enum] : ( ! [V38m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V37n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V38m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V38m)),inj__ty_2Enum_2Enum(V37n)))))) & (( ! [V39n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V39n)))) <=> p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V39n))))) & (( ! [V40n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V40n)))) <=> p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V40n))))) & ((~~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))))))))))))))))))))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__add,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n)))) = V0n) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = V0n) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & (surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))))))))))))))))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__eq,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((fo__c_2Earithmetic_2EZERO = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((fo__c_2Earithmetic_2EZERO = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m)) & ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__lte,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n))) <=> $true) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> (~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__pre,lemma,(((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & ((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = fo__c_2Earithmetic_2EZERO) & (( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2n))))))))))).
tff(conj_thm_2Enumeral_2EiDUB__removal,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiDUB,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enumeral_2EiDUB,inj__ty_2Enum_2Enum(V0n))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiDUB,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))) & (surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiDUB,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO)))))).
tff(conj_thm_2Enumeral_2Enumeral__evenodd,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) & (p(ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) & ((~~ p(ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))) & ((~~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) & ((~~ p(ap(c_2Earithmetic_2EODD,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))))) & p(ap(c_2Earithmetic_2EODD,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__texp__help,lemma,(( ! [V0acc:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Etexp__help,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0acc))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0acc)))) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Etexp__help,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0acc))) = surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Etexp__help,ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0acc))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Etexp__help,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0acc))) = surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Etexp__help,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0acc))))))))))).
tff(ax_thm_2Enumeral_2Eonecount__def,axiom,(( ! [V0x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Eonecount,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0x))) = V0x)) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Eonecount,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2x))) = surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Eonecount,inj__ty_2Enum_2Enum(V1n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2x))))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Eonecount,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3n))),inj__ty_2Enum_2Enum(V4x))) = fo__c_2Earithmetic_2EZERO)))))).
tff(ax_thm_2Enumeral_2Eexactlog__def,axiom,((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2Eexactlog,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & (( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enumeral_2Eexactlog,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) = fo__c_2Earithmetic_2EZERO)) & ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enumeral_2Eexactlog,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Enum_2Enum),f202),ap(ap(c_2Enumeral_2Eonecount,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Enumeral_2EDIV2__BIT1,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EDIV2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x)))) = V0x)))).
tff(conj_thm_2Enumeral_2Eenumeral__mult,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2y:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2y)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Einternal__mult,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2y))))) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1x))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2y)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Enum_2Enum),f203(V1x,V2y)),ap(c_2Enumeral_2Eexactlog,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2y)))))) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1x))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2y)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Enum_2Enum),f204(V1x,V2y)),ap(c_2Enumeral_2Eexactlog,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1x)))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1x))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2y)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Enum_2Enum),f206(V1x,V2y)),ap(c_2Enumeral_2Eexactlog,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1x)))))))))))))))).
tff(conj_thm_2Enumeral_2Einternal__mult__characterisation,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Einternal__mult,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Einternal__mult,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Einternal__mult,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1m))) = surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enumeral_2EiDUB,ap(ap(c_2Enumeral_2Einternal__mult,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))),inj__ty_2Enum_2Enum(V1m))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Enumeral_2Einternal__mult,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1m))) = surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiDUB,ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Enumeral_2Einternal__mult,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V1m))))))))))))).
tff(ax_thm_2Ewords_2Eword__sub__def,axiom,( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V1w:$i] : (mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => (ap(ap(c_2Ewords_2Eword__sub(A_27a),V0v),V1w) = ap(ap(c_2Ewords_2Eword__add(A_27a),V0v),ap(c_2Ewords_2Eword__2comp(A_27a),V1w))))))))).
tff(conj_thm_2Ewords_2Eword__add__n2w,lemma,(( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Ewords_2Eword__add(A_27a),ap(c_2Ewords_2En2w(A_27a),inj__ty_2Enum_2Enum(V0m))),ap(c_2Ewords_2En2w(A_27a),inj__ty_2Enum_2Enum(V1n))) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Ewords_2Eword__mul__n2w,lemma,(( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),inj__ty_2Enum_2Enum(V0m))),ap(c_2Ewords_2En2w(A_27a),inj__ty_2Enum_2Enum(V1n))) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Ewords_2EWORD__ADD__ASSOC,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V1w:$i] : (mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V2x:$i] : (mem(V2x,ty_2Efcp_2Ecart(bool,A_27a)) => (ap(ap(c_2Ewords_2Eword__add(A_27a),V0v),ap(ap(c_2Ewords_2Eword__add(A_27a),V1w),V2x)) = ap(ap(c_2Ewords_2Eword__add(A_27a),ap(ap(c_2Ewords_2Eword__add(A_27a),V0v),V1w)),V2x))))))))))).
tff(conj_thm_2Ewords_2EWORD__ADD__COMM,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V1w:$i] : (mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => (ap(ap(c_2Ewords_2Eword__add(A_27a),V0v),V1w) = ap(ap(c_2Ewords_2Eword__add(A_27a),V1w),V0v))))))))).
tff(conj_thm_2Ewords_2EWORD__LEFT__ADD__DISTRIB,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V1w:$i] : (mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V2x:$i] : (mem(V2x,ty_2Efcp_2Ecart(bool,A_27a)) => (ap(ap(c_2Ewords_2Eword__mul(A_27a),V0v),ap(ap(c_2Ewords_2Eword__add(A_27a),V1w),V2x)) = ap(ap(c_2Ewords_2Eword__add(A_27a),ap(ap(c_2Ewords_2Eword__mul(A_27a),V0v),V1w)),ap(ap(c_2Ewords_2Eword__mul(A_27a),V0v),V2x)))))))))))).
tff(conj_thm_2Ewords_2EWORD__NEG__LMUL,lemma,(( ! [A_27a:del]: ( ! [V0v:$i] : (mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ( ! [V1w:$i] : (mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => (ap(c_2Ewords_2Eword__2comp(A_27a),ap(ap(c_2Ewords_2Eword__mul(A_27a),V0v),V1w)) = ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),V0v)),V1w))))))))).
tff(conj_thm_2Ewords_2EWORD__NEG__MUL,lemma,(( ! [A_27a:del]: ( ! [V0w:$i] : (mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => (ap(c_2Ewords_2Eword__2comp(A_27a),V0w) = ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),V0w))))))).
tff(conj_thm_2Ealignment_2Ealigned__numeric,conjecture,(( ! [A_27a:del]: ( ! [A_27a0:del]: ( ! [A_27a1:del]: ( ! [A_27a10:del]: ( ! [A_27a11:del]: ( ! [A_27a12:del]: ( ! [A_27a13:del]: ( ! [A_27a14:del]: ( ! [A_27a15:del]: ( ! [A_27a16:del]: ( ! [A_27a17:del]: ( ! [A_27a18:del]: ( ! [A_27a19:del]: ( ! [A_27a2:del]: ( ! [A_27a20:del]: ( ! [A_27a21:del]: ( ! [A_27a22:del]: ( ! [A_27a23:del]: ( ! [A_27a24:del]: ( ! [A_27a25:del]: ( ! [A_27a26:del]: ( ! [A_27a27:del]: ( ! [A_27a3:del]: ( ! [A_27a4:del]: ( ! [A_27a5:del]: ( ! [A_27a6:del]: ( ! [A_27a7:del]: ( ! [A_27a8:del]: ( ! [A_27a9:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [A_27f:del]: ( ! [A_27g:del]: ( ! [A_27h:del]: ( ! [A_27i:del]: ( ! [A_27j:del]: ( ! [A_27k:del]: ( ! [A_27l:del]: ( ! [A_27m:del]: ( ! [A_27n:del]: ( ! [A_27o:del]: ( ! [A_27p:del]: ( ! [A_27q:del]: ( ! [A_27r:del]: ( ! [A_27s:del]: ( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27v:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [A_27y:del]: ( ! [A_27z:del]: (( ! [V0x:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ealignment_2Ealigned(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))))))))) & (( ! [V1x:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ealignment_2Ealigned(A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Ewords_2En2w(A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1x)))))))) & (( ! [V2x:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ealignment_2Ealigned(A_27c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Ewords_2En2w(A_27c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2x))))))) & (( ! [V3x:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ealignment_2Ealigned(A_27d),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Ewords_2Eword__2comp(A_27d),ap(c_2Ewords_2En2w(A_27d),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3x)))))))))) & (( ! [V4x:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ealignment_2Ealigned(A_27e),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Ewords_2Eword__2comp(A_27e),ap(c_2Ewords_2En2w(A_27e),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V4x))))))))) & (( ! [V5x:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ealignment_2Ealigned(A_27f),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Ewords_2Eword__2comp(A_27f),ap(c_2Ewords_2En2w(A_27f),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V5x)))))))) & (( ! [V6x:$i] : (mem(V6x,A_27g) => ( ! [V7y:$i] : (mem(V7y,ty_2Efcp_2Ecart(bool,A_27h)) => ( ! [V8f:$i] : (mem(V8f,arr(A_27g,ty_2Enum_2Enum)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27h),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27h),V7y),ap(c_2Ewords_2En2w(A_27h),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(V8f,V6x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27h),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27h),V7y),ap(c_2Ewords_2En2w(A_27h),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))) & (( ! [V9x:tp__ty_2Enum_2Enum] : ( ! [V10y:$i] : (mem(V10y,ty_2Efcp_2Ecart(bool,A_27i)) => ( ! [V11f:$i] : (mem(V11f,A_27j) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27i),V10y),ap(c_2Ewords_2En2w(A_27i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V9x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27i),V10y),ap(c_2Ewords_2En2w(A_27i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V12x:tp__ty_2Enum_2Enum] : ( ! [V13y:$i] : (mem(V13y,ty_2Efcp_2Ecart(bool,A_27k)) => ( ! [V14f:$i] : (mem(V14f,A_27l) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27k),V13y),ap(c_2Ewords_2En2w(A_27k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V12x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27k),V13y),ap(c_2Ewords_2En2w(A_27k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))) & (( ! [V15x:tp__ty_2Enum_2Enum] : ( ! [V16y:$i] : (mem(V16y,ty_2Efcp_2Ecart(bool,A_27m)) => ( ! [V17f:$i] : (mem(V17f,A_27n) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27m),V16y),ap(c_2Ewords_2En2w(A_27m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V15x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27m),V16y),ap(c_2Ewords_2En2w(A_27m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V18x:tp__ty_2Enum_2Enum] : ( ! [V19y:$i] : (mem(V19y,ty_2Efcp_2Ecart(bool,A_27o)) => ( ! [V20f:$i] : (mem(V20f,A_27p) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27o),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27o),V19y),ap(c_2Ewords_2En2w(A_27o),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V18x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27o),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V19y)))))))) & (( ! [V21x:tp__ty_2Enum_2Enum] : ( ! [V22y:$i] : (mem(V22y,ty_2Efcp_2Ecart(bool,A_27q)) => ( ! [V23f:$i] : (mem(V23f,A_27r) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27q),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27q),V22y),ap(c_2Ewords_2En2w(A_27q),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V21x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27q),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27q),V22y),ap(c_2Ewords_2En2w(A_27q),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V24x:tp__ty_2Enum_2Enum] : ( ! [V25y:$i] : (mem(V25y,ty_2Efcp_2Ecart(bool,A_27s)) => ( ! [V26f:$i] : (mem(V26f,A_27t) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27s),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27s),V25y),ap(c_2Ewords_2En2w(A_27s),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V24x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27s),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27s),V25y),ap(c_2Ewords_2En2w(A_27s),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))) & (( ! [V27x:tp__ty_2Enum_2Enum] : ( ! [V28y:$i] : (mem(V28y,ty_2Efcp_2Ecart(bool,A_27u)) => ( ! [V29f:$i] : (mem(V29f,A_27v) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27u),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27u),V28y),ap(c_2Ewords_2En2w(A_27u),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V27x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27u),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__add(A_27u),V28y),ap(c_2Ewords_2En2w(A_27u),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V30x:$i] : (mem(V30x,A_27w) => ( ! [V31y:$i] : (mem(V31y,ty_2Efcp_2Ecart(bool,A_27x)) => ( ! [V32f:$i] : (mem(V32f,arr(A_27w,ty_2Enum_2Enum)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27x),V31y),ap(c_2Ewords_2En2w(A_27x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(V32f,V30x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27x),V31y),ap(c_2Ewords_2En2w(A_27x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))) & (( ! [V33x:tp__ty_2Enum_2Enum] : ( ! [V34y:$i] : (mem(V34y,ty_2Efcp_2Ecart(bool,A_27y)) => ( ! [V35f:$i] : (mem(V35f,A_27z) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27y),V34y),ap(c_2Ewords_2En2w(A_27y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V33x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27y),V34y),ap(c_2Ewords_2En2w(A_27y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V36x:tp__ty_2Enum_2Enum] : ( ! [V37y:$i] : (mem(V37y,ty_2Efcp_2Ecart(bool,A_27a0)) => ( ! [V38f:$i] : (mem(V38f,A_27a1) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a0),V37y),ap(c_2Ewords_2En2w(A_27a0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V36x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a0),V37y),ap(c_2Ewords_2En2w(A_27a0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))) & (( ! [V39x:tp__ty_2Enum_2Enum] : ( ! [V40y:$i] : (mem(V40y,ty_2Efcp_2Ecart(bool,A_27a2)) => ( ! [V41f:$i] : (mem(V41f,A_27a3) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a2),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a2),V40y),ap(c_2Ewords_2En2w(A_27a2),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V39x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a2),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a2),V40y),ap(c_2Ewords_2En2w(A_27a2),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V42x:tp__ty_2Enum_2Enum] : ( ! [V43y:$i] : (mem(V43y,ty_2Efcp_2Ecart(bool,A_27a4)) => ( ! [V44f:$i] : (mem(V44f,A_27a5) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a4),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a4),V43y),ap(c_2Ewords_2En2w(A_27a4),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V42x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a4),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V43y)))))))) & (( ! [V45x:tp__ty_2Enum_2Enum] : ( ! [V46y:$i] : (mem(V46y,ty_2Efcp_2Ecart(bool,A_27a6)) => ( ! [V47f:$i] : (mem(V47f,A_27a7) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a6),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a6),V46y),ap(c_2Ewords_2En2w(A_27a6),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V45x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a6),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a6),V46y),ap(c_2Ewords_2En2w(A_27a6),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V48x:tp__ty_2Enum_2Enum] : ( ! [V49y:$i] : (mem(V49y,ty_2Efcp_2Ecart(bool,A_27a8)) => ( ! [V50f:$i] : (mem(V50f,A_27a9) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a8),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a8),V49y),ap(c_2Ewords_2En2w(A_27a8),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V48x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a8),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a8),V49y),ap(c_2Ewords_2En2w(A_27a8),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))) & (( ! [V51x:tp__ty_2Enum_2Enum] : ( ! [V52y:$i] : (mem(V52y,ty_2Efcp_2Ecart(bool,A_27a10)) => ( ! [V53f:$i] : (mem(V53f,A_27a11) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a10),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a10),V52y),ap(c_2Ewords_2En2w(A_27a10),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V51x))))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a10),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ewords_2Eword__sub(A_27a10),V52y),ap(c_2Ewords_2En2w(A_27a10),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V54x:$i] : (mem(V54x,A_27a12) => ( ! [V55y:$i] : (mem(V55y,ty_2Efcp_2Ecart(bool,A_27a13)) => ( ! [V56f:$i] : (mem(V56f,arr(A_27a12,ty_2Enum_2Enum)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a13),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a13),V55y),ap(c_2Ewords_2En2w(A_27a13),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(V56f,V54x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a13),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a13),V55y),ap(c_2Ewords_2En2w(A_27a13),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))) & (( ! [V57x:tp__ty_2Enum_2Enum] : ( ! [V58y:$i] : (mem(V58y,ty_2Efcp_2Ecart(bool,A_27a14)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a14),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a14),V58y),ap(c_2Ewords_2En2w(A_27a14),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V57x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a14),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a14),V58y),ap(c_2Ewords_2En2w(A_27a14),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))) & (( ! [V59x:tp__ty_2Enum_2Enum] : ( ! [V60y:$i] : (mem(V60y,ty_2Efcp_2Ecart(bool,A_27a15)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a15),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a15),V60y),ap(c_2Ewords_2En2w(A_27a15),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V59x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a15),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V60y)))))) & (( ! [V61x:tp__ty_2Enum_2Enum] : ( ! [V62y:$i] : (mem(V62y,ty_2Efcp_2Ecart(bool,A_27a16)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a16),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a16),V62y),ap(c_2Ewords_2En2w(A_27a16),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V61x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a16),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a16),V62y),ap(c_2Ewords_2En2w(A_27a16),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))) & (( ! [V63x:$i] : (mem(V63x,A_27a17) => ( ! [V64y:$i] : (mem(V64y,ty_2Efcp_2Ecart(bool,A_27a18)) => ( ! [V65f:$i] : (mem(V65f,arr(A_27a17,ty_2Enum_2Enum)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a18),V64y),ap(c_2Ewords_2En2w(A_27a18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(V65f,V63x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a18),V64y),ap(c_2Ewords_2En2w(A_27a18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))) & (( ! [V66x:tp__ty_2Enum_2Enum] : ( ! [V67y:$i] : (mem(V67y,ty_2Efcp_2Ecart(bool,A_27a19)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a19),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a19),V67y),ap(c_2Ewords_2En2w(A_27a19),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V66x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a19),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a19),V67y),ap(c_2Ewords_2En2w(A_27a19),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))) & (( ! [V68x:tp__ty_2Enum_2Enum] : ( ! [V69y:$i] : (mem(V69y,ty_2Efcp_2Ecart(bool,A_27a20)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a20),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a20),V69y),ap(c_2Ewords_2En2w(A_27a20),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V68x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a20),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V69y)))))) & (( ! [V70x:tp__ty_2Enum_2Enum] : ( ! [V71y:$i] : (mem(V71y,ty_2Efcp_2Ecart(bool,A_27a21)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a21),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a21),V71y),ap(c_2Ewords_2En2w(A_27a21),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V70x)))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a21),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a21),V71y),ap(c_2Ewords_2En2w(A_27a21),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))) & (( ! [V72x:$i] : (mem(V72x,A_27a22) => ( ! [V73y:$i] : (mem(V73y,ty_2Efcp_2Ecart(bool,A_27a23)) => ( ! [V74f:$i] : (mem(V74f,arr(A_27a22,ty_2Enum_2Enum)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a23),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a23),V73y),ap(c_2Ewords_2En2w(A_27a23),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(V74f,V72x))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a23),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a23),V73y),ap(c_2Ewords_2En2w(A_27a23),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V75x:$i] : (mem(V75x,A_27a24) => ( ! [V76y:$i] : (mem(V76y,ty_2Efcp_2Ecart(bool,A_27a25)) => ( ! [V77f:$i] : (mem(V77f,arr(A_27a24,ty_2Enum_2Enum)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a25),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a25),V76y),ap(c_2Ewords_2En2w(A_27a25),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(V77f,V75x))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a25),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a25),V76y),ap(c_2Ewords_2En2w(A_27a25),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))) & (( ! [V78x:tp__ty_2Enum_2Enum] : ( ! [V79y:$i] : (mem(V79y,ty_2Efcp_2Ecart(bool,A_27a26)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a26),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__add(A_27a26),V79y),ap(c_2Ewords_2En2w(A_27a26),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V78x))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a26),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V79y)))))) & ( ! [V80x:tp__ty_2Enum_2Enum] : ( ! [V81y:$i] : (mem(V81y,ty_2Efcp_2Ecart(bool,A_27a27)) => (p(ap(ap(c_2Ealignment_2Ealigned(A_27a27),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Ewords_2Eword__sub(A_27a27),V81y),ap(c_2Ewords_2En2w(A_27a27),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V80x))))))) <=> p(ap(ap(c_2Ealignment_2Ealigned(A_27a27),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),V81y))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
