include('Axioms/HL4001^2.ax').
thf(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum:del )).
thf(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
thf(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : (tp__ty_2Enum_2Enum > $i))).
thf(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : ($i > tp__ty_2Enum_2Enum))).
thf(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem @ (inj__ty_2Enum_2Enum @ X) @ ty_2Enum_2Enum))).
thf(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ ty_2Enum_2Enum) => (X = (inj__ty_2Enum_2Enum @ (surj__ty_2Enum_2Enum @ X)))))).
thf(tp_ty_2Epair_2Eprod,type,( ty_2Epair_2Eprod: del > del >del )).
thf(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : ($i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (mem @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X) @ (ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)) => (X = (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X)))))).
thf(tp_c_2Ebit_2EDIVMOD__2EXP,type,(c_2Ebit_2EDIVMOD__2EXP:$i)).
thf(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))))).
thf(tp_c_2Earithmetic_2EDIV,type,(c_2Earithmetic_2EDIV:$i)).
thf(mem_c_2Earithmetic_2EDIV,axiom,(mem@c_2Earithmetic_2EDIV@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EDIV,type,(fo__c_2Earithmetic_2EDIV:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2EDIV,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2EDIV @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2EDIV @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
thf(mem_c_2Emin_2E_3D_3D_3E,axiom,(mem@c_2Emin_2E_3D_3D_3E@(arr@bool@(arr@bool@bool)))).
thf(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)))))))).
thf(tp_c_2Ecombin_2EI,type,(c_2Ecombin_2EI:(del>$i))).
thf(mem_c_2Ecombin_2EI,axiom,( ! [A_27a:del] : (mem@(c_2Ecombin_2EI@A_27a)@(arr@A_27a@A_27a)))).
thf(tp_c_2Epred__set_2EUNIV,type,(c_2Epred__set_2EUNIV:(del>$i))).
thf(mem_c_2Epred__set_2EUNIV,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EUNIV@A_27a)@(arr@A_27a@bool)))).
thf(tp_c_2Epred__set_2EFINITE,type,(c_2Epred__set_2EFINITE:(del>$i))).
thf(mem_c_2Epred__set_2EFINITE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EFINITE@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(tp_c_2Ebool_2EARB,type,(c_2Ebool_2EARB:(del>$i))).
thf(mem_c_2Ebool_2EARB,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2EARB@A_27a)@A_27a))).
thf(tp_ty_2Eone_2Eone,type,( ty_2Eone_2Eone:del )).
thf(stp_ty_2Eone_2Eone,type,(tp__ty_2Eone_2Eone : $tType)).
thf(stp_inj_ty_2Eone_2Eone,type,(inj__ty_2Eone_2Eone : (tp__ty_2Eone_2Eone > $i))).
thf(stp_surj_ty_2Eone_2Eone,type,(surj__ty_2Eone_2Eone : ($i > tp__ty_2Eone_2Eone))).
thf(stp_inj_surj_ty_2Eone_2Eone,axiom,( ! [X:tp__ty_2Eone_2Eone] : ((surj__ty_2Eone_2Eone @ (inj__ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_ty_2Eone_2Eone,axiom,( ! [X:tp__ty_2Eone_2Eone] : (mem @ (inj__ty_2Eone_2Eone @ X) @ ty_2Eone_2Eone))).
thf(stp_iso_mem_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ ty_2Eone_2Eone) => (X = (inj__ty_2Eone_2Eone @ (surj__ty_2Eone_2Eone @ X)))))).
thf(tp_ty_2Efcp_2Ebit1,type,( ty_2Efcp_2Ebit1: del >del )).
thf(tp_ty_2Efcp_2Ebit0,type,( ty_2Efcp_2Ebit0: del >del )).
thf(tp_ty_2Efcp_2Ecart,type,( ty_2Efcp_2Ecart: del > del >del )).
thf(stp_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))) => (X = (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)))))).
thf(tp_ty_2Ebinary__ieee_2Efloat,type,( ty_2Ebinary__ieee_2Efloat: del > del >del )).
thf(tp_c_2Ebinary__ieee_2Efloat__Significand__fupd,type,(c_2Ebinary__ieee_2Efloat__Significand__fupd:(del>(del>(del>$i))))).
thf(mem_c_2Ebinary__ieee_2Efloat__Significand__fupd,axiom,( ! [A_27t:del] : ( ! [A_27u:del] : ( ! [A_27w:del] : (mem@(c_2Ebinary__ieee_2Efloat__Significand__fupd@A_27t@A_27u@A_27w)@(arr@(arr@(ty_2Efcp_2Ecart@bool@A_27t)@(ty_2Efcp_2Ecart@bool@A_27u))@(arr@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27w)@(ty_2Ebinary__ieee_2Efloat@A_27u@A_27w)))))))).
thf(stp_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))) => (X = (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Exponent__fupd,type,(c_2Ebinary__ieee_2Efloat__Exponent__fupd:(del>(del>(del>$i))))).
thf(mem_c_2Ebinary__ieee_2Efloat__Exponent__fupd,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : ( ! [A_27x:del] : (mem@(c_2Ebinary__ieee_2Efloat__Exponent__fupd@A_27t@A_27w@A_27x)@(arr@(arr@(ty_2Efcp_2Ecart@bool@A_27w)@(ty_2Efcp_2Ecart@bool@A_27x))@(arr@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27w)@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27x)))))))).
thf(stp_c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)))).
thf(stp_iso_mem_c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)) => (X = (inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ X)))))).
thf(tp_c_2Ecombin_2EK,type,(c_2Ecombin_2EK:(del>(del>$i)))).
thf(mem_c_2Ecombin_2EK,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecombin_2EK@A_27a@A_27b)@(arr@A_27a@(arr@A_27b@A_27a)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Sign__fupd,type,(c_2Ebinary__ieee_2Efloat__Sign__fupd:(del>(del>$i)))).
thf(mem_c_2Ebinary__ieee_2Efloat__Sign__fupd,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : (mem@(c_2Ebinary__ieee_2Efloat__Sign__fupd@A_27t@A_27w)@(arr@(arr@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone))@(arr@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27w)@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27w))))))).
thf(stp_c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))).
thf(stp_iso_mem_c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))) => (X = (inj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))) => (X = (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))) => (X = (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@ty_2Eone_2Eone)) => (X = (inj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))) => (X = (inj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit1@ty_2Eone_2Eone)) => (X = (inj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))) => (X = (inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(stp_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : (tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,type,(surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone : ($i > tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X) @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))).
thf(stp_iso_mem_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))) => (X = (inj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (surj__c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ X)))))).
thf(tp_c_2Emachine__ieee_2Efp64__to__float,type,(c_2Emachine__ieee_2Efp64__to__float:$i)).
thf(mem_c_2Emachine__ieee_2Efp64__to__float,axiom,(mem@c_2Emachine__ieee_2Efp64__to__float@(arr@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))).
thf(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
thf(mem_c_2Earithmetic_2E_3E_3D,axiom,(mem@c_2Earithmetic_2E_3E_3D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
thf(mem_c_2Earithmetic_2E_3E,axiom,(mem@c_2Earithmetic_2E_3E@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Enumeral_2EiiSUC,type,(c_2Enumeral_2EiiSUC:$i)).
thf(mem_c_2Enumeral_2EiiSUC,axiom,(mem@c_2Enumeral_2EiiSUC@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiiSUC,type,(fo__c_2Enumeral_2EiiSUC:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Enumeral_2EiZ,type,(c_2Enumeral_2EiZ:$i)).
thf(mem_c_2Enumeral_2EiZ,axiom,(mem@c_2Enumeral_2EiZ@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiZ,type,(fo__c_2Enumeral_2EiZ:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
thf(mem_c_2Ebool_2EF,axiom,(mem@c_2Ebool_2EF@bool)).
thf(ax_false_p,axiom,(~ (p@c_2Ebool_2EF))).
thf(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
thf(mem_c_2Ebool_2ET,axiom,(mem@c_2Ebool_2ET@bool)).
thf(ax_true_p,axiom,(p@c_2Ebool_2ET)).
thf(tp_c_2Enumeral_2EiSUB,type,(c_2Enumeral_2EiSUB:$i)).
thf(mem_c_2Enumeral_2EiSUB,axiom,(mem@c_2Enumeral_2EiSUB@(arr@bool@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
thf(mem_c_2Ebool_2E_7E,axiom,(mem@c_2Ebool_2E_7E@(arr@bool@bool))).
thf(ax_neg_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ((p@(ap@c_2Ebool_2E_7E@Q)) <=> (~ (p@Q)))))).
thf(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
thf(mem_c_2Earithmetic_2EEVEN,axiom,(mem@c_2Earithmetic_2EEVEN@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2Eprim__rec_2E_3C,type,(c_2Eprim__rec_2E_3C:$i)).
thf(mem_c_2Eprim__rec_2E_3C,axiom,(mem@c_2Eprim__rec_2E_3C@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
thf(mem_c_2Enum_2E0,axiom,(mem@c_2Enum_2E0@ty_2Enum_2Enum)).
thf(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Enum_2E0,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0) = c_2Enum_2E0)).
thf(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
thf(mem_c_2Earithmetic_2EEXP,axiom,(mem@c_2Earithmetic_2EEXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Enum_2ESUC,type,(c_2Enum_2ESUC:$i)).
thf(mem_c_2Enum_2ESUC,axiom,(mem@c_2Enum_2ESUC@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enum_2ESUC,type,(fo__c_2Enum_2ESUC:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Enumeral_2Eonecount,type,(c_2Enumeral_2Eonecount:$i)).
thf(mem_c_2Enumeral_2Eonecount,axiom,(mem@c_2Enumeral_2Eonecount@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Enumeral_2Eonecount,type,(fo__c_2Enumeral_2Eonecount:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Enumeral_2Eexactlog,type,(c_2Enumeral_2Eexactlog:$i)).
thf(mem_c_2Enumeral_2Eexactlog,axiom,(mem@c_2Enumeral_2Eexactlog@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2Eexactlog,type,(fo__c_2Enumeral_2Eexactlog:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Eprim__rec_2EPRE,type,(c_2Eprim__rec_2EPRE:$i)).
thf(mem_c_2Eprim__rec_2EPRE,axiom,(mem@c_2Eprim__rec_2EPRE@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eprim__rec_2EPRE,type,(fo__c_2Eprim__rec_2EPRE:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2EDIV2,type,(c_2Earithmetic_2EDIV2:$i)).
thf(mem_c_2Earithmetic_2EDIV2,axiom,(mem@c_2Earithmetic_2EDIV2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EDIV2,type,(fo__c_2Earithmetic_2EDIV2:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Enumeral_2Etexp__help,type,(c_2Enumeral_2Etexp__help:$i)).
thf(mem_c_2Enumeral_2Etexp__help,axiom,(mem@c_2Enumeral_2Etexp__help@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Enumeral_2Etexp__help,type,(fo__c_2Enumeral_2Etexp__help:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
thf(mem_c_2Earithmetic_2EODD,axiom,(mem@c_2Earithmetic_2EODD@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2Ebool_2ELET,type,(c_2Ebool_2ELET:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Enumeral_2Einternal__mult,type,(c_2Enumeral_2Einternal__mult:$i)).
thf(mem_c_2Enumeral_2Einternal__mult,axiom,(mem@c_2Enumeral_2Einternal__mult@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Enumeral_2Einternal__mult,type,(fo__c_2Enumeral_2Einternal__mult:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
thf(mem_c_2Earithmetic_2E_2A,axiom,(mem@c_2Earithmetic_2E_2A@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
thf(mem_c_2Ebool_2E_2F_5C,axiom,(mem@c_2Ebool_2E_2F_5C@(arr@bool@(arr@bool@bool)))).
thf(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)))))))).
thf(tp_c_2Enumeral_2EiDUB,type,(c_2Enumeral_2EiDUB:$i)).
thf(mem_c_2Enumeral_2EiDUB,axiom,(mem@c_2Enumeral_2EiDUB@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiDUB,type,(fo__c_2Enumeral_2EiDUB:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Epair_2E_2C,type,(c_2Epair_2E_2C:(del>(del>$i)))).
thf(mem_c_2Epair_2E_2C,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epair_2E_2C@A_27a@A_27b)@(arr@A_27a@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@A_27b))))))).
thf(tp_c_2Epair_2EUNCURRY,type,(c_2Epair_2EUNCURRY:(del>(del>(del>$i))))).
thf(mem_c_2Epair_2EUNCURRY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Epair_2EUNCURRY@A_27a@A_27b@A_27c)@(arr@(arr@A_27a@(arr@A_27b@A_27c))@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c))))))).
thf(tp_ty_2Ebool_2Eitself,type,( ty_2Ebool_2Eitself: del >del )).
thf(tp_c_2Ewords_2Edimword,type,(c_2Ewords_2Edimword:(del>$i))).
thf(mem_c_2Ewords_2Edimword,axiom,( ! [A_27a:del] : (mem@(c_2Ewords_2Edimword@A_27a)@(arr@(ty_2Ebool_2Eitself@A_27a)@ty_2Enum_2Enum)))).
thf(tp_c_2Earithmetic_2EMOD,type,(c_2Earithmetic_2EMOD:$i)).
thf(mem_c_2Earithmetic_2EMOD,axiom,(mem@c_2Earithmetic_2EMOD@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EMOD,type,(fo__c_2Earithmetic_2EMOD:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2EMOD,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2EMOD @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2EMOD @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
thf(mem_c_2Earithmetic_2E_2B,axiom,(mem@c_2Earithmetic_2E_2B@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
thf(mem_c_2Earithmetic_2E_2D,axiom,(mem@c_2Earithmetic_2E_2D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EMIN,type,(c_2Earithmetic_2EMIN:$i)).
thf(mem_c_2Earithmetic_2EMIN,axiom,(mem@c_2Earithmetic_2EMIN@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EMIN,type,(fo__c_2Earithmetic_2EMIN:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2EMIN,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2EMIN @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2EMIN @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Ebit_2EBITS,type,(c_2Ebit_2EBITS:$i)).
thf(mem_c_2Ebit_2EBITS,axiom,(mem@c_2Ebit_2EBITS@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(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))))).
thf(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))))))).
thf(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
thf(mem_c_2Earithmetic_2E_3C_3D,axiom,(mem@c_2Earithmetic_2E_3C_3D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:(del>$i))).
thf(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2ECOND@A_27a)@(arr@bool@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Ewords_2En2w,type,(c_2Ewords_2En2w:(del>$i))).
thf(mem_c_2Ewords_2En2w,axiom,( ! [A_27a:del] : (mem@(c_2Ewords_2En2w@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Efcp_2Ecart@bool@A_27a))))).
thf(tp_c_2Ewords_2Eword__extract,type,(c_2Ewords_2Eword__extract:(del>(del>$i)))).
thf(mem_c_2Ewords_2Eword__extract,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ewords_2Eword__extract@A_27a@A_27b)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Efcp_2Ecart@bool@A_27a)@(ty_2Efcp_2Ecart@bool@A_27b)))))))).
thf(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:(del>$i))).
thf(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_21@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(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))))))))).
thf(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
thf(mem_c_2Earithmetic_2EZERO,axiom,(mem@c_2Earithmetic_2EZERO@ty_2Enum_2Enum)).
thf(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
thf(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
thf(mem_c_2Earithmetic_2EBIT1,axiom,(mem@c_2Earithmetic_2EBIT1@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
thf(mem_c_2Earithmetic_2EBIT2,axiom,(mem@c_2Earithmetic_2EBIT2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
thf(mem_c_2Earithmetic_2ENUMERAL,axiom,(mem@c_2Earithmetic_2ENUMERAL@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Ebool_2Ethe__value,type,(c_2Ebool_2Ethe__value:(del>$i))).
thf(mem_c_2Ebool_2Ethe__value,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2Ethe__value@A_27a)@(ty_2Ebool_2Eitself@A_27a)))).
thf(tp_c_2Efcp_2Edimindex,type,(c_2Efcp_2Edimindex:(del>$i))).
thf(mem_c_2Efcp_2Edimindex,axiom,( ! [A_27a:del] : (mem@(c_2Efcp_2Edimindex@A_27a)@(arr@(ty_2Ebool_2Eitself@A_27a)@ty_2Enum_2Enum)))).
thf(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:(del>$i))).
thf(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_3D@A_27a)@(arr@A_27a@(arr@A_27a@bool))))).
thf(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)))))))).
thf(conj_thm_2Earithmetic_2EADD__0,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V0m))).
thf(conj_thm_2Earithmetic_2ESUB__0,lemma,( ! [V0m: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 @ V0m))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V0m)))).
thf(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)))))).
thf(conj_thm_2Earithmetic_2EDIV__1,lemma,( ! [V0q:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EDIV@(inj__ty_2Enum_2Enum @ V0q))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = V0q))).
thf(conj_thm_2Earithmetic_2EDIV__DIV__DIV__MULT,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0m))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))) => ( ! [V2x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EDIV@(ap@(ap@c_2Earithmetic_2EDIV@(inj__ty_2Enum_2Enum @ V2x))@(inj__ty_2Enum_2Enum @ V0m)))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EDIV@(inj__ty_2Enum_2Enum @ V2x))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(conj_thm_2Earithmetic_2EEXP__1,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0n))) = (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_2EEXP@(inj__ty_2Enum_2Enum @ V0n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = V0n)))).
thf(conj_thm_2Earithmetic_2EMIN__IDEM,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMIN@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V0n))) = V0n))).
thf(conj_thm_2Ebinary__ieee_2Efloat__literal__11,lemma,( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [V0c11:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V1c01:$i] : ((mem@V1c01@(ty_2Efcp_2Ecart@bool@A_27x)) => ( ! [V2c1:$i] : ((mem@V2c1@(ty_2Efcp_2Ecart@bool@A_27u)) => ( ! [V3c12:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V4c02:$i] : ((mem@V4c02@(ty_2Efcp_2Ecart@bool@A_27x)) => ( ! [V5c2:$i] : ((mem@V5c2@(ty_2Efcp_2Ecart@bool@A_27u)) => (((ap@(ap@(c_2Ebinary__ieee_2Efloat__Sign__fupd@A_27u@A_27x)@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone))@(inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ V0c11)))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Exponent__fupd@A_27u@A_27w@A_27x)@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@A_27x)@(ty_2Efcp_2Ecart@bool@A_27w))@V1c01))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Significand__fupd@A_27t@A_27u@A_27w)@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@A_27u)@(ty_2Efcp_2Ecart@bool@A_27t))@V2c1))@(c_2Ebool_2EARB@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27w))))) = (ap@(ap@(c_2Ebinary__ieee_2Efloat__Sign__fupd@A_27u@A_27x)@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone))@(inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone @ V3c12)))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Exponent__fupd@A_27u@A_27w@A_27x)@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@A_27x)@(ty_2Efcp_2Ecart@bool@A_27w))@V4c02))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Significand__fupd@A_27t@A_27u@A_27w)@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@A_27u)@(ty_2Efcp_2Ecart@bool@A_27t))@V5c2))@(c_2Ebool_2EARB@(ty_2Ebinary__ieee_2Efloat@A_27t@A_27w)))))) <=> ((V0c11 = V3c12) & ((V1c01 = V4c02) & (V2c1 = V5c2))))))))))))))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))))))).
thf(ax_thm_2Ebool_2ELET__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ((c_2Ebool_2ELET@A_27a@A_27b) = (lam@(arr@A_27a@A_27b)@(^ [V0f:$i] : (lam@A_27a@(^ [V1x:$i] : (ap@V0f@V1x))))))))).
thf(ax_thm_2Ebool_2EETA__AX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@A_27b)) => ((lam@A_27a@(^ [V1x:$i] : (ap@V0t@V1x))) = V0t)))))).
thf(conj_thm_2Ebool_2ETRUTH,lemma,$true).
thf(conj_thm_2Ebool_2ELET__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Ebool_2ELET@A_27a@A_27b)@V0f)@V1x) = (ap@V0f@V1x))))))))).
thf(conj_thm_2Ebool_2EAND__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true & (p@V0t)) <=> (p@V0t)) & ((((p@V0t) & $true) <=> (p@V0t)) & ((($false & (p@V0t)) <=> $false) & ((((p@V0t) & $false) <=> $false) & (((p@V0t) & (p@V0t)) <=> (p@V0t))))))))).
thf(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,(( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t)))) & (((~ ($true)) <=> $false) & ((~ ($false)) <=> $true)))).
thf(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((V0x = V0x) <=> $true))))).
thf(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)))))))).
thf(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true <=> (p@V0t)) <=> (p@V0t)) & ((((p@V0t) <=> $true) <=> (p@V0t)) & ((($false <=> (p@V0t)) <=> (~ (p@V0t))) & (((p@V0t) <=> $false) <=> (~ (p@V0t))))))))).
thf(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)@c_2Ebool_2ET)@V0t1)@V1t2) = V0t1) & ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2EF)@V0t1)@V1t2) = V1t2)))))))).
thf(conj_thm_2Ebool_2EAND__IMP__INTRO,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => ( ! [V2t3:$i] : ((mem@V2t3@bool) => (((p@V0t1) => ((p@V1t2) => (p@V2t3))) <=> (((p@V0t1) & (p@V1t2)) => (p@V2t3)))))))))).
thf(conj_thm_2Ebool_2ECOND__CONG,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@bool) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3x_27:$i] : ((mem@V3x_27@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => ( ! [V5y_27:$i] : ((mem@V5y_27@A_27a) => ((((p@V0P) <=> (p@V1Q)) & (((p@V1Q) => (V2x = V3x_27)) & ((~ (p@V1Q)) => (V4y = V5y_27)))) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@V0P)@V2x)@V4y) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@V1Q)@V3x_27)@V5y_27))))))))))))))))).
thf(conj_thm_2Ebool_2Ebool__case__thm,lemma,( ! [A_27a:del]: (( ! [V0t1:$i] : ((mem@V0t1@A_27a) => ( ! [V1t2:$i] : ((mem@V1t2@A_27a) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2ET)@V0t1)@V1t2) = V0t1))))) & ( ! [V2t1:$i] : ((mem@V2t1@A_27a) => ( ! [V3t2:$i] : ((mem@V3t2@A_27a) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2EF)@V2t1)@V3t2) = V3t2)))))))).
thf(conj_thm_2Ecombin_2EI__THM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Ecombin_2EI@A_27a)@V0x) = V0x))))).
thf(conj_thm_2Efcp_2Eindex__bit0,lemma,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum @ (ap@(c_2Efcp_2Edimindex@(ty_2Efcp_2Ebit0@A_27a))@(c_2Ebool_2Ethe__value@(ty_2Efcp_2Ebit0@A_27a)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(c_2Efcp_2Edimindex@A_27a)@(c_2Ebool_2Ethe__value@A_27a))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Efcp_2Efinite__bit0,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Epred__set_2EFINITE@(ty_2Efcp_2Ebit0@A_27a))@(c_2Epred__set_2EUNIV@(ty_2Efcp_2Ebit0@A_27a)))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))))).
thf(conj_thm_2Efcp_2Eindex__bit1,lemma,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum @ (ap@(c_2Efcp_2Edimindex@(ty_2Efcp_2Ebit1@A_27a))@(c_2Ebool_2Ethe__value@(ty_2Efcp_2Ebit1@A_27a)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))@(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@(c_2Efcp_2Edimindex@A_27a)@(c_2Ebool_2Ethe__value@A_27a))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Efcp_2Efinite__bit1,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Epred__set_2EFINITE@(ty_2Efcp_2Ebit1@A_27a))@(c_2Epred__set_2EUNIV@(ty_2Efcp_2Ebit1@A_27a)))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))))).
thf(conj_thm_2Efcp_2Eindex__one,lemma,((surj__ty_2Enum_2Enum @ (ap@(c_2Efcp_2Edimindex@ty_2Eone_2Eone)@(c_2Ebool_2Ethe__value@ty_2Eone_2Eone))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))).
thf(conj_thm_2Efcp_2Efinite__one,lemma,(p@(ap@(c_2Epred__set_2EFINITE@ty_2Eone_2Eone)@(c_2Epred__set_2EUNIV@ty_2Eone_2Eone)))).
thf(ax_thm_2Emachine__ieee_2Efp64__to__float__def,axiom,( ! [V0w:tp__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone] : ((surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (ap@c_2Emachine__ieee_2Efp64__to__float@(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ V0w))) = (surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (ap@(ap@(c_2Ebinary__ieee_2Efloat__Sign__fupd@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone))@(ap@(ap@(ap@(c_2Ewords_2Eword__extract@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))@ty_2Eone_2Eone)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))@(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ V0w))))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Exponent__fupd@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))@(ap@(ap@(ap@(c_2Ewords_2Eword__extract@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ V0w))))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Significand__fupd@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))))@(ap@(ap@(ap@(c_2Ewords_2Eword__extract@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Efcp_2Ecart_o_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ V0w))))@(c_2Ebool_2EARB@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))))))).
thf(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))))))))).
thf(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))))))))))))))))))))))))))))))))))))))).
thf(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)))))))))))))))))))))))))).
thf(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)))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__lt,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))) <=> $true) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))) <=> $true) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) <=> $false) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (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@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (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@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (~ (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))))))))).
thf(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))))))))))))).
thf(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)))))))))).
thf(ax_thm_2Enumeral_2EiDUB,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(inj__ty_2Enum_2Enum @ V0x))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V0x)))))).
thf(conj_thm_2Enumeral_2EiSUB__THM,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1b:$i] : ((mem@V1b@bool) => ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@V1b)@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0x))) = fo__c_2Earithmetic_2EZERO) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = V2n) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(inj__ty_2Enum_2Enum @ V2n)))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))) & ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2EF)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m)))))))))))))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__sub,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@(ap@c_2Enumeral_2EiSUB@c_2Ebool_2ET)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(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))))).
thf(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))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__MIN,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMIN@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0x))) = fo__c_2Enum_2E0) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMIN@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMIN@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0x)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V1y)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1y)))@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1y)))))))))).
thf(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)))))))))).
thf(conj_thm_2Enumeral_2ETWO__EXP__THM,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 @ fo__c_2Enum_2E0))) = (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_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & ((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))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(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)))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V2x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V2x)@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(ap@c_2Earithmetic_2EBIT1@V2x)))))@(ap@(ap@c_2Enumeral_2Eonecount@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(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))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2EODD@V3n))@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EDIV2@V3n))@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1x)))))@(ap@(ap@c_2Enumeral_2Einternal__mult@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1x)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ 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)@(lam@ty_2Enum_2Enum@(^ [V4m:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2EODD@V4m))@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EDIV2@V4m))@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2y)))))@(ap@(ap@c_2Enumeral_2Einternal__mult@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1x)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ 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)@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (ap@(ap@(c_2Ebool_2ELET@ty_2Enum_2Enum@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2EODD@V5m))@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EDIV2@V5m))@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2y)))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2EODD@V6n))@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EDIV2@V6n))@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1x)))))@(ap@(ap@c_2Enumeral_2Einternal__mult@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1x)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2y))))))))@(ap@c_2Enumeral_2Eexactlog@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2y)))))))@(ap@c_2Enumeral_2Eexactlog@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1x))))))))))))))).
thf(conj_thm_2Enumeral__bit_2EiDUB__NUMERAL,lemma,( ! [V0i:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0i)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enumeral_2EiDUB@(inj__ty_2Enum_2Enum @ V0i))))))).
thf(conj_thm_2Epair_2EUNCURRY__DEF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27c))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@A_27c)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)) = (ap@(ap@V0f@V1x)@V2y)))))))))))).
thf(conj_thm_2Ewords_2En2w__11,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((ap@(c_2Ewords_2En2w@A_27a)@(inj__ty_2Enum_2Enum @ V0m)) = (ap@(c_2Ewords_2En2w@A_27a)@(inj__ty_2Enum_2Enum @ V1n))) <=> ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Ewords_2Edimword@A_27a)@(c_2Ebool_2Ethe__value@A_27a)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Ewords_2Edimword@A_27a)@(c_2Ebool_2Ethe__value@A_27a)))))))))).
thf(conj_thm_2Ewords_2Eword__extract__n2w,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1l:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@(ap@(ap@(c_2Ewords_2Eword__extract@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V0h))@(inj__ty_2Enum_2Enum @ V1l))@(ap@(c_2Ewords_2En2w@A_27a)@(inj__ty_2Enum_2Enum @ V2n))) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Efcp_2Ecart@bool@A_27b))@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Efcp_2Edimindex@A_27b)@(c_2Ebool_2Ethe__value@A_27b)))@(ap@(c_2Efcp_2Edimindex@A_27a)@(c_2Ebool_2Ethe__value@A_27a))))@(ap@(c_2Ewords_2En2w@A_27b)@(ap@(ap@(ap@c_2Ebit_2EBITS@(ap@(ap@c_2Earithmetic_2EMIN@(inj__ty_2Enum_2Enum @ V0h))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Efcp_2Edimindex@A_27a)@(c_2Ebool_2Ethe__value@A_27a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(inj__ty_2Enum_2Enum @ V1l))@(inj__ty_2Enum_2Enum @ V2n))))@(ap@(c_2Ewords_2En2w@A_27b)@(ap@(ap@(ap@c_2Ebit_2EBITS@(ap@(ap@c_2Earithmetic_2EMIN@(ap@(ap@c_2Earithmetic_2EMIN@(inj__ty_2Enum_2Enum @ V0h))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Efcp_2Edimindex@A_27a)@(c_2Ebool_2Ethe__value@A_27a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Efcp_2Edimindex@A_27a)@(c_2Ebool_2Ethe__value@A_27a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Enum_2Enum @ V1l))))@(inj__ty_2Enum_2Enum @ V1l))@(inj__ty_2Enum_2Enum @ V2n))))))))))).
thf(conj_thm_2Ewords_2Edimindex__1,lemma,((surj__ty_2Enum_2Enum @ (ap@(c_2Efcp_2Edimindex@ty_2Eone_2Eone)@(c_2Ebool_2Ethe__value@ty_2Eone_2Eone))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))).
thf(conj_thm_2Ewords_2Edimindex__11,lemma,((surj__ty_2Enum_2Enum @ (ap@(c_2Efcp_2Edimindex@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(c_2Ebool_2Ethe__value@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Ewords_2Edimindex__64,lemma,((surj__ty_2Enum_2Enum @ (ap@(c_2Efcp_2Edimindex@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))@(c_2Ebool_2Ethe__value@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(conj_thm_2Emachine__ieee_2Efp64__to__float__n2w,conjecture,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (ap@c_2Emachine__ieee_2Efp64__to__float@(ap@(c_2Ewords_2En2w@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))))@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__c_ty_2Ebinary__ieee_2Efloat_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_c_ty_2Efcp_2Ebit1_ty_2Eone_2Eone_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit1_c_ty_2Efcp_2Ebit0_ty_2Eone_2Eone @ (ap@(ap@(c_2Ebool_2ELET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))@(lam@ty_2Enum_2Enum@(^ [V1q:$i] : (lam@ty_2Enum_2Enum@(^ [V2f:$i] : (ap@(ap@(c_2Ebool_2ELET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))@(lam@ty_2Enum_2Enum@(^ [V3s:$i] : (lam@ty_2Enum_2Enum@(^ [V4e:$i] : (ap@(ap@(c_2Ebinary__ieee_2Efloat__Sign__fupd@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone))@(ap@(c_2Ewords_2En2w@ty_2Eone_2Eone)@(ap@(ap@c_2Earithmetic_2EMOD@V3s)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Exponent__fupd@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone)))))@(ap@(c_2Ewords_2En2w@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@V4e)))@(ap@(ap@(c_2Ebinary__ieee_2Efloat__Significand__fupd@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))@(ap@(c_2Ecombin_2EK@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))@(ty_2Efcp_2Ecart@bool@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))))@(ap@(c_2Ewords_2En2w@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone))))))@V2f)))@(c_2Ebool_2EARB@(ty_2Ebinary__ieee_2Efloat@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@(ty_2Efcp_2Ebit1@ty_2Eone_2Eone)))))@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit1@(ty_2Efcp_2Ebit0@ty_2Eone_2Eone))))))))))))))@(ap@(ap@c_2Ebit_2EDIVMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@V1q))))))))@(ap@(ap@c_2Ebit_2EDIVMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(inj__ty_2Enum_2Enum @ V0n))))))).
