include('Axioms/numpair_2.ax').
tff(tp_c_2Ebit_2EBIT,type,(c_2Ebit_2EBIT:$i)).
tff(mem_c_2Ebit_2EBIT,axiom,mem(c_2Ebit_2EBIT,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Ebit_2EBIT,type,(fo__c_2Ebit_2EBIT:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Ebit_2EBIT,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Ebit_2EBIT(X0,X1)) = ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2EBITS,type,(c_2Ebit_2EBITS:$i)).
tff(mem_c_2Ebit_2EBITS,axiom,mem(c_2Ebit_2EBITS,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(stp_fo_c_2Ebit_2EBITS,type,(fo__c_2Ebit_2EBITS:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2EBITS,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2EBITS(X0,X1,X2)) = ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2Ebit_2EBITV,type,(c_2Ebit_2EBITV:$i)).
tff(mem_c_2Ebit_2EBITV,axiom,mem(c_2Ebit_2EBITV,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Ebit_2EBITV,type,(fo__c_2Ebit_2EBITV:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2EBITV,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2EBITV(X0,X1)) = ap(ap(c_2Ebit_2EBITV,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2EBITWISE,type,(c_2Ebit_2EBITWISE:$i)).
tff(mem_c_2Ebit_2EBITWISE,axiom,mem(c_2Ebit_2EBITWISE,arr(ty_2Enum_2Enum,arr(arr(bool,arr(bool,bool)),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))))).
tff(tp_c_2Ebit_2EBIT__MODIFY,type,(c_2Ebit_2EBIT__MODIFY:$i)).
tff(mem_c_2Ebit_2EBIT__MODIFY,axiom,mem(c_2Ebit_2EBIT__MODIFY,arr(ty_2Enum_2Enum,arr(arr(ty_2Enum_2Enum,arr(bool,bool)),arr(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(tp_c_2Ebit_2EBIT__REVERSE,type,(c_2Ebit_2EBIT__REVERSE:$i)).
tff(mem_c_2Ebit_2EBIT__REVERSE,axiom,mem(c_2Ebit_2EBIT__REVERSE,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Ebit_2EBIT__REVERSE,type,(fo__c_2Ebit_2EBIT__REVERSE:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2EBIT__REVERSE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2EBIT__REVERSE(X0,X1)) = ap(ap(c_2Ebit_2EBIT__REVERSE,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2EDIVMOD__2EXP,type,(c_2Ebit_2EDIVMOD__2EXP:$i)).
tff(mem_c_2Ebit_2EDIVMOD__2EXP,axiom,mem(c_2Ebit_2EDIVMOD__2EXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(tp_c_2Ebit_2EDIV__2EXP,type,(c_2Ebit_2EDIV__2EXP:$i)).
tff(mem_c_2Ebit_2EDIV__2EXP,axiom,mem(c_2Ebit_2EDIV__2EXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Ebit_2EDIV__2EXP,type,(fo__c_2Ebit_2EDIV__2EXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2EDIV__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2EDIV__2EXP(X0,X1)) = ap(ap(c_2Ebit_2EDIV__2EXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2ELOG2,type,(c_2Ebit_2ELOG2:$i)).
tff(mem_c_2Ebit_2ELOG2,axiom,mem(c_2Ebit_2ELOG2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebit_2ELOG2,type,(fo__c_2Ebit_2ELOG2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2ELOG2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2ELOG2(X0)) = ap(c_2Ebit_2ELOG2,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebit_2ELOWEST__SET__BIT,type,(c_2Ebit_2ELOWEST__SET__BIT:$i)).
tff(mem_c_2Ebit_2ELOWEST__SET__BIT,axiom,mem(c_2Ebit_2ELOWEST__SET__BIT,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebit_2ELOWEST__SET__BIT,type,(fo__c_2Ebit_2ELOWEST__SET__BIT:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2ELOWEST__SET__BIT,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2ELOWEST__SET__BIT(X0)) = ap(c_2Ebit_2ELOWEST__SET__BIT,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebit_2EMOD__2EXP,type,(c_2Ebit_2EMOD__2EXP:$i)).
tff(mem_c_2Ebit_2EMOD__2EXP,axiom,mem(c_2Ebit_2EMOD__2EXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Ebit_2EMOD__2EXP,type,(fo__c_2Ebit_2EMOD__2EXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2EMOD__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2EMOD__2EXP(X0,X1)) = ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2EMOD__2EXP__EQ,type,(c_2Ebit_2EMOD__2EXP__EQ:$i)).
tff(mem_c_2Ebit_2EMOD__2EXP__EQ,axiom,mem(c_2Ebit_2EMOD__2EXP__EQ,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))))).
tff(stp_fo_c_2Ebit_2EMOD__2EXP__EQ,type,(fo__c_2Ebit_2EMOD__2EXP__EQ:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Ebit_2EMOD__2EXP__EQ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Ebit_2EMOD__2EXP__EQ(X0,X1,X2)) = ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2Ebit_2EMOD__2EXP__MAX,type,(c_2Ebit_2EMOD__2EXP__MAX:$i)).
tff(mem_c_2Ebit_2EMOD__2EXP__MAX,axiom,mem(c_2Ebit_2EMOD__2EXP__MAX,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Ebit_2EMOD__2EXP__MAX,type,(fo__c_2Ebit_2EMOD__2EXP__MAX:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Ebit_2EMOD__2EXP__MAX,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Ebit_2EMOD__2EXP__MAX(X0,X1)) = ap(ap(c_2Ebit_2EMOD__2EXP__MAX,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2ESBIT,type,(c_2Ebit_2ESBIT:$i)).
tff(mem_c_2Ebit_2ESBIT,axiom,mem(c_2Ebit_2ESBIT,arr(bool,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Ebit_2ESBIT,type,(fo__c_2Ebit_2ESBIT:(tp__o * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2ESBIT,axiom,( ! [X0:tp__o] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2ESBIT(X0,X1)) = ap(ap(c_2Ebit_2ESBIT,inj__o(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebit_2ESIGN__EXTEND,type,(c_2Ebit_2ESIGN__EXTEND:$i)).
tff(mem_c_2Ebit_2ESIGN__EXTEND,axiom,mem(c_2Ebit_2ESIGN__EXTEND,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(stp_fo_c_2Ebit_2ESIGN__EXTEND,type,(fo__c_2Ebit_2ESIGN__EXTEND:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2ESIGN__EXTEND,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2ESIGN__EXTEND(X0,X1,X2)) = ap(ap(ap(c_2Ebit_2ESIGN__EXTEND,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2Ebit_2ESLICE,type,(c_2Ebit_2ESLICE:$i)).
tff(mem_c_2Ebit_2ESLICE,axiom,mem(c_2Ebit_2ESLICE,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(stp_fo_c_2Ebit_2ESLICE,type,(fo__c_2Ebit_2ESLICE:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2ESLICE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2ESLICE(X0,X1,X2)) = ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2Ebit_2ETIMES__2EXP,type,(c_2Ebit_2ETIMES__2EXP:$i)).
tff(mem_c_2Ebit_2ETIMES__2EXP,axiom,mem(c_2Ebit_2ETIMES__2EXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Ebit_2ETIMES__2EXP,type,(fo__c_2Ebit_2ETIMES__2EXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebit_2ETIMES__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Ebit_2ETIMES__2EXP(X0,X1)) = ap(ap(c_2Ebit_2ETIMES__2EXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(ax_thm_2Ebit_2EMOD__2EXP__def,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1n)),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(V0x)))))))).
tff(ax_thm_2Ebit_2EDIV__2EXP__def,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EDIV__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1n)),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(V0x)))))))).
tff(ax_thm_2Ebit_2ETIMES__2EXP__def,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ETIMES__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),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(V0x)))))))).
tff(ax_thm_2Ebit_2EDIVMOD__2EXP__def,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Ebit_2EDIVMOD__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1n)),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(V0x)))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1n)),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(V0x))))))))).
tff(ax_thm_2Ebit_2ESBIT__def,axiom,( ! [V0b:tp__o] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ESBIT,inj__o(V0b)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(V0b)),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(V1n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(ax_thm_2Ebit_2EBITS__def,axiom,( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EMOD__2EXP,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l))),ap(ap(c_2Ebit_2EDIV__2EXP,inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(ax_thm_2Ebit_2EBITV__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EBITV,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1b))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V0n))))))).
tff(ax_thm_2Ebit_2EBIT__def,axiom,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n))) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(ax_thm_2Ebit_2ESLICE__def,axiom,( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Ebit_2EMOD__2EXP,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(ax_thm_2Ebit_2ELOG2__def,axiom,(c_2Ebit_2ELOG2 = ap(c_2Elogroot_2ELOG,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))).
tff(ax_thm_2Ebit_2ELOWEST__SET__BIT__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Ebit_2ELOWEST__SET__BIT,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Ewhile_2ELEAST,f249(V0n)))))).
tff(ax_thm_2Ebit_2EBIT__REVERSE__def,axiom,(( ! [V0x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EBIT__REVERSE,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0x))) = fo__c_2Enum_2E0)) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EBIT__REVERSE,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2x))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Ebit_2EBIT__REVERSE,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ebit_2ESBIT,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2x))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(ax_thm_2Ebit_2EBITWISE__def,axiom,(( ! [V0op:$i] : (mem(V0op,arr(bool,arr(bool,bool))) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2y:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0op),inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V2y))) = fo__c_2Enum_2E0))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4op:$i] : (mem(V4op,arr(bool,arr(bool,bool))) => ( ! [V5x:tp__ty_2Enum_2Enum] : ( ! [V6y:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n))),V4op),inj__ty_2Enum_2Enum(V5x)),inj__ty_2Enum_2Enum(V6y))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(V3n)),V4op),inj__ty_2Enum_2Enum(V5x)),inj__ty_2Enum_2Enum(V6y))),ap(ap(c_2Ebit_2ESBIT,ap(ap(V4op,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V3n)),inj__ty_2Enum_2Enum(V5x))),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V3n)),inj__ty_2Enum_2Enum(V6y)))),inj__ty_2Enum_2Enum(V3n)))))))))))).
tff(ax_thm_2Ebit_2EBIT__MODIFY__def,axiom,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,arr(bool,bool))) => ( ! [V1x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBIT__MODIFY,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0f),inj__ty_2Enum_2Enum(V1x))) = fo__c_2Enum_2E0)))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3f:$i] : (mem(V3f,arr(ty_2Enum_2Enum,arr(bool,bool))) => ( ! [V4x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBIT__MODIFY,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),V3f),inj__ty_2Enum_2Enum(V4x))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2EBIT__MODIFY,inj__ty_2Enum_2Enum(V2n)),V3f),inj__ty_2Enum_2Enum(V4x))),ap(ap(c_2Ebit_2ESBIT,ap(ap(V3f,inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V4x)))),inj__ty_2Enum_2Enum(V2n))))))))))).
tff(ax_thm_2Ebit_2ESIGN__EXTEND__def,axiom,( ! [V0l:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESIGN__EXTEND,inj__ty_2Enum_2Enum(V0l)),inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Enum_2Enum),f250(V0l,V2n,V1h)),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2n)),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(V0l)))))))))).
tff(ax_thm_2Ebit_2EMOD__2EXP__EQ__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2Ebit_2EMOD__2EXP__EQ,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a)),inj__ty_2Enum_2Enum(V2b))) <=> (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2b))))))))).
tff(ax_thm_2Ebit_2EMOD__2EXP__MAX__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EMOD__2EXP__MAX,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) <=> (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,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(V0n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Ebit_2ELESS__MULT__MONO2,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ( ! [V3y:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V2x))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V3y)))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2x)),inj__ty_2Enum_2Enum(V3y))))))))))).
tff(conj_thm_2Ebit_2ELOG2__UNIQUE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,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(V1p))),inj__ty_2Enum_2Enum(V0n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1p)))))) => (surj__ty_2Enum_2Enum(ap(c_2Ebit_2ELOG2,inj__ty_2Enum_2Enum(V0n))) = V1p)))))).
tff(conj_thm_2Ebit_2ELOG2__TWOEXP,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Ebit_2ELOG2,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(V0n)))) = V0n)))).
tff(conj_thm_2Ebit_2EDIVMOD__2EXP,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Ebit_2EDIVMOD__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(ap(c_2Ebit_2EDIV__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Ebit_2EMOD__2EXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Ebit_2ESUC__SUB,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0a))),inj__ty_2Enum_2Enum(V0a))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Ebit_2EDIV__MULT__1,lemma,(( ! [V0r:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0r)),inj__ty_2Enum_2Enum(V1n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0r))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Ebit_2ENOT__ZERO__ADD1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ((~~ (V0m = fo__c_2Enum_2E0)) => (? [V1p:tp__ty_2Enum_2Enum] : (V0m = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1p))))))))).
tff(conj_thm_2Ebit_2EZERO__LT__TWOEXP,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),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(V0n))))))).
tff(conj_thm_2Ebit_2EONE__LE__TWOEXP,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),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(V0n))))))).
tff(conj_thm_2Ebit_2ETWOEXP__NOT__ZERO,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (~~ (surj__ty_2Enum_2Enum(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(V0n))) = fo__c_2Enum_2E0))))).
tff(conj_thm_2Ebit_2EMOD__2EXP__LT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),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(V0n)))),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(V0n)))))))).
tff(conj_thm_2Ebit_2ETWOEXP__DIVISION,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : (V1k = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1k)),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(V0n)))),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(V0n)))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),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(V0n)))))))))).
tff(conj_thm_2Ebit_2ETWOEXP__MONO,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) => p(ap(ap(c_2Eprim__rec_2E_3C,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(V0a))),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(V1b))))))))).
tff(conj_thm_2Ebit_2ETWOEXP__MONO2,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,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(V0a))),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(V1b))))))))).
tff(conj_thm_2Ebit_2EEXP__SUB__LESS__EQ,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b)))),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(V0a)))))))).
tff(conj_thm_2Ebit_2EMOD__LEQ,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1b))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))),inj__ty_2Enum_2Enum(V0a)))))))).
tff(conj_thm_2Ebit_2EBITS__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2n)),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(V1l)))),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l))))))))))).
tff(conj_thm_2Ebit_2EBITSLT__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l)))))))))).
tff(conj_thm_2Ebit_2EBITSLT__THM2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h)))))))))).
tff(conj_thm_2Ebit_2EBITS__THM2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))))),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(V1l)))))))))).
tff(conj_thm_2Ebit_2EBITS__LEQ,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V2n)))))))).
tff(conj_thm_2Ebit_2EBITS__COMP__THM,lemma,(( ! [V0h1:tp__ty_2Enum_2Enum] : ( ! [V1l1:tp__ty_2Enum_2Enum] : ( ! [V2h2:tp__ty_2Enum_2Enum] : ( ! [V3l2:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2h2)),inj__ty_2Enum_2Enum(V1l1))),inj__ty_2Enum_2Enum(V0h1))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V2h2)),inj__ty_2Enum_2Enum(V3l2)),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h1)),inj__ty_2Enum_2Enum(V1l1)),inj__ty_2Enum_2Enum(V4n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2h2)),inj__ty_2Enum_2Enum(V1l1))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3l2)),inj__ty_2Enum_2Enum(V1l1))),inj__ty_2Enum_2Enum(V4n)))))))))))).
tff(conj_thm_2Ebit_2EBITS__DIV__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2x))),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(V3n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V3n))),inj__ty_2Enum_2Enum(V2x)))))))))).
tff(conj_thm_2Ebit_2EBITS__LT__HIGH,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2n)),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(V1l))))))))))).
tff(conj_thm_2Ebit_2EBITS__ZERO,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Ebit_2EBITS__ZERO2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0))))).
tff(conj_thm_2Ebit_2EBITS__ZERO3,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h)))))))))).
tff(conj_thm_2Ebit_2EBITS__ZERO4,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V0h))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2a)),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(V1l))))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2a)))))))))).
tff(conj_thm_2Ebit_2EBITS__ZEROL,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1a)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1a))) = V1a)))))).
tff(conj_thm_2Ebit_2EBITS__LOG2__ZERO__ID,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Ebit_2ELOG2,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = V0n))))).
tff(conj_thm_2Ebit_2EBITS__LT__LOW,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),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(V1l)))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Ebit_2EBIT__ZERO,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Ebit_2EBIT__B,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),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(V0b))))))).
tff(conj_thm_2Ebit_2EBIT__TWO__POW,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),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)))) <=> (V1m = V0n)))))).
tff(conj_thm_2Ebit_2EBIT__B__NEQ,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((~~ (V0a = V1b)) => (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0a)),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(V1b)))))))))).
tff(conj_thm_2Ebit_2EBITS__COMP__THM2,lemma,(( ! [V0h1:tp__ty_2Enum_2Enum] : ( ! [V1l1:tp__ty_2Enum_2Enum] : ( ! [V2h2:tp__ty_2Enum_2Enum] : ( ! [V3l2:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V2h2)),inj__ty_2Enum_2Enum(V3l2)),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h1)),inj__ty_2Enum_2Enum(V1l1)),inj__ty_2Enum_2Enum(V4n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(ap(c_2Earithmetic_2EMIN,inj__ty_2Enum_2Enum(V0h1)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2h2)),inj__ty_2Enum_2Enum(V1l1)))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V3l2)),inj__ty_2Enum_2Enum(V1l1))),inj__ty_2Enum_2Enum(V4n))))))))))).
tff(conj_thm_2Ebit_2ENOT__MOD2__LEM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = fo__c_2Enum_2E0)) <=> (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Ebit_2ENOT__MOD2__LEM2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = 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(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = fo__c_2Enum_2E0))))).
tff(conj_thm_2Ebit_2EODD__MOD2__LEM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n))) <=> (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Ebit_2EDIV__MULT__THM,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1n)),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(V0x)))),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(V0x)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1n)),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(V0x)))))))))).
tff(conj_thm_2Ebit_2EDIV__MULT__THM2,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)))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Ebit_2ELESS__EQ__EXP__MULT,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))) => (? [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(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(V1b))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,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(V0a))))))))))).
tff(conj_thm_2Ebit_2ESLICE__THM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V0n))),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(V2l)))))))))).
tff(conj_thm_2Ebit_2ESLICELT__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h)))))))))).
tff(conj_thm_2Ebit_2EBITS__SLICE__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(conj_thm_2Ebit_2EBITS__SLICE__THM2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1h2:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1h2))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V1h2)),inj__ty_2Enum_2Enum(V2l)),ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n))))))))))).
tff(conj_thm_2Ebit_2ESLICE__ZERO__THM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Ebit_2EMOD__2EXP__MONO,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V1h))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),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(V2l)))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1h)))))))))))).
tff(conj_thm_2Ebit_2ESLICE__COMP__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V0h))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V1m)))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V3n))),ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n))))))))))).
tff(conj_thm_2Ebit_2ESLICE__COMP__RWT,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1m_27:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V3l)),inj__ty_2Enum_2Enum(V2m))) & ((V1m_27 = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V0h))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1m_27)),inj__ty_2Enum_2Enum(V4n))),ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V3l)),inj__ty_2Enum_2Enum(V4n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V3l)),inj__ty_2Enum_2Enum(V4n)))))))))))).
tff(conj_thm_2Ebit_2ESLICE__ZERO,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Ebit_2ESLICE__ZERO2,lemma,(( ! [V0l:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(V0l)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0))))).
tff(conj_thm_2Ebit_2EBITS__SUM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3b)),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(V1l)))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2a)),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(V1l)))),inj__ty_2Enum_2Enum(V3b)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2a)),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(V1l))))))))))))).
tff(conj_thm_2Ebit_2EBITS__SUM2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2a)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))))),inj__ty_2Enum_2Enum(V3b)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V3b)))))))))).
tff(conj_thm_2Ebit_2ESLICE__COMP__THM2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ( ! [V3y:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V2x))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V3y)),inj__ty_2Enum_2Enum(V1l)))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V2x)),inj__ty_2Enum_2Enum(V3y)),inj__ty_2Enum_2Enum(V4n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V4n)))))))))))).
tff(conj_thm_2Ebit_2EBITS__SUM3,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1a))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2b))))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1a)),inj__ty_2Enum_2Enum(V2b)))))))))).
tff(conj_thm_2Ebit_2EBITS__MUL,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2A,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1a))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2b))))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1a)),inj__ty_2Enum_2Enum(V2b)))))))))).
tff(conj_thm_2Ebit_2EBIT__COMP__THM3,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V0h))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V1m)))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V3n))),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V2l))))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n))))))))))).
tff(conj_thm_2Ebit_2ENOT__BIT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a)))) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Ebit_2ENOT__BITS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ((~~ (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = fo__c_2Enum_2E0)) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Ebit_2ENOT__BITS2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ((~~ (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = 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(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Ebit_2EBIT__SLICE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) <=> p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2b)))) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2b)))))))))).
tff(conj_thm_2Ebit_2EBIT__SLICE__LEM,lemma,(( ! [V0y:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ESBIT,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0y)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V2n))),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(V0y)))))))))).
tff(conj_thm_2Ebit_2EBIT__SLICE__THM,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ESBIT,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0x))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Ebit_2EBIT__SLICE__THM2,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n))) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(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(V0b))))))))).
tff(conj_thm_2Ebit_2EBIT__SLICE__THM3,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n)))) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Ebit_2EBIT__SLICE__THM4,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),ap(ap(ap(c_2Ebit_2ESLICE,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3n)))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V0b))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1h))) & p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V3n)))))))))))).
tff(conj_thm_2Ebit_2ESBIT__DIV,lemma,(( ! [V0b:tp__o] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V1m))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ESBIT,inj__o(V0b)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Ebit_2ESBIT,inj__o(V0b)),inj__ty_2Enum_2Enum(V1m))),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(V2n))))))))))).
tff(conj_thm_2Ebit_2EBITS__SUC,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1l)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h)))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Ebit_2ESBIT,ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l)))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n)))))))))).
tff(conj_thm_2Ebit_2EBITS__SUC__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Ebit_2ESBIT,ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0h))),inj__ty_2Enum_2Enum(V1l)))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2n))))))))))).
tff(conj_thm_2Ebit_2EBIT__BITS__THM,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : (( ! [V4x:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V4x))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V4x)),inj__ty_2Enum_2Enum(V0h)))) => (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V4x)),inj__ty_2Enum_2Enum(V2a))) <=> p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V4x)),inj__ty_2Enum_2Enum(V3b)))))) <=> (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2a))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V3b))))))))))).
tff(conj_thm_2Ebit_2EBITS__ZERO5,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (( ! [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V0n))) => (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V1m)))))) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1m))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Ebit_2EBIT0__ODD,lemma,((ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = c_2Earithmetic_2EODD))).
tff(conj_thm_2Ebit_2EBITV__THM,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2EBITV,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0b))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ESBIT,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Ebit_2EADD__BIT0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (~~ (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) <=> p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Ebit_2EADD__BITS__SUC,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1a)),inj__ty_2Enum_2Enum(V2b)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1a))),ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2b)))),ap(ap(ap(c_2Ebit_2EBITS,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1a))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2b)))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Ebit_2EADD__BIT__SUC,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1a)),inj__ty_2Enum_2Enum(V2b)))) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1a))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2b))))),ap(ap(c_2Emin_2E_3D(bool),ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1a))),ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2b)))),ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D(bool),ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1a))),ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2b)))))))))))).
tff(conj_thm_2Ebit_2EBITWISE__LT__2EXP,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1op:$i] : (mem(V1op,arr(bool,arr(bool,bool))) => ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(V0n)),V1op),inj__ty_2Enum_2Enum(V2a)),inj__ty_2Enum_2Enum(V3b))),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(V0n))))))))))).
tff(conj_thm_2Ebit_2EBITWISE__THM,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2op:$i] : (mem(V2op,arr(bool,arr(bool,bool))) => ( ! [V3a:tp__ty_2Enum_2Enum] : ( ! [V4b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) => (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(V1n)),V2op),inj__ty_2Enum_2Enum(V3a)),inj__ty_2Enum_2Enum(V4b)))) <=> p(ap(ap(V2op,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V3a))),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V4b)))))))))))))).
tff(conj_thm_2Ebit_2EBITWISE__COR,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2op:$i] : (mem(V2op,arr(bool,arr(bool,bool))) => ( ! [V3a:tp__ty_2Enum_2Enum] : ( ! [V4b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) => (p(ap(ap(V2op,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V3a))),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V4b)))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2EDIV,ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(V1n)),V2op),inj__ty_2Enum_2Enum(V3a)),inj__ty_2Enum_2Enum(V4b))),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(V0x)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))).
tff(conj_thm_2Ebit_2EBITWISE__NOT__COR,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2op:$i] : (mem(V2op,arr(bool,arr(bool,bool))) => ( ! [V3a:tp__ty_2Enum_2Enum] : ( ! [V4b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))) => ((~~ p(ap(ap(V2op,ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V3a))),ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V4b))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2EDIV,ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(V1n)),V2op),inj__ty_2Enum_2Enum(V3a)),inj__ty_2Enum_2Enum(V4b))),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(V0x)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2Ebit_2EBITWISE__BITS,lemma,(( ! [V0wl:tp__ty_2Enum_2Enum] : ( ! [V1op:$i] : (mem(V1op,arr(bool,arr(bool,bool))) => ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0wl))),V1op),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0wl)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2a))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0wl)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3b)))) = surj__ty_2Enum_2Enum(ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0wl))),V1op),inj__ty_2Enum_2Enum(V2a)),inj__ty_2Enum_2Enum(V3b))))))))))).
tff(conj_thm_2Ebit_2ENOT__BIT__GT__TWOEXP,lemma,(( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),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(V0i)))) => (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Ebit_2EBIT__IMP__GE__TWOEXP,lemma,(( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,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(V0i))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Ebit_2EBITWISE__ONE__COMP__LEM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),f251),inj__ty_2Enum_2Enum(V1a)),inj__ty_2Enum_2Enum(V2b))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1a)))))))))).
tff(conj_thm_2Ebit_2EBIT__COMPLEMENT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V1i)),ap(ap(c_2Earithmetic_2E_2D,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(V0n))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2a)),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(V0n)))))) <=> (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2a)),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(V0n)))) = fo__c_2Enum_2E0) & (V1i = V0n)) | ((~~ (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2a)),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(V0n)))) = fo__c_2Enum_2E0)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V0n))) & (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V1i)),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2a)),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(V0n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))).
tff(conj_thm_2Ebit_2EBIT__OF__BITS__THM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1h:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__ty_2Enum_2Enum] : ( ! [V3a:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1h))) => (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V1h)),inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V3a)))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2l)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V3a))))))))))).
tff(conj_thm_2Ebit_2EBIT__SHIFT__THM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2s:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2s))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1a)),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(V2s))))) <=> p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1a))))))))).
tff(conj_thm_2Ebit_2EBIT__SHIFT__THM2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2s:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2s)),inj__ty_2Enum_2Enum(V0n))) => (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1a)),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(V2s))))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2s))),inj__ty_2Enum_2Enum(V1a)))))))))).
tff(conj_thm_2Ebit_2EBIT__SHIFT__THM3,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2s:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2s))) => (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1a)),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(V2s)))))))))))).
tff(conj_thm_2Ebit_2EBIT__OF__BITS__THM2,lemma,(( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0h)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V2x)))) => (~~ p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V2x)),ap(ap(ap(c_2Ebit_2EBITS,inj__ty_2Enum_2Enum(V0h)),inj__ty_2Enum_2Enum(V1l)),inj__ty_2Enum_2Enum(V3n)))))))))))).
tff(conj_thm_2Ebit_2EBIT__DIV2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1i)))))))).
tff(conj_thm_2Ebit_2EBIT__SHIFT__THM4,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V1i)),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2a)),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(V0n))))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2a))))))))).
tff(conj_thm_2Ebit_2EDIV__LT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2a)),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))))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2a)),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(V0n)))),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)))))))))).
tff(conj_thm_2Ebit_2EMOD__ZERO__GT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Enum_2Enum] : (((~~ (V1a = fo__c_2Enum_2E0)) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1a)),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(V0n)))) = fo__c_2Enum_2E0)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,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(V0n))),inj__ty_2Enum_2Enum(V1a)))))))).
tff(conj_thm_2Ebit_2EDIV__GT0,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V0a))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1b)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))))))))).
tff(conj_thm_2Ebit_2EDIV__SUB1,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,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(V1b))),inj__ty_2Enum_2Enum(V0a))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0a)),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(V1b)))) = fo__c_2Enum_2E0)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0a)),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(V1b)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0a)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),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(V1b)))))))))).
tff(conj_thm_2Ebit_2EBIT__EXP__SUB1,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V0b)),ap(ap(c_2Earithmetic_2E_2D,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(V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Ebit_2EBIT__SHIFT__THM5,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3a:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3a)),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))))) => (p(ap(ap(c_2Ebit_2EBIT,inj__ty_2Enum_2Enum(V2i)),ap(ap(c_2Earithmetic_2E_2D,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))),ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V3a)),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(V0n)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V3a)),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(V0n)))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),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)))))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2E_2D,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))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V3a)),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)))))))))))))).
tff(conj_thm_2Ebit_2ESBIT__MULT,lemma,(( ! [V0b:tp__o] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Ebit_2ESBIT,inj__o(V0b)),inj__ty_2Enum_2Enum(V2n))),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)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Ebit_2ESBIT,inj__o(V0b)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V1m)))))))))).
tff(conj_thm_2Ebit_2EBITWISE__EVAL,conjecture,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1op:$i] : (mem(V1op,arr(bool,arr(bool,bool))) => ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),V1op),inj__ty_2Enum_2Enum(V2a)),inj__ty_2Enum_2Enum(V3b))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(ap(ap(c_2Ebit_2EBITWISE,inj__ty_2Enum_2Enum(V0n)),V1op),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2a)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V3b)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),ap(ap(c_2Ebit_2ESBIT,ap(ap(V1op,ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V2a))),ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V3b)))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
