include('Axioms/complex^2.ax').
thf(tp_ty_2Eieee_2Eccode,type,( ty_2Eieee_2Eccode:del )).
thf(tp_ty_2Eieee_2Efloat,type,( ty_2Eieee_2Efloat:del )).
thf(tp_ty_2Eieee_2Eroundmode,type,( ty_2Eieee_2Eroundmode:del )).
thf(stp_ty_2Eieee_2Eccode,type,(tp__ty_2Eieee_2Eccode : $tType)).
thf(stp_inj_ty_2Eieee_2Eccode,type,(inj__ty_2Eieee_2Eccode : (tp__ty_2Eieee_2Eccode > $i))).
thf(stp_surj_ty_2Eieee_2Eccode,type,(surj__ty_2Eieee_2Eccode : ($i > tp__ty_2Eieee_2Eccode))).
thf(stp_inj_surj_ty_2Eieee_2Eccode,axiom,( ! [X:tp__ty_2Eieee_2Eccode] : ((surj__ty_2Eieee_2Eccode @ (inj__ty_2Eieee_2Eccode @ X)) = X))).
thf(stp_inj_mem_ty_2Eieee_2Eccode,axiom,( ! [X:tp__ty_2Eieee_2Eccode] : (mem @ (inj__ty_2Eieee_2Eccode @ X) @ ty_2Eieee_2Eccode))).
thf(stp_iso_mem_ty_2Eieee_2Eccode,axiom,( ! [X:$i] : ((mem @ X @ ty_2Eieee_2Eccode) => (X = (inj__ty_2Eieee_2Eccode @ (surj__ty_2Eieee_2Eccode @ X)))))).
thf(tp_c_2Eieee_2EEq,type,(c_2Eieee_2EEq:$i)).
thf(mem_c_2Eieee_2EEq,axiom,(mem@c_2Eieee_2EEq@ty_2Eieee_2Eccode)).
thf(stp_fo_c_2Eieee_2EEq,type,(fo__c_2Eieee_2EEq:tp__ty_2Eieee_2Eccode)).
thf(stp_eq_fo_c_2Eieee_2EEq,axiom,((inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EEq) = c_2Eieee_2EEq)).
thf(stp_ty_2Eieee_2Efloat,type,(tp__ty_2Eieee_2Efloat : $tType)).
thf(stp_inj_ty_2Eieee_2Efloat,type,(inj__ty_2Eieee_2Efloat : (tp__ty_2Eieee_2Efloat > $i))).
thf(stp_surj_ty_2Eieee_2Efloat,type,(surj__ty_2Eieee_2Efloat : ($i > tp__ty_2Eieee_2Efloat))).
thf(stp_inj_surj_ty_2Eieee_2Efloat,axiom,( ! [X:tp__ty_2Eieee_2Efloat] : ((surj__ty_2Eieee_2Efloat @ (inj__ty_2Eieee_2Efloat @ X)) = X))).
thf(stp_inj_mem_ty_2Eieee_2Efloat,axiom,( ! [X:tp__ty_2Eieee_2Efloat] : (mem @ (inj__ty_2Eieee_2Efloat @ X) @ ty_2Eieee_2Efloat))).
thf(stp_iso_mem_ty_2Eieee_2Efloat,axiom,( ! [X:$i] : ((mem @ X @ ty_2Eieee_2Efloat) => (X = (inj__ty_2Eieee_2Efloat @ (surj__ty_2Eieee_2Efloat @ X)))))).
thf(tp_c_2Eieee_2EExponent,type,(c_2Eieee_2EExponent:$i)).
thf(mem_c_2Eieee_2EExponent,axiom,(mem@c_2Eieee_2EExponent@(arr@ty_2Eieee_2Efloat@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2EExponent,type,(fo__c_2Eieee_2EExponent:(tp__ty_2Eieee_2Efloat > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2EExponent,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2EExponent @ X0)) = (ap @ c_2Eieee_2EExponent @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2EFinite,type,(c_2Eieee_2EFinite:$i)).
thf(mem_c_2Eieee_2EFinite,axiom,(mem@c_2Eieee_2EFinite@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2EFloat,type,(c_2Eieee_2EFloat:$i)).
thf(mem_c_2Eieee_2EFloat,axiom,(mem@c_2Eieee_2EFloat@(arr@ty_2Erealax_2Ereal@ty_2Eieee_2Efloat))).
thf(stp_fo_c_2Eieee_2EFloat,type,(fo__c_2Eieee_2EFloat:(tp__ty_2Erealax_2Ereal > tp__ty_2Eieee_2Efloat))).
thf(stp_eq_fo_c_2Eieee_2EFloat,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ((inj__ty_2Eieee_2Efloat @ (fo__c_2Eieee_2EFloat @ X0)) = (ap @ c_2Eieee_2EFloat @ (inj__ty_2Erealax_2Ereal @ X0))))).
thf(tp_c_2Eieee_2EFraction,type,(c_2Eieee_2EFraction:$i)).
thf(mem_c_2Eieee_2EFraction,axiom,(mem@c_2Eieee_2EFraction@(arr@ty_2Eieee_2Efloat@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2EFraction,type,(fo__c_2Eieee_2EFraction:(tp__ty_2Eieee_2Efloat > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2EFraction,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2EFraction @ X0)) = (ap @ c_2Eieee_2EFraction @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2EGt,type,(c_2Eieee_2EGt:$i)).
thf(mem_c_2Eieee_2EGt,axiom,(mem@c_2Eieee_2EGt@ty_2Eieee_2Eccode)).
thf(stp_fo_c_2Eieee_2EGt,type,(fo__c_2Eieee_2EGt:tp__ty_2Eieee_2Eccode)).
thf(stp_eq_fo_c_2Eieee_2EGt,axiom,((inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EGt) = c_2Eieee_2EGt)).
thf(tp_c_2Eieee_2EInfinity,type,(c_2Eieee_2EInfinity:$i)).
thf(mem_c_2Eieee_2EInfinity,axiom,(mem@c_2Eieee_2EInfinity@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2EIsdenormal,type,(c_2Eieee_2EIsdenormal:$i)).
thf(mem_c_2Eieee_2EIsdenormal,axiom,(mem@c_2Eieee_2EIsdenormal@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2EIsintegral,type,(c_2Eieee_2EIsintegral:$i)).
thf(mem_c_2Eieee_2EIsintegral,axiom,(mem@c_2Eieee_2EIsintegral@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2EIsnan,type,(c_2Eieee_2EIsnan:$i)).
thf(mem_c_2Eieee_2EIsnan,axiom,(mem@c_2Eieee_2EIsnan@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2EIsnormal,type,(c_2Eieee_2EIsnormal:$i)).
thf(mem_c_2Eieee_2EIsnormal,axiom,(mem@c_2Eieee_2EIsnormal@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2EIszero,type,(c_2Eieee_2EIszero:$i)).
thf(mem_c_2Eieee_2EIszero,axiom,(mem@c_2Eieee_2EIszero@(arr@ty_2Eieee_2Efloat@bool))).
thf(tp_c_2Eieee_2ELt,type,(c_2Eieee_2ELt:$i)).
thf(mem_c_2Eieee_2ELt,axiom,(mem@c_2Eieee_2ELt@ty_2Eieee_2Eccode)).
thf(stp_fo_c_2Eieee_2ELt,type,(fo__c_2Eieee_2ELt:tp__ty_2Eieee_2Eccode)).
thf(stp_eq_fo_c_2Eieee_2ELt,axiom,((inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2ELt) = c_2Eieee_2ELt)).
thf(tp_c_2Eieee_2EMinus__infinity,type,(c_2Eieee_2EMinus__infinity:$i)).
thf(mem_c_2Eieee_2EMinus__infinity,axiom,(mem@c_2Eieee_2EMinus__infinity@ty_2Eieee_2Efloat)).
thf(stp_fo_c_2Eieee_2EMinus__infinity,type,(fo__c_2Eieee_2EMinus__infinity:tp__ty_2Eieee_2Efloat)).
thf(stp_eq_fo_c_2Eieee_2EMinus__infinity,axiom,((inj__ty_2Eieee_2Efloat @ fo__c_2Eieee_2EMinus__infinity) = c_2Eieee_2EMinus__infinity)).
thf(tp_c_2Eieee_2EMinus__zero,type,(c_2Eieee_2EMinus__zero:$i)).
thf(mem_c_2Eieee_2EMinus__zero,axiom,(mem@c_2Eieee_2EMinus__zero@ty_2Eieee_2Efloat)).
thf(stp_fo_c_2Eieee_2EMinus__zero,type,(fo__c_2Eieee_2EMinus__zero:tp__ty_2Eieee_2Efloat)).
thf(stp_eq_fo_c_2Eieee_2EMinus__zero,axiom,((inj__ty_2Eieee_2Efloat @ fo__c_2Eieee_2EMinus__zero) = c_2Eieee_2EMinus__zero)).
thf(tp_c_2Eieee_2EPlus__infinity,type,(c_2Eieee_2EPlus__infinity:$i)).
thf(mem_c_2Eieee_2EPlus__infinity,axiom,(mem@c_2Eieee_2EPlus__infinity@ty_2Eieee_2Efloat)).
thf(stp_fo_c_2Eieee_2EPlus__infinity,type,(fo__c_2Eieee_2EPlus__infinity:tp__ty_2Eieee_2Efloat)).
thf(stp_eq_fo_c_2Eieee_2EPlus__infinity,axiom,((inj__ty_2Eieee_2Efloat @ fo__c_2Eieee_2EPlus__infinity) = c_2Eieee_2EPlus__infinity)).
thf(tp_c_2Eieee_2EPlus__zero,type,(c_2Eieee_2EPlus__zero:$i)).
thf(mem_c_2Eieee_2EPlus__zero,axiom,(mem@c_2Eieee_2EPlus__zero@ty_2Eieee_2Efloat)).
thf(stp_fo_c_2Eieee_2EPlus__zero,type,(fo__c_2Eieee_2EPlus__zero:tp__ty_2Eieee_2Efloat)).
thf(stp_eq_fo_c_2Eieee_2EPlus__zero,axiom,((inj__ty_2Eieee_2Efloat @ fo__c_2Eieee_2EPlus__zero) = c_2Eieee_2EPlus__zero)).
thf(tp_c_2Eieee_2EROUNDFLOAT,type,(c_2Eieee_2EROUNDFLOAT:$i)).
thf(mem_c_2Eieee_2EROUNDFLOAT,axiom,(mem@c_2Eieee_2EROUNDFLOAT@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat))).
thf(stp_fo_c_2Eieee_2EROUNDFLOAT,type,(fo__c_2Eieee_2EROUNDFLOAT:(tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat))).
thf(stp_eq_fo_c_2Eieee_2EROUNDFLOAT,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ (fo__c_2Eieee_2EROUNDFLOAT @ X0)) = (ap @ c_2Eieee_2EROUNDFLOAT @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2ESign,type,(c_2Eieee_2ESign:$i)).
thf(mem_c_2Eieee_2ESign,axiom,(mem@c_2Eieee_2ESign@(arr@ty_2Eieee_2Efloat@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2ESign,type,(fo__c_2Eieee_2ESign:(tp__ty_2Eieee_2Efloat > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2ESign,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2ESign @ X0)) = (ap @ c_2Eieee_2ESign @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(stp_ty_2Eieee_2Eroundmode,type,(tp__ty_2Eieee_2Eroundmode : $tType)).
thf(stp_inj_ty_2Eieee_2Eroundmode,type,(inj__ty_2Eieee_2Eroundmode : (tp__ty_2Eieee_2Eroundmode > $i))).
thf(stp_surj_ty_2Eieee_2Eroundmode,type,(surj__ty_2Eieee_2Eroundmode : ($i > tp__ty_2Eieee_2Eroundmode))).
thf(stp_inj_surj_ty_2Eieee_2Eroundmode,axiom,( ! [X:tp__ty_2Eieee_2Eroundmode] : ((surj__ty_2Eieee_2Eroundmode @ (inj__ty_2Eieee_2Eroundmode @ X)) = X))).
thf(stp_inj_mem_ty_2Eieee_2Eroundmode,axiom,( ! [X:tp__ty_2Eieee_2Eroundmode] : (mem @ (inj__ty_2Eieee_2Eroundmode @ X) @ ty_2Eieee_2Eroundmode))).
thf(stp_iso_mem_ty_2Eieee_2Eroundmode,axiom,( ! [X:$i] : ((mem @ X @ ty_2Eieee_2Eroundmode) => (X = (inj__ty_2Eieee_2Eroundmode @ (surj__ty_2Eieee_2Eroundmode @ X)))))).
thf(tp_c_2Eieee_2ETo__nearest,type,(c_2Eieee_2ETo__nearest:$i)).
thf(mem_c_2Eieee_2ETo__nearest,axiom,(mem@c_2Eieee_2ETo__nearest@ty_2Eieee_2Eroundmode)).
thf(stp_fo_c_2Eieee_2ETo__nearest,type,(fo__c_2Eieee_2ETo__nearest:tp__ty_2Eieee_2Eroundmode)).
thf(stp_eq_fo_c_2Eieee_2ETo__nearest,axiom,((inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest) = c_2Eieee_2ETo__nearest)).
thf(tp_c_2Eieee_2ETo__ninfinity,type,(c_2Eieee_2ETo__ninfinity:$i)).
thf(mem_c_2Eieee_2ETo__ninfinity,axiom,(mem@c_2Eieee_2ETo__ninfinity@ty_2Eieee_2Eroundmode)).
thf(stp_fo_c_2Eieee_2ETo__ninfinity,type,(fo__c_2Eieee_2ETo__ninfinity:tp__ty_2Eieee_2Eroundmode)).
thf(stp_eq_fo_c_2Eieee_2ETo__ninfinity,axiom,((inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity) = c_2Eieee_2ETo__ninfinity)).
thf(tp_c_2Eieee_2ETo__pinfinity,type,(c_2Eieee_2ETo__pinfinity:$i)).
thf(mem_c_2Eieee_2ETo__pinfinity,axiom,(mem@c_2Eieee_2ETo__pinfinity@ty_2Eieee_2Eroundmode)).
thf(stp_fo_c_2Eieee_2ETo__pinfinity,type,(fo__c_2Eieee_2ETo__pinfinity:tp__ty_2Eieee_2Eroundmode)).
thf(stp_eq_fo_c_2Eieee_2ETo__pinfinity,axiom,((inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity) = c_2Eieee_2ETo__pinfinity)).
thf(tp_c_2Eieee_2EUlp,type,(c_2Eieee_2EUlp:$i)).
thf(mem_c_2Eieee_2EUlp,axiom,(mem@c_2Eieee_2EUlp@(arr@ty_2Eieee_2Efloat@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Eieee_2EUlp,type,(fo__c_2Eieee_2EUlp:(tp__ty_2Eieee_2Efloat > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Eieee_2EUlp,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Eieee_2EUlp @ X0)) = (ap @ c_2Eieee_2EUlp @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2EUn,type,(c_2Eieee_2EUn:$i)).
thf(mem_c_2Eieee_2EUn,axiom,(mem@c_2Eieee_2EUn@ty_2Eieee_2Eccode)).
thf(stp_fo_c_2Eieee_2EUn,type,(fo__c_2Eieee_2EUn:tp__ty_2Eieee_2Eccode)).
thf(stp_eq_fo_c_2Eieee_2EUn,axiom,((inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EUn) = c_2Eieee_2EUn)).
thf(tp_c_2Eieee_2EVal,type,(c_2Eieee_2EVal:$i)).
thf(mem_c_2Eieee_2EVal,axiom,(mem@c_2Eieee_2EVal@(arr@ty_2Eieee_2Efloat@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Eieee_2EVal,type,(fo__c_2Eieee_2EVal:(tp__ty_2Eieee_2Efloat > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Eieee_2EVal,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Eieee_2EVal @ X0)) = (ap @ c_2Eieee_2EVal @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2Ebias,type,(c_2Eieee_2Ebias:$i)).
thf(mem_c_2Eieee_2Ebias,axiom,(mem@c_2Eieee_2Ebias@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Ebias,type,(fo__c_2Eieee_2Ebias:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Ebias,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Ebias @ X0)) = (ap @ c_2Eieee_2Ebias @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Ebottomfloat,type,(c_2Eieee_2Ebottomfloat:$i)).
thf(mem_c_2Eieee_2Ebottomfloat,axiom,(mem@c_2Eieee_2Ebottomfloat@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Eccode2num,type,(c_2Eieee_2Eccode2num:$i)).
thf(mem_c_2Eieee_2Eccode2num,axiom,(mem@c_2Eieee_2Eccode2num@(arr@ty_2Eieee_2Eccode@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eccode2num,type,(fo__c_2Eieee_2Eccode2num:(tp__ty_2Eieee_2Eccode > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eccode2num,axiom,( ! [X0:tp__ty_2Eieee_2Eccode] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eccode2num @ X0)) = (ap @ c_2Eieee_2Eccode2num @ (inj__ty_2Eieee_2Eccode @ X0))))).
thf(tp_c_2Eieee_2Eccode__CASE,type,(c_2Eieee_2Eccode__CASE:(del>$i))).
thf(mem_c_2Eieee_2Eccode__CASE,axiom,( ! [A_27a:del] : (mem@(c_2Eieee_2Eccode__CASE@A_27a)@(arr@ty_2Eieee_2Eccode@(arr@A_27a@(arr@A_27a@(arr@A_27a@(arr@A_27a@A_27a)))))))).
thf(tp_c_2Eieee_2Eccode__size,type,(c_2Eieee_2Eccode__size:$i)).
thf(mem_c_2Eieee_2Eccode__size,axiom,(mem@c_2Eieee_2Eccode__size@(arr@ty_2Eieee_2Eccode@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eccode__size,type,(fo__c_2Eieee_2Eccode__size:(tp__ty_2Eieee_2Eccode > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eccode__size,axiom,( ! [X0:tp__ty_2Eieee_2Eccode] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eccode__size @ X0)) = (ap @ c_2Eieee_2Eccode__size @ (inj__ty_2Eieee_2Eccode @ X0))))).
thf(tp_c_2Eieee_2Eclosest,type,(c_2Eieee_2Eclosest:(del>$i))).
thf(mem_c_2Eieee_2Eclosest,axiom,( ! [A_27a:del] : (mem@(c_2Eieee_2Eclosest@A_27a)@(arr@(arr@A_27a@ty_2Erealax_2Ereal)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@ty_2Erealax_2Ereal@A_27a))))))).
thf(tp_c_2Eieee_2Edefloat,type,(c_2Eieee_2Edefloat:$i)).
thf(mem_c_2Eieee_2Edefloat,axiom,(mem@c_2Eieee_2Edefloat@(arr@ty_2Eieee_2Efloat@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Eemax,type,(c_2Eieee_2Eemax:$i)).
thf(mem_c_2Eieee_2Eemax,axiom,(mem@c_2Eieee_2Eemax@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eemax,type,(fo__c_2Eieee_2Eemax:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eemax,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eemax @ X0)) = (ap @ c_2Eieee_2Eemax @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Eencoding,type,(c_2Eieee_2Eencoding:$i)).
thf(mem_c_2Eieee_2Eencoding,axiom,(mem@c_2Eieee_2Eencoding@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Eieee_2Eencoding,type,(fo__c_2Eieee_2Eencoding:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Eieee_2Eencoding,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Eieee_2Eencoding @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Eencoding @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Eieee_2Eexponent,type,(c_2Eieee_2Eexponent:$i)).
thf(mem_c_2Eieee_2Eexponent,axiom,(mem@c_2Eieee_2Eexponent@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eexponent,type,(fo__c_2Eieee_2Eexponent:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eexponent,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eexponent @ X0)) = (ap @ c_2Eieee_2Eexponent @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Eexpwidth,type,(c_2Eieee_2Eexpwidth:$i)).
thf(mem_c_2Eieee_2Eexpwidth,axiom,(mem@c_2Eieee_2Eexpwidth@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eexpwidth,type,(fo__c_2Eieee_2Eexpwidth:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eexpwidth,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eexpwidth @ X0)) = (ap @ c_2Eieee_2Eexpwidth @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Efadd,type,(c_2Eieee_2Efadd:$i)).
thf(mem_c_2Eieee_2Efadd,axiom,(mem@c_2Eieee_2Efadd@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))))))).
thf(tp_c_2Eieee_2Efcompare,type,(c_2Eieee_2Efcompare:$i)).
thf(mem_c_2Eieee_2Efcompare,axiom,(mem@c_2Eieee_2Efcompare@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Eieee_2Eccode))))).
thf(stp_fo_c_2Eieee_2Efcompare,type,(fo__c_2Eieee_2Efcompare:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Eieee_2Eccode))))).
thf(stp_eq_fo_c_2Eieee_2Efcompare,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Eieee_2Eccode @ (((fo__c_2Eieee_2Efcompare @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2Eieee_2Efcompare @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X1)) @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X2))))))).
thf(tp_c_2Eieee_2Efdiv,type,(c_2Eieee_2Efdiv:$i)).
thf(mem_c_2Eieee_2Efdiv,axiom,(mem@c_2Eieee_2Efdiv@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))))))).
thf(tp_c_2Eieee_2Efeq,type,(c_2Eieee_2Efeq:$i)).
thf(mem_c_2Eieee_2Efeq,axiom,(mem@c_2Eieee_2Efeq@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool))))).
thf(tp_c_2Eieee_2Efge,type,(c_2Eieee_2Efge:$i)).
thf(mem_c_2Eieee_2Efge,axiom,(mem@c_2Eieee_2Efge@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool))))).
thf(tp_c_2Eieee_2Efgt,type,(c_2Eieee_2Efgt:$i)).
thf(mem_c_2Eieee_2Efgt,axiom,(mem@c_2Eieee_2Efgt@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool))))).
thf(tp_c_2Eieee_2Efintrnd,type,(c_2Eieee_2Efintrnd:$i)).
thf(mem_c_2Eieee_2Efintrnd,axiom,(mem@c_2Eieee_2Efintrnd@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))))).
thf(tp_c_2Eieee_2Efle,type,(c_2Eieee_2Efle:$i)).
thf(mem_c_2Eieee_2Efle,axiom,(mem@c_2Eieee_2Efle@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool))))).
thf(tp_c_2Eieee_2Efloat,type,(c_2Eieee_2Efloat:$i)).
thf(mem_c_2Eieee_2Efloat,axiom,(mem@c_2Eieee_2Efloat@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Eieee_2Efloat))).
thf(stp_fo_c_2Eieee_2Efloat,type,(fo__c_2Eieee_2Efloat:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Eieee_2Efloat))).
thf(stp_eq_fo_c_2Eieee_2Efloat,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Eieee_2Efloat @ (fo__c_2Eieee_2Efloat @ X0)) = (ap @ c_2Eieee_2Efloat @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Efloat__To__zero,type,(c_2Eieee_2Efloat__To__zero:$i)).
thf(mem_c_2Eieee_2Efloat__To__zero,axiom,(mem@c_2Eieee_2Efloat__To__zero@ty_2Eieee_2Eroundmode)).
thf(stp_fo_c_2Eieee_2Efloat__To__zero,type,(fo__c_2Eieee_2Efloat__To__zero:tp__ty_2Eieee_2Eroundmode)).
thf(stp_eq_fo_c_2Eieee_2Efloat__To__zero,axiom,((inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero) = c_2Eieee_2Efloat__To__zero)).
thf(tp_c_2Eieee_2Efloat__abs,type,(c_2Eieee_2Efloat__abs:$i)).
thf(mem_c_2Eieee_2Efloat__abs,axiom,(mem@c_2Eieee_2Efloat__abs@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat))).
thf(stp_fo_c_2Eieee_2Efloat__abs,type,(fo__c_2Eieee_2Efloat__abs:(tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat))).
thf(stp_eq_fo_c_2Eieee_2Efloat__abs,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ (fo__c_2Eieee_2Efloat__abs @ X0)) = (ap @ c_2Eieee_2Efloat__abs @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2Efloat__add,type,(c_2Eieee_2Efloat__add:$i)).
thf(mem_c_2Eieee_2Efloat__add,axiom,(mem@c_2Eieee_2Efloat__add@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat)))).
thf(stp_fo_c_2Eieee_2Efloat__add,type,(fo__c_2Eieee_2Efloat__add:(tp__ty_2Eieee_2Efloat > (tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat)))).
thf(stp_eq_fo_c_2Eieee_2Efloat__add,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ ((fo__c_2Eieee_2Efloat__add @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Efloat__add @ (inj__ty_2Eieee_2Efloat @ X0)) @ (inj__ty_2Eieee_2Efloat @ X1)))))).
thf(tp_c_2Eieee_2Efloat__div,type,(c_2Eieee_2Efloat__div:$i)).
thf(mem_c_2Eieee_2Efloat__div,axiom,(mem@c_2Eieee_2Efloat__div@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat)))).
thf(stp_fo_c_2Eieee_2Efloat__div,type,(fo__c_2Eieee_2Efloat__div:(tp__ty_2Eieee_2Efloat > (tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat)))).
thf(stp_eq_fo_c_2Eieee_2Efloat__div,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ ((fo__c_2Eieee_2Efloat__div @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Efloat__div @ (inj__ty_2Eieee_2Efloat @ X0)) @ (inj__ty_2Eieee_2Efloat @ X1)))))).
thf(tp_c_2Eieee_2Efloat__eq,type,(c_2Eieee_2Efloat__eq:$i)).
thf(mem_c_2Eieee_2Efloat__eq,axiom,(mem@c_2Eieee_2Efloat__eq@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@bool)))).
thf(tp_c_2Eieee_2Efloat__format,type,(c_2Eieee_2Efloat__format:$i)).
thf(mem_c_2Eieee_2Efloat__format,axiom,(mem@c_2Eieee_2Efloat__format@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(tp_c_2Eieee_2Efloat__ge,type,(c_2Eieee_2Efloat__ge:$i)).
thf(mem_c_2Eieee_2Efloat__ge,axiom,(mem@c_2Eieee_2Efloat__ge@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@bool)))).
thf(tp_c_2Eieee_2Efloat__gt,type,(c_2Eieee_2Efloat__gt:$i)).
thf(mem_c_2Eieee_2Efloat__gt,axiom,(mem@c_2Eieee_2Efloat__gt@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@bool)))).
thf(tp_c_2Eieee_2Efloat__le,type,(c_2Eieee_2Efloat__le:$i)).
thf(mem_c_2Eieee_2Efloat__le,axiom,(mem@c_2Eieee_2Efloat__le@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@bool)))).
thf(tp_c_2Eieee_2Efloat__lt,type,(c_2Eieee_2Efloat__lt:$i)).
thf(mem_c_2Eieee_2Efloat__lt,axiom,(mem@c_2Eieee_2Efloat__lt@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@bool)))).
thf(tp_c_2Eieee_2Efloat__mul,type,(c_2Eieee_2Efloat__mul:$i)).
thf(mem_c_2Eieee_2Efloat__mul,axiom,(mem@c_2Eieee_2Efloat__mul@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat)))).
thf(stp_fo_c_2Eieee_2Efloat__mul,type,(fo__c_2Eieee_2Efloat__mul:(tp__ty_2Eieee_2Efloat > (tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat)))).
thf(stp_eq_fo_c_2Eieee_2Efloat__mul,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ ((fo__c_2Eieee_2Efloat__mul @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Efloat__mul @ (inj__ty_2Eieee_2Efloat @ X0)) @ (inj__ty_2Eieee_2Efloat @ X1)))))).
thf(tp_c_2Eieee_2Efloat__neg,type,(c_2Eieee_2Efloat__neg:$i)).
thf(mem_c_2Eieee_2Efloat__neg,axiom,(mem@c_2Eieee_2Efloat__neg@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat))).
thf(stp_fo_c_2Eieee_2Efloat__neg,type,(fo__c_2Eieee_2Efloat__neg:(tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat))).
thf(stp_eq_fo_c_2Eieee_2Efloat__neg,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ (fo__c_2Eieee_2Efloat__neg @ X0)) = (ap @ c_2Eieee_2Efloat__neg @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2Efloat__rem,type,(c_2Eieee_2Efloat__rem:$i)).
thf(mem_c_2Eieee_2Efloat__rem,axiom,(mem@c_2Eieee_2Efloat__rem@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat)))).
thf(stp_fo_c_2Eieee_2Efloat__rem,type,(fo__c_2Eieee_2Efloat__rem:(tp__ty_2Eieee_2Efloat > (tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat)))).
thf(stp_eq_fo_c_2Eieee_2Efloat__rem,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ ((fo__c_2Eieee_2Efloat__rem @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Efloat__rem @ (inj__ty_2Eieee_2Efloat @ X0)) @ (inj__ty_2Eieee_2Efloat @ X1)))))).
thf(tp_c_2Eieee_2Efloat__sqrt,type,(c_2Eieee_2Efloat__sqrt:$i)).
thf(mem_c_2Eieee_2Efloat__sqrt,axiom,(mem@c_2Eieee_2Efloat__sqrt@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat))).
thf(stp_fo_c_2Eieee_2Efloat__sqrt,type,(fo__c_2Eieee_2Efloat__sqrt:(tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat))).
thf(stp_eq_fo_c_2Eieee_2Efloat__sqrt,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ (fo__c_2Eieee_2Efloat__sqrt @ X0)) = (ap @ c_2Eieee_2Efloat__sqrt @ (inj__ty_2Eieee_2Efloat @ X0))))).
thf(tp_c_2Eieee_2Efloat__sub,type,(c_2Eieee_2Efloat__sub:$i)).
thf(mem_c_2Eieee_2Efloat__sub,axiom,(mem@c_2Eieee_2Efloat__sub@(arr@ty_2Eieee_2Efloat@(arr@ty_2Eieee_2Efloat@ty_2Eieee_2Efloat)))).
thf(stp_fo_c_2Eieee_2Efloat__sub,type,(fo__c_2Eieee_2Efloat__sub:(tp__ty_2Eieee_2Efloat > (tp__ty_2Eieee_2Efloat > tp__ty_2Eieee_2Efloat)))).
thf(stp_eq_fo_c_2Eieee_2Efloat__sub,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : ((inj__ty_2Eieee_2Efloat @ ((fo__c_2Eieee_2Efloat__sub @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Efloat__sub @ (inj__ty_2Eieee_2Efloat @ X0)) @ (inj__ty_2Eieee_2Efloat @ X1)))))).
thf(tp_c_2Eieee_2Eflt,type,(c_2Eieee_2Eflt:$i)).
thf(mem_c_2Eieee_2Eflt,axiom,(mem@c_2Eieee_2Eflt@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool))))).
thf(tp_c_2Eieee_2Efmul,type,(c_2Eieee_2Efmul:$i)).
thf(mem_c_2Eieee_2Efmul,axiom,(mem@c_2Eieee_2Efmul@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))))))).
thf(tp_c_2Eieee_2Efneg,type,(c_2Eieee_2Efneg:$i)).
thf(mem_c_2Eieee_2Efneg,axiom,(mem@c_2Eieee_2Efneg@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))))).
thf(tp_c_2Eieee_2Efraction,type,(c_2Eieee_2Efraction:$i)).
thf(mem_c_2Eieee_2Efraction,axiom,(mem@c_2Eieee_2Efraction@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Efraction,type,(fo__c_2Eieee_2Efraction:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Efraction,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Efraction @ X0)) = (ap @ c_2Eieee_2Efraction @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Efracwidth,type,(c_2Eieee_2Efracwidth:$i)).
thf(mem_c_2Eieee_2Efracwidth,axiom,(mem@c_2Eieee_2Efracwidth@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Efracwidth,type,(fo__c_2Eieee_2Efracwidth:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Efracwidth,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Efracwidth @ X0)) = (ap @ c_2Eieee_2Efracwidth @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Efrem,type,(c_2Eieee_2Efrem:$i)).
thf(mem_c_2Eieee_2Efrem,axiom,(mem@c_2Eieee_2Efrem@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))))))).
thf(tp_c_2Eieee_2Efsqrt,type,(c_2Eieee_2Efsqrt:$i)).
thf(mem_c_2Eieee_2Efsqrt,axiom,(mem@c_2Eieee_2Efsqrt@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))))).
thf(tp_c_2Eieee_2Efsub,type,(c_2Eieee_2Efsub:$i)).
thf(mem_c_2Eieee_2Efsub,axiom,(mem@c_2Eieee_2Efsub@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))))))).
thf(tp_c_2Eieee_2Eintround,type,(c_2Eieee_2Eintround:$i)).
thf(mem_c_2Eieee_2Eintround,axiom,(mem@c_2Eieee_2Eintround@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@ty_2Erealax_2Ereal@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))))).
thf(tp_c_2Eieee_2Eis__closest,type,(c_2Eieee_2Eis__closest:(del>$i))).
thf(mem_c_2Eieee_2Eis__closest,axiom,( ! [A_27a:del] : (mem@(c_2Eieee_2Eis__closest@A_27a)@(arr@(arr@A_27a@ty_2Erealax_2Ereal)@(arr@(arr@A_27a@bool)@(arr@ty_2Erealax_2Ereal@(arr@A_27a@bool))))))).
thf(tp_c_2Eieee_2Eis__denormal,type,(c_2Eieee_2Eis__denormal:$i)).
thf(mem_c_2Eieee_2Eis__denormal,axiom,(mem@c_2Eieee_2Eis__denormal@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__double,type,(c_2Eieee_2Eis__double:$i)).
thf(mem_c_2Eieee_2Eis__double,axiom,(mem@c_2Eieee_2Eis__double@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool))).
thf(tp_c_2Eieee_2Eis__double__extended,type,(c_2Eieee_2Eis__double__extended:$i)).
thf(mem_c_2Eieee_2Eis__double__extended,axiom,(mem@c_2Eieee_2Eis__double__extended@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool))).
thf(tp_c_2Eieee_2Eis__finite,type,(c_2Eieee_2Eis__finite:$i)).
thf(mem_c_2Eieee_2Eis__finite,axiom,(mem@c_2Eieee_2Eis__finite@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__infinity,type,(c_2Eieee_2Eis__infinity:$i)).
thf(mem_c_2Eieee_2Eis__infinity,axiom,(mem@c_2Eieee_2Eis__infinity@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__integral,type,(c_2Eieee_2Eis__integral:$i)).
thf(mem_c_2Eieee_2Eis__integral,axiom,(mem@c_2Eieee_2Eis__integral@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__nan,type,(c_2Eieee_2Eis__nan:$i)).
thf(mem_c_2Eieee_2Eis__nan,axiom,(mem@c_2Eieee_2Eis__nan@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__normal,type,(c_2Eieee_2Eis__normal:$i)).
thf(mem_c_2Eieee_2Eis__normal,axiom,(mem@c_2Eieee_2Eis__normal@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__single,type,(c_2Eieee_2Eis__single:$i)).
thf(mem_c_2Eieee_2Eis__single,axiom,(mem@c_2Eieee_2Eis__single@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool))).
thf(tp_c_2Eieee_2Eis__single__extended,type,(c_2Eieee_2Eis__single__extended:$i)).
thf(mem_c_2Eieee_2Eis__single__extended,axiom,(mem@c_2Eieee_2Eis__single__extended@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool))).
thf(tp_c_2Eieee_2Eis__valid,type,(c_2Eieee_2Eis__valid:$i)).
thf(mem_c_2Eieee_2Eis__valid,axiom,(mem@c_2Eieee_2Eis__valid@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Eis__zero,type,(c_2Eieee_2Eis__zero:$i)).
thf(mem_c_2Eieee_2Eis__zero,axiom,(mem@c_2Eieee_2Eis__zero@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)))).
thf(tp_c_2Eieee_2Elargest,type,(c_2Eieee_2Elargest:$i)).
thf(mem_c_2Eieee_2Elargest,axiom,(mem@c_2Eieee_2Elargest@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Eieee_2Elargest,type,(fo__c_2Eieee_2Elargest:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Eieee_2Elargest,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Eieee_2Elargest @ X0)) = (ap @ c_2Eieee_2Elargest @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Eminus,type,(c_2Eieee_2Eminus:$i)).
thf(mem_c_2Eieee_2Eminus,axiom,(mem@c_2Eieee_2Eminus@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))))).
thf(tp_c_2Eieee_2Eminus__infinity,type,(c_2Eieee_2Eminus__infinity:$i)).
thf(mem_c_2Eieee_2Eminus__infinity,axiom,(mem@c_2Eieee_2Eminus__infinity@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Eminus__zero,type,(c_2Eieee_2Eminus__zero:$i)).
thf(mem_c_2Eieee_2Eminus__zero,axiom,(mem@c_2Eieee_2Eminus__zero@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Enum2ccode,type,(c_2Eieee_2Enum2ccode:$i)).
thf(mem_c_2Eieee_2Enum2ccode,axiom,(mem@c_2Eieee_2Enum2ccode@(arr@ty_2Enum_2Enum@ty_2Eieee_2Eccode))).
thf(stp_fo_c_2Eieee_2Enum2ccode,type,(fo__c_2Eieee_2Enum2ccode:(tp__ty_2Enum_2Enum > tp__ty_2Eieee_2Eccode))).
thf(stp_eq_fo_c_2Eieee_2Enum2ccode,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Eieee_2Eccode @ (fo__c_2Eieee_2Enum2ccode @ X0)) = (ap @ c_2Eieee_2Enum2ccode @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Enum2roundmode,type,(c_2Eieee_2Enum2roundmode:$i)).
thf(mem_c_2Eieee_2Enum2roundmode,axiom,(mem@c_2Eieee_2Enum2roundmode@(arr@ty_2Enum_2Enum@ty_2Eieee_2Eroundmode))).
thf(stp_fo_c_2Eieee_2Enum2roundmode,type,(fo__c_2Eieee_2Enum2roundmode:(tp__ty_2Enum_2Enum > tp__ty_2Eieee_2Eroundmode))).
thf(stp_eq_fo_c_2Eieee_2Enum2roundmode,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Eieee_2Eroundmode @ (fo__c_2Eieee_2Enum2roundmode @ X0)) = (ap @ c_2Eieee_2Enum2roundmode @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Eplus__infinity,type,(c_2Eieee_2Eplus__infinity:$i)).
thf(mem_c_2Eieee_2Eplus__infinity,axiom,(mem@c_2Eieee_2Eplus__infinity@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Eplus__zero,type,(c_2Eieee_2Eplus__zero:$i)).
thf(mem_c_2Eieee_2Eplus__zero,axiom,(mem@c_2Eieee_2Eplus__zero@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Erem,type,(c_2Eieee_2Erem:$i)).
thf(mem_c_2Eieee_2Erem,axiom,(mem@c_2Eieee_2Erem@(arr@ty_2Erealax_2Ereal@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Eieee_2Erem,type,(fo__c_2Eieee_2Erem:(tp__ty_2Erealax_2Ereal > (tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal)))).
thf(stp_eq_fo_c_2Eieee_2Erem,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ ((fo__c_2Eieee_2Erem @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Erem @ (inj__ty_2Erealax_2Ereal @ X0)) @ (inj__ty_2Erealax_2Ereal @ X1)))))).
thf(tp_c_2Eieee_2Eround,type,(c_2Eieee_2Eround:$i)).
thf(mem_c_2Eieee_2Eround,axiom,(mem@c_2Eieee_2Eround@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Eieee_2Eroundmode@(arr@ty_2Erealax_2Ereal@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))))).
thf(tp_c_2Eieee_2Eroundmode2num,type,(c_2Eieee_2Eroundmode2num:$i)).
thf(mem_c_2Eieee_2Eroundmode2num,axiom,(mem@c_2Eieee_2Eroundmode2num@(arr@ty_2Eieee_2Eroundmode@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eroundmode2num,type,(fo__c_2Eieee_2Eroundmode2num:(tp__ty_2Eieee_2Eroundmode > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eroundmode2num,axiom,( ! [X0:tp__ty_2Eieee_2Eroundmode] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eroundmode2num @ X0)) = (ap @ c_2Eieee_2Eroundmode2num @ (inj__ty_2Eieee_2Eroundmode @ X0))))).
thf(tp_c_2Eieee_2Eroundmode__CASE,type,(c_2Eieee_2Eroundmode__CASE:(del>$i))).
thf(mem_c_2Eieee_2Eroundmode__CASE,axiom,( ! [A_27a:del] : (mem@(c_2Eieee_2Eroundmode__CASE@A_27a)@(arr@ty_2Eieee_2Eroundmode@(arr@A_27a@(arr@A_27a@(arr@A_27a@(arr@A_27a@A_27a)))))))).
thf(tp_c_2Eieee_2Eroundmode__size,type,(c_2Eieee_2Eroundmode__size:$i)).
thf(mem_c_2Eieee_2Eroundmode__size,axiom,(mem@c_2Eieee_2Eroundmode__size@(arr@ty_2Eieee_2Eroundmode@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Eroundmode__size,type,(fo__c_2Eieee_2Eroundmode__size:(tp__ty_2Eieee_2Eroundmode > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Eroundmode__size,axiom,( ! [X0:tp__ty_2Eieee_2Eroundmode] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Eroundmode__size @ X0)) = (ap @ c_2Eieee_2Eroundmode__size @ (inj__ty_2Eieee_2Eroundmode @ X0))))).
thf(tp_c_2Eieee_2Esign,type,(c_2Eieee_2Esign:$i)).
thf(mem_c_2Eieee_2Esign,axiom,(mem@c_2Eieee_2Esign@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Esign,type,(fo__c_2Eieee_2Esign:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Esign,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Esign @ X0)) = (ap @ c_2Eieee_2Esign @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Esome__nan,type,(c_2Eieee_2Esome__nan:$i)).
thf(mem_c_2Eieee_2Esome__nan,axiom,(mem@c_2Eieee_2Esome__nan@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Ethreshold,type,(c_2Eieee_2Ethreshold:$i)).
thf(mem_c_2Eieee_2Ethreshold,axiom,(mem@c_2Eieee_2Ethreshold@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Eieee_2Ethreshold,type,(fo__c_2Eieee_2Ethreshold:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Eieee_2Ethreshold,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Eieee_2Ethreshold @ X0)) = (ap @ c_2Eieee_2Ethreshold @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Etopfloat,type,(c_2Eieee_2Etopfloat:$i)).
thf(mem_c_2Eieee_2Etopfloat,axiom,(mem@c_2Eieee_2Etopfloat@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Eieee_2Eulp,type,(c_2Eieee_2Eulp:$i)).
thf(mem_c_2Eieee_2Eulp,axiom,(mem@c_2Eieee_2Eulp@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Eieee_2Eulp,type,(fo__c_2Eieee_2Eulp:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Erealax_2Ereal)))).
thf(stp_eq_fo_c_2Eieee_2Eulp,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Erealax_2Ereal @ ((fo__c_2Eieee_2Eulp @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Eulp @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Eieee_2Evalof,type,(c_2Eieee_2Evalof:$i)).
thf(mem_c_2Eieee_2Evalof,axiom,(mem@c_2Eieee_2Evalof@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Eieee_2Evalof,type,(fo__c_2Eieee_2Evalof:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Erealax_2Ereal)))).
thf(stp_eq_fo_c_2Eieee_2Evalof,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Erealax_2Ereal @ ((fo__c_2Eieee_2Evalof @ X0) @ X1)) = (ap @ (ap @ c_2Eieee_2Evalof @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Eieee_2Ewordlength,type,(c_2Eieee_2Ewordlength:$i)).
thf(mem_c_2Eieee_2Ewordlength,axiom,(mem@c_2Eieee_2Ewordlength@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eieee_2Ewordlength,type,(fo__c_2Eieee_2Ewordlength:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eieee_2Ewordlength,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eieee_2Ewordlength @ X0)) = (ap @ c_2Eieee_2Ewordlength @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Eieee_2Ezerosign,type,(c_2Eieee_2Ezerosign:$i)).
thf(mem_c_2Eieee_2Ezerosign,axiom,(mem@c_2Eieee_2Ezerosign@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))))).
thf(ax_thm_2Eieee_2Eexpwidth,axiom,( ! [V0ew:tp__ty_2Enum_2Enum] : ( ! [V1fw:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexpwidth@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0ew))@(inj__ty_2Enum_2Enum @ V1fw)))) = V0ew)))).
thf(ax_thm_2Eieee_2Efracwidth,axiom,( ! [V0ew:tp__ty_2Enum_2Enum] : ( ! [V1fw:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Efracwidth@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0ew))@(inj__ty_2Enum_2Enum @ V1fw)))) = V1fw)))).
thf(ax_thm_2Eieee_2Ewordlength,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Ewordlength@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(ax_thm_2Eieee_2Eemax,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(ax_thm_2Eieee_2Ebias,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Ebias@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(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(ax_thm_2Eieee_2Eis__single,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@c_2Eieee_2Eis__single@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) <=> (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Ewordlength@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (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@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))).
thf(ax_thm_2Eieee_2Eis__double,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@c_2Eieee_2Eis__double@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) <=> (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (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))))))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Ewordlength@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (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(ax_thm_2Eieee_2Eis__single__extended,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@c_2Eieee_2Eis__single__extended@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@c_2Eieee_2Ewordlength@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))).
thf(ax_thm_2Eieee_2Eis__double__extended,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@c_2Eieee_2Eis__double__extended@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@c_2Eieee_2Ewordlength@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))).
thf(ax_thm_2Eieee_2Esign,axiom,( ! [V0s:tp__ty_2Enum_2Enum] : ( ! [V1e:tp__ty_2Enum_2Enum] : ( ! [V2f:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Esign@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V0s))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1e))@(inj__ty_2Enum_2Enum @ V2f))))) = V0s))))).
thf(ax_thm_2Eieee_2Eexponent,axiom,( ! [V0s:tp__ty_2Enum_2Enum] : ( ! [V1e:tp__ty_2Enum_2Enum] : ( ! [V2f:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexponent@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V0s))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1e))@(inj__ty_2Enum_2Enum @ V2f))))) = V1e))))).
thf(ax_thm_2Eieee_2Efraction,axiom,( ! [V0s:tp__ty_2Enum_2Enum] : ( ! [V1e:tp__ty_2Enum_2Enum] : ( ! [V2f:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Efraction@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V0s))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1e))@(inj__ty_2Enum_2Enum @ V2f))))) = V2f))))).
thf(ax_thm_2Eieee_2Eis__nan,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))) & (~ ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Efraction@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = fo__c_2Enum_2E0))))))).
thf(ax_thm_2Eieee_2Eis__infinity,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Efraction@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = fo__c_2Enum_2E0)))))).
thf(ax_thm_2Eieee_2Eis__normal,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__normal@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))))).
thf(ax_thm_2Eieee_2Eis__denormal,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__denormal@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = fo__c_2Enum_2E0) & (~ ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Efraction@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = fo__c_2Enum_2E0))))))).
thf(ax_thm_2Eieee_2Eis__zero,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Efraction@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = fo__c_2Enum_2E0)))))).
thf(ax_thm_2Eieee_2Eis__valid,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1s:tp__ty_2Enum_2Enum] : ( ! [V2e:tp__ty_2Enum_2Enum] : ( ! [V3f:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__valid@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V1s))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2e))@(inj__ty_2Enum_2Enum @ V3f))))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1s))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2e))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Eexpwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3f))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))))))))).
thf(ax_thm_2Eieee_2Eis__finite,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__finite@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> ((p@(ap@(ap@c_2Eieee_2Eis__valid@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) & ((p@(ap@(ap@c_2Eieee_2Eis__normal@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) | ((p@(ap@(ap@c_2Eieee_2Eis__denormal@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) | (p@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))))))))).
thf(ax_thm_2Eieee_2Eplus__infinity,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(ax_thm_2Eieee_2Eminus__infinity,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(ax_thm_2Eieee_2Eplus__zero,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Eplus__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(ax_thm_2Eieee_2Eminus__zero,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Eminus__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(ax_thm_2Eieee_2Etopfloat,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Etopfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(ax_thm_2Eieee_2Ebottomfloat,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Ebottomfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(ax_thm_2Eieee_2Eminus,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@c_2Eieee_2Eminus@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))@(ap@c_2Eieee_2Efraction@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))))))))).
thf(ax_thm_2Eieee_2Eencoding,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1s:tp__ty_2Enum_2Enum] : ( ! [V2e:tp__ty_2Enum_2Enum] : ( ! [V3f:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Eieee_2Eencoding@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V1s))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2e))@(inj__ty_2Enum_2Enum @ V3f))))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V1s))@(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_2Eieee_2Ewordlength@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V2e))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))@(inj__ty_2Enum_2Enum @ V3f))))))))).
thf(ax_thm_2Eieee_2Evalof,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1s:tp__ty_2Enum_2Enum] : ( ! [V2e:tp__ty_2Enum_2Enum] : ( ! [V3f:tp__ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V1s))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2e))@(inj__ty_2Enum_2Enum @ V3f))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2e))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(inj__ty_2Enum_2Enum @ V1s)))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Ebias@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V3f)))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(inj__ty_2Enum_2Enum @ V1s)))@(ap@(ap@c_2Ereal_2E_2F@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Enum_2Enum @ V2e)))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Ebias@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V3f)))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))))))))))))).
thf(ax_thm_2Eieee_2Elargest,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2E_2F@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Ebias@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))))@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Erealax_2Einv@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))))))))).
thf(ax_thm_2Eieee_2Ethreshold,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Eieee_2Ethreshold@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2E_2F@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Eieee_2Eemax@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Ebias@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))))@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Erealax_2Einv@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Enum_2ESUC@(ap@c_2Eieee_2Efracwidth@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))))))))).
thf(ax_thm_2Eieee_2Eulp,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Eieee_2Eulp@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(ax_thm_2Eieee_2Eroundmode__TY__DEF,axiom,(? [V0rep:$i] : ((mem@V0rep@(arr@ty_2Eieee_2Eroundmode@ty_2Enum_2Enum)) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@ty_2Enum_2Enum@ty_2Eieee_2Eroundmode)@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Eprim__rec_2E_3C@V1n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@V0rep))))).
thf(ax_thm_2Eieee_2Eroundmode__BIJ,axiom,(( ! [V0a:tp__ty_2Eieee_2Eroundmode] : ((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V0a)))) = V0a)) & ( ! [V1r:tp__ty_2Enum_2Enum] : ((p@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Eprim__rec_2E_3C@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(inj__ty_2Enum_2Enum @ V1r))) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(ap@c_2Eieee_2Enum2roundmode@(inj__ty_2Enum_2Enum @ V1r)))) = V1r))))).
thf(conj_thm_2Eieee_2Enum2roundmode__roundmode2num,lemma,( ! [V0a:tp__ty_2Eieee_2Eroundmode] : ((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V0a)))) = V0a))).
thf(conj_thm_2Eieee_2Eroundmode2num__num2roundmode,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(ap@c_2Eieee_2Enum2roundmode@(inj__ty_2Enum_2Enum @ V0r)))) = V0r)))).
thf(conj_thm_2Eieee_2Enum2roundmode__11,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ( ! [V1r_27:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1r_27))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(inj__ty_2Enum_2Enum @ V0r))) = (surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(inj__ty_2Enum_2Enum @ V1r_27)))) <=> (V0r = V1r_27))))))).
thf(conj_thm_2Eieee_2Eroundmode2num__11,lemma,( ! [V0a:tp__ty_2Eieee_2Eroundmode] : ( ! [V1a_27:tp__ty_2Eieee_2Eroundmode] : (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V0a))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V1a_27)))) <=> (V0a = V1a_27))))).
thf(conj_thm_2Eieee_2Enum2roundmode__ONTO,lemma,( ! [V0a:tp__ty_2Eieee_2Eroundmode] : (? [V1r:tp__ty_2Enum_2Enum] : ((V0a = (surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(inj__ty_2Enum_2Enum @ V1r)))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Eieee_2Eroundmode2num__ONTO,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (? [V1a:tp__ty_2Eieee_2Eroundmode] : (V0r = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V1a)))))))).
thf(conj_thm_2Eieee_2Enum2roundmode__thm,lemma,(((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Eieee_2ETo__nearest) & (((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = fo__c_2Eieee_2Efloat__To__zero) & (((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = fo__c_2Eieee_2ETo__pinfinity) & ((surj__ty_2Eieee_2Eroundmode @ (ap@c_2Eieee_2Enum2roundmode@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = fo__c_2Eieee_2ETo__ninfinity))))).
thf(conj_thm_2Eieee_2Eroundmode2num__thm,lemma,(((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest))) = fo__c_2Enum_2E0) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Eieee_2Eroundmode__EQ__roundmode,lemma,( ! [V0a:tp__ty_2Eieee_2Eroundmode] : ( ! [V1a_27:tp__ty_2Eieee_2Eroundmode] : ((V0a = V1a_27) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V0a))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V1a_27)))))))).
thf(ax_thm_2Eieee_2Eroundmode__size__def,axiom,( ! [V0x:tp__ty_2Eieee_2Eroundmode] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eroundmode__size@(inj__ty_2Eieee_2Eroundmode @ V0x))) = fo__c_2Enum_2E0))).
thf(ax_thm_2Eieee_2Eroundmode__CASE,axiom,( ! [A_27a:del]: ( ! [V0x:tp__ty_2Eieee_2Eroundmode] : ( ! [V1v0:$i] : ((mem@V1v0@A_27a) => ( ! [V2v1:$i] : ((mem@V2v1@A_27a) => ( ! [V3v2:$i] : ((mem@V3v2@A_27a) => ( ! [V4v3:$i] : ((mem@V4v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ V0x))@V1v0)@V2v1)@V3v2)@V4v3) = (ap@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@c_2Eprim__rec_2E_3C@V5m)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V1v0)@(ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@c_2Eprim__rec_2E_3C@V5m)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V2v1)@(ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V5m)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V3v2)@V4v3)))))@(ap@c_2Eieee_2Eroundmode2num@(inj__ty_2Eieee_2Eroundmode @ V0x))))))))))))))).
thf(conj_thm_2Eieee_2Eroundmode__case__def,lemma,( ! [A_27a:del]: (( ! [V0v0:$i] : ((mem@V0v0@A_27a) => ( ! [V1v1:$i] : ((mem@V1v1@A_27a) => ( ! [V2v2:$i] : ((mem@V2v2@A_27a) => ( ! [V3v3:$i] : ((mem@V3v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest))@V0v0)@V1v1)@V2v2)@V3v3) = V0v0))))))))) & (( ! [V4v0:$i] : ((mem@V4v0@A_27a) => ( ! [V5v1:$i] : ((mem@V5v1@A_27a) => ( ! [V6v2:$i] : ((mem@V6v2@A_27a) => ( ! [V7v3:$i] : ((mem@V7v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero))@V4v0)@V5v1)@V6v2)@V7v3) = V5v1))))))))) & (( ! [V8v0:$i] : ((mem@V8v0@A_27a) => ( ! [V9v1:$i] : ((mem@V9v1@A_27a) => ( ! [V10v2:$i] : ((mem@V10v2@A_27a) => ( ! [V11v3:$i] : ((mem@V11v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity))@V8v0)@V9v1)@V10v2)@V11v3) = V10v2))))))))) & ( ! [V12v0:$i] : ((mem@V12v0@A_27a) => ( ! [V13v1:$i] : ((mem@V13v1@A_27a) => ( ! [V14v2:$i] : ((mem@V14v2@A_27a) => ( ! [V15v3:$i] : ((mem@V15v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity))@V12v0)@V13v1)@V14v2)@V15v3) = V15v3)))))))))))))).
thf(conj_thm_2Eieee_2Edatatype__roundmode,lemma,( ! [V0roundmode:$i] : ((mem@V0roundmode@(arr@ty_2Eieee_2Eroundmode@(arr@ty_2Eieee_2Eroundmode@(arr@ty_2Eieee_2Eroundmode@(arr@ty_2Eieee_2Eroundmode@bool))))) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@(ap@(ap@V0roundmode@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity))))))).
thf(conj_thm_2Eieee_2Eroundmode__distinct,lemma,((~~ (fo__c_2Eieee_2ETo__nearest = fo__c_2Eieee_2Efloat__To__zero)) & ((~~ (fo__c_2Eieee_2ETo__nearest = fo__c_2Eieee_2ETo__pinfinity)) & ((~~ (fo__c_2Eieee_2ETo__nearest = fo__c_2Eieee_2ETo__ninfinity)) & ((~~ (fo__c_2Eieee_2Efloat__To__zero = fo__c_2Eieee_2ETo__pinfinity)) & ((~~ (fo__c_2Eieee_2Efloat__To__zero = fo__c_2Eieee_2ETo__ninfinity)) & (~~ (fo__c_2Eieee_2ETo__pinfinity = fo__c_2Eieee_2ETo__ninfinity)))))))).
thf(conj_thm_2Eieee_2Eroundmode__nchotomy,lemma,( ! [V0a:tp__ty_2Eieee_2Eroundmode] : ((V0a = fo__c_2Eieee_2ETo__nearest) | ((V0a = fo__c_2Eieee_2Efloat__To__zero) | ((V0a = fo__c_2Eieee_2ETo__pinfinity) | (V0a = fo__c_2Eieee_2ETo__ninfinity)))))).
thf(conj_thm_2Eieee_2Eroundmode__Axiom,lemma,( ! [A_27a:del]: ( ! [V0x0:$i] : ((mem@V0x0@A_27a) => ( ! [V1x1:$i] : ((mem@V1x1@A_27a) => ( ! [V2x2:$i] : ((mem@V2x2@A_27a) => ( ! [V3x3:$i] : ((mem@V3x3@A_27a) => (? [V4f:$i] : ((mem@V4f@(arr@ty_2Eieee_2Eroundmode@A_27a)) & (((ap@V4f@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest)) = V0x0) & (((ap@V4f@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero)) = V1x1) & (((ap@V4f@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity)) = V2x2) & ((ap@V4f@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity)) = V3x3)))))))))))))))).
thf(conj_thm_2Eieee_2Eroundmode__induction,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Eieee_2Eroundmode@bool)) => (((p@(ap@V0P@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest))) & ((p@(ap@V0P@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity))) & ((p@(ap@V0P@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity))) & (p@(ap@V0P@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero)))))) => ( ! [V1a:tp__ty_2Eieee_2Eroundmode] : (p@(ap@V0P@(inj__ty_2Eieee_2Eroundmode @ V1a)))))))).
thf(conj_thm_2Eieee_2Eroundmode__case__cong,lemma,( ! [A_27a:del]: ( ! [V0v0_27:$i] : ((mem@V0v0_27@A_27a) => ( ! [V1v1_27:$i] : ((mem@V1v1_27@A_27a) => ( ! [V2v2_27:$i] : ((mem@V2v2_27@A_27a) => ( ! [V3v3_27:$i] : ((mem@V3v3_27@A_27a) => ( ! [V4M:tp__ty_2Eieee_2Eroundmode] : ( ! [V5M_27:tp__ty_2Eieee_2Eroundmode] : ( ! [V6v0:$i] : ((mem@V6v0@A_27a) => ( ! [V7v1:$i] : ((mem@V7v1@A_27a) => ( ! [V8v2:$i] : ((mem@V8v2@A_27a) => ( ! [V9v3:$i] : ((mem@V9v3@A_27a) => (((V4M = V5M_27) & (((V5M_27 = fo__c_2Eieee_2ETo__nearest) => (V6v0 = V0v0_27)) & (((V5M_27 = fo__c_2Eieee_2Efloat__To__zero) => (V7v1 = V1v1_27)) & (((V5M_27 = fo__c_2Eieee_2ETo__pinfinity) => (V8v2 = V2v2_27)) & ((V5M_27 = fo__c_2Eieee_2ETo__ninfinity) => (V9v3 = V3v3_27)))))) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ V4M))@V6v0)@V7v1)@V8v2)@V9v3) = (ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ V5M_27))@V0v0_27)@V1v1_27)@V2v2_27)@V3v3_27))))))))))))))))))))))).
thf(conj_thm_2Eieee_2Eroundmode__case__eq,lemma,( ! [A_27a:del]: ( ! [V0x:tp__ty_2Eieee_2Eroundmode] : ( ! [V1v0:$i] : ((mem@V1v0@A_27a) => ( ! [V2v1:$i] : ((mem@V2v1@A_27a) => ( ! [V3v2:$i] : ((mem@V3v2@A_27a) => ( ! [V4v3:$i] : ((mem@V4v3@A_27a) => ( ! [V5v:$i] : ((mem@V5v@A_27a) => (((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eroundmode__CASE@A_27a)@(inj__ty_2Eieee_2Eroundmode @ V0x))@V1v0)@V2v1)@V3v2)@V4v3) = V5v) <=> (((V0x = fo__c_2Eieee_2ETo__nearest) & (V1v0 = V5v)) | (((V0x = fo__c_2Eieee_2Efloat__To__zero) & (V2v1 = V5v)) | (((V0x = fo__c_2Eieee_2ETo__pinfinity) & (V3v2 = V5v)) | ((V0x = fo__c_2Eieee_2ETo__ninfinity) & (V4v3 = V5v))))))))))))))))))).
thf(ax_thm_2Eieee_2Eis__closest,axiom,( ! [A_27a:del]: ( ! [V0v:$i] : ((mem@V0v@(arr@A_27a@ty_2Erealax_2Ereal)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3a:$i] : ((mem@V3a@A_27a) => ((p@(ap@(ap@(ap@(ap@(c_2Eieee_2Eis__closest@A_27a)@V0v)@V1s)@(inj__ty_2Erealax_2Ereal @ V2x))@V3a)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3a)@V1s)) & ( ! [V4b:$i] : ((mem@V4b@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4b)@V1s)) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0v@V3a))@(inj__ty_2Erealax_2Ereal @ V2x))))@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0v@V4b))@(inj__ty_2Erealax_2Ereal @ V2x))))))))))))))))))).
thf(ax_thm_2Eieee_2Eclosest,axiom,( ! [A_27a:del]: ( ! [V0v:$i] : ((mem@V0v@(arr@A_27a@ty_2Erealax_2Ereal)) => ( ! [V1p:$i] : ((mem@V1p@(arr@A_27a@bool)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3x:tp__ty_2Erealax_2Ereal] : ((ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@A_27a)@V0v)@V1p)@V2s)@(inj__ty_2Erealax_2Ereal @ V3x)) = (ap@(c_2Emin_2E_40@A_27a)@(lam@A_27a@(^ [V4a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@(ap@(c_2Eieee_2Eis__closest@A_27a)@V0v)@V2s)@(inj__ty_2Erealax_2Ereal @ V3x))@V4a))@(ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V5b:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@(ap@(c_2Eieee_2Eis__closest@A_27a)@V0v)@V2s)@(inj__ty_2Erealax_2Ereal @ V3x))@V5b))@(ap@V1p@V5b))))))@(ap@V1p@V4a)))))))))))))))).
thf(ax_thm_2Eieee_2Eround__def,axiom,(( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest))@(inj__ty_2Erealax_2Ereal @ V1x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Ethreshold@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))))@(ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__ge@(inj__ty_2Erealax_2Ereal @ V1x))@(ap@c_2Eieee_2Ethreshold@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V2a:$i] : (ap@c_2Earithmetic_2EEVEN@(ap@c_2Eieee_2Efraction@V2a)))))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V3a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V3a)@(ap@(ap@c_2Eieee_2Eis__finite@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@V3a))))))@(inj__ty_2Erealax_2Ereal @ V1x)))))))) & (( ! [V4X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V5x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero))@(inj__ty_2Erealax_2Ereal @ V5x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V5x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X)))))@(ap@c_2Eieee_2Ebottomfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__gt@(inj__ty_2Erealax_2Ereal @ V5x))@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X))))@(ap@c_2Eieee_2Etopfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V6x:$i] : c_2Ebool_2ET)))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V7a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V7a)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__finite@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X))@V7a))@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V4X))@V7a)))@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V5x)))))))))@(inj__ty_2Erealax_2Ereal @ V5x)))))))) & (( ! [V8X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V9x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity))@(inj__ty_2Erealax_2Ereal @ V9x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V9x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X)))))@(ap@c_2Eieee_2Ebottomfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__gt@(inj__ty_2Erealax_2Ereal @ V9x))@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X))))@(ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V10x:$i] : c_2Ebool_2ET)))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V11a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V11a)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__finite@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X))@V11a))@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V8X))@V11a))@(inj__ty_2Erealax_2Ereal @ V9x))))))))@(inj__ty_2Erealax_2Ereal @ V9x)))))))) & ( ! [V12X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V13x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity))@(inj__ty_2Erealax_2Ereal @ V13x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V13x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X)))))@(ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__gt@(inj__ty_2Erealax_2Ereal @ V13x))@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X))))@(ap@c_2Eieee_2Etopfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V14x:$i] : c_2Ebool_2ET)))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V15a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V15a)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__finite@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X))@V15a))@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V12X))@V15a))@(inj__ty_2Erealax_2Ereal @ V13x))))))))@(inj__ty_2Erealax_2Ereal @ V13x)))))))))))).
thf(ax_thm_2Eieee_2Eis__integral,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eieee_2Eis__integral@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) <=> ((p@(ap@(ap@c_2Eieee_2Eis__finite@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a))) & (? [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Eabs@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V1a)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V2n)))))))))).
thf(ax_thm_2Eieee_2Eintround__def,axiom,(( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eintround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__nearest))@(inj__ty_2Erealax_2Ereal @ V1x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Ethreshold@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))))@(ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__ge@(inj__ty_2Erealax_2Ereal @ V1x))@(ap@c_2Eieee_2Ethreshold@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V2a:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Earithmetic_2EEVEN@V3n))@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@V2a)))@(ap@c_2Ereal_2Ereal__of__num@V3n)))))))))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V4a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V4a)@(ap@(ap@c_2Eieee_2Eis__integral@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@V4a))))))@(inj__ty_2Erealax_2Ereal @ V1x)))))))) & (( ! [V5X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V6x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eintround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2Efloat__To__zero))@(inj__ty_2Erealax_2Ereal @ V6x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V6x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X)))))@(ap@c_2Eieee_2Ebottomfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__gt@(inj__ty_2Erealax_2Ereal @ V6x))@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X))))@(ap@c_2Eieee_2Etopfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V7x:$i] : c_2Ebool_2ET)))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V8a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V8a)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__integral@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X))@V8a))@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V5X))@V8a)))@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V6x)))))))))@(inj__ty_2Erealax_2Ereal @ V6x)))))))) & (( ! [V9X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V10x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eintround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__pinfinity))@(inj__ty_2Erealax_2Ereal @ V10x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V10x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X)))))@(ap@c_2Eieee_2Ebottomfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__gt@(inj__ty_2Erealax_2Ereal @ V10x))@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X))))@(ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V11x:$i] : c_2Ebool_2ET)))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V12a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V12a)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__integral@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X))@V12a))@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V9X))@V12a))@(inj__ty_2Erealax_2Ereal @ V10x))))))))@(inj__ty_2Erealax_2Ereal @ V10x)))))))) & ( ! [V13X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V14x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Eintround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity))@(inj__ty_2Erealax_2Ereal @ V14x))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V14x))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X)))))@(ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ereal_2Ereal__gt@(inj__ty_2Erealax_2Ereal @ V14x))@(ap@c_2Eieee_2Elargest@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X))))@(ap@c_2Eieee_2Etopfloat@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X)))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V15x:$i] : c_2Ebool_2ET)))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V16a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@bool)@V16a)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__integral@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X))@V16a))@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V13X))@V16a))@(inj__ty_2Erealax_2Ereal @ V14x))))))))@(inj__ty_2Erealax_2Ereal @ V14x)))))))))))).
thf(ax_thm_2Eieee_2Esome__nan,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(c_2Emin_2E_40@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(^ [V1a:$i] : (ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@V1a)))))))).
thf(ax_thm_2Eieee_2Ezerosign,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1s:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Enum_2Enum @ V1s))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1s))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Eieee_2Eplus__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Eieee_2Eminus__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))))))).
thf(ax_thm_2Eieee_2Erem,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Eieee_2Erem@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Ebool_2ELET@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V2n:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@(ap@c_2Erealax_2Ereal__mul@V2n)@(inj__ty_2Erealax_2Ereal @ V1y))))))@(ap@(ap@(ap@(ap@(c_2Eieee_2Eclosest@ty_2Erealax_2Ereal)@(c_2Ecombin_2EI@ty_2Erealax_2Ereal))@(lam@ty_2Erealax_2Ereal@(^ [V3x:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Earithmetic_2EEVEN@V4n))@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Eabs@V3x))@(ap@c_2Ereal_2Ereal__of__num@V4n)))))))))@(ap@(c_2Epred__set_2EGSPEC@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V5x:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@bool)@V5x)@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Eabs@V5x))@(ap@c_2Ereal_2Ereal__of__num@V6n))))))))))@(ap@(ap@c_2Ereal_2E_2F@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y))))))))).
thf(ax_thm_2Eieee_2Efintrnd,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Efintrnd@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(ap@c_2Eieee_2Eintround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))))))))))).
thf(ax_thm_2Eieee_2Efadd,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3b:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@c_2Eieee_2Efadd@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))))))))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Eieee_2Eroundmode)@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))))))))))))).
thf(ax_thm_2Eieee_2Efsub,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3b:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@c_2Eieee_2Efsub@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))))))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@c_2Eieee_2Eminus@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))))))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Eieee_2Eroundmode)@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__ty_2Eieee_2Eroundmode @ fo__c_2Eieee_2ETo__ninfinity)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))))))))))))).
thf(ax_thm_2Eieee_2Efmul,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3b:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@c_2Eieee_2Efmul@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))))))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))))))))))))).
thf(ax_thm_2Eieee_2Efdiv,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3b:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@c_2Eieee_2Efdiv@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))))))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@c_2Eieee_2Eplus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Eieee_2Eminus__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(ap@c_2Eieee_2Eplus__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@c_2Eieee_2Eminus__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@(ap@c_2Ereal_2E_2F@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))))))))))))).
thf(ax_thm_2Eieee_2Efsqrt,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Efsqrt@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@c_2Etransc_2Esqrt@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))))))))))))).
thf(ax_thm_2Eieee_2Efrem,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3b:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(ap@c_2Eieee_2Efrem@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Eis__zero@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b))))))@(ap@c_2Eieee_2Esome__nan@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))@(ap@(ap@c_2Eieee_2Eis__infinity@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))@(ap@(ap@(ap@c_2Eieee_2Ezerosign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@(ap@c_2Eieee_2Eround@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(ap@(ap@c_2Eieee_2Erem@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Eieee_2Evalof@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V3b)))))))))))))).
thf(ax_thm_2Eieee_2Efneg,axiom,( ! [V0X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Eieee_2Eroundmode] : ( ! [V2a:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Eieee_2Efneg@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V0X))@(inj__ty_2Eieee_2Eroundmode @ V1m))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eieee_2Esign@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Eieee_2Eexponent@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))@(ap@c_2Eieee_2Efraction@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ V2a)))))))))).
thf(ax_thm_2Eieee_2Eccode__TY__DEF,axiom,(? [V0rep:$i] : ((mem@V0rep@(arr@ty_2Eieee_2Eccode@ty_2Enum_2Enum)) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@ty_2Enum_2Enum@ty_2Eieee_2Eccode)@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Eprim__rec_2E_3C@V1n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@V0rep))))).
thf(ax_thm_2Eieee_2Eccode__BIJ,axiom,(( ! [V0a:tp__ty_2Eieee_2Eccode] : ((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V0a)))) = V0a)) & ( ! [V1r:tp__ty_2Enum_2Enum] : ((p@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Eprim__rec_2E_3C@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(inj__ty_2Enum_2Enum @ V1r))) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(ap@c_2Eieee_2Enum2ccode@(inj__ty_2Enum_2Enum @ V1r)))) = V1r))))).
thf(conj_thm_2Eieee_2Enum2ccode__ccode2num,lemma,( ! [V0a:tp__ty_2Eieee_2Eccode] : ((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V0a)))) = V0a))).
thf(conj_thm_2Eieee_2Eccode2num__num2ccode,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(ap@c_2Eieee_2Enum2ccode@(inj__ty_2Enum_2Enum @ V0r)))) = V0r)))).
thf(conj_thm_2Eieee_2Enum2ccode__11,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ( ! [V1r_27:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1r_27))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(inj__ty_2Enum_2Enum @ V0r))) = (surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(inj__ty_2Enum_2Enum @ V1r_27)))) <=> (V0r = V1r_27))))))).
thf(conj_thm_2Eieee_2Eccode2num__11,lemma,( ! [V0a:tp__ty_2Eieee_2Eccode] : ( ! [V1a_27:tp__ty_2Eieee_2Eccode] : (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V0a))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V1a_27)))) <=> (V0a = V1a_27))))).
thf(conj_thm_2Eieee_2Enum2ccode__ONTO,lemma,( ! [V0a:tp__ty_2Eieee_2Eccode] : (? [V1r:tp__ty_2Enum_2Enum] : ((V0a = (surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(inj__ty_2Enum_2Enum @ V1r)))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Eieee_2Eccode2num__ONTO,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (? [V1a:tp__ty_2Eieee_2Eccode] : (V0r = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V1a)))))))).
thf(conj_thm_2Eieee_2Enum2ccode__thm,lemma,(((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Eieee_2EGt) & (((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = fo__c_2Eieee_2ELt) & (((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = fo__c_2Eieee_2EEq) & ((surj__ty_2Eieee_2Eccode @ (ap@c_2Eieee_2Enum2ccode@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = fo__c_2Eieee_2EUn))))).
thf(conj_thm_2Eieee_2Eccode2num__thm,lemma,(((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EGt))) = fo__c_2Enum_2E0) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2ELt))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EEq))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EUn))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Eieee_2Eccode__EQ__ccode,lemma,( ! [V0a:tp__ty_2Eieee_2Eccode] : ( ! [V1a_27:tp__ty_2Eieee_2Eccode] : ((V0a = V1a_27) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V0a))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V1a_27)))))))).
thf(ax_thm_2Eieee_2Eccode__size__def,axiom,( ! [V0x:tp__ty_2Eieee_2Eccode] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eieee_2Eccode__size@(inj__ty_2Eieee_2Eccode @ V0x))) = fo__c_2Enum_2E0))).
thf(ax_thm_2Eieee_2Eccode__CASE,axiom,( ! [A_27a:del]: ( ! [V0x:tp__ty_2Eieee_2Eccode] : ( ! [V1v0:$i] : ((mem@V1v0@A_27a) => ( ! [V2v1:$i] : ((mem@V2v1@A_27a) => ( ! [V3v2:$i] : ((mem@V3v2@A_27a) => ( ! [V4v3:$i] : ((mem@V4v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eccode__CASE@A_27a)@(inj__ty_2Eieee_2Eccode @ V0x))@V1v0)@V2v1)@V3v2)@V4v3) = (ap@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@c_2Eprim__rec_2E_3C@V5m)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V1v0)@(ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@c_2Eprim__rec_2E_3C@V5m)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V2v1)@(ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V5m)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V3v2)@V4v3)))))@(ap@c_2Eieee_2Eccode2num@(inj__ty_2Eieee_2Eccode @ V0x))))))))))))))).
thf(conj_thm_2Eieee_2Eccode__case__def,lemma,( ! [A_27a:del]: (( ! [V0v0:$i] : ((mem@V0v0@A_27a) => ( ! [V1v1:$i] : ((mem@V1v1@A_27a) => ( ! [V2v2:$i] : ((mem@V2v2@A_27a) => ( ! [V3v3:$i] : ((mem@V3v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eccode__CASE@A_27a)@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EGt))@V0v0)@V1v1)@V2v2)@V3v3) = V0v0))))))))) & (( ! [V4v0:$i] : ((mem@V4v0@A_27a) => ( ! [V5v1:$i] : ((mem@V5v1@A_27a) => ( ! [V6v2:$i] : ((mem@V6v2@A_27a) => ( ! [V7v3:$i] : ((mem@V7v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eccode__CASE@A_27a)@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2ELt))@V4v0)@V5v1)@V6v2)@V7v3) = V5v1))))))))) & (( ! [V8v0:$i] : ((mem@V8v0@A_27a) => ( ! [V9v1:$i] : ((mem@V9v1@A_27a) => ( ! [V10v2:$i] : ((mem@V10v2@A_27a) => ( ! [V11v3:$i] : ((mem@V11v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eccode__CASE@A_27a)@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EEq))@V8v0)@V9v1)@V10v2)@V11v3) = V10v2))))))))) & ( ! [V12v0:$i] : ((mem@V12v0@A_27a) => ( ! [V13v1:$i] : ((mem@V13v1@A_27a) => ( ! [V14v2:$i] : ((mem@V14v2@A_27a) => ( ! [V15v3:$i] : ((mem@V15v3@A_27a) => ((ap@(ap@(ap@(ap@(ap@(c_2Eieee_2Eccode__CASE@A_27a)@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EUn))@V12v0)@V13v1)@V14v2)@V15v3) = V15v3)))))))))))))).
thf(conj_thm_2Eieee_2Edatatype__ccode,lemma,( ! [V0ccode:$i] : ((mem@V0ccode@(arr@ty_2Eieee_2Eccode@(arr@ty_2Eieee_2Eccode@(arr@ty_2Eieee_2Eccode@(arr@ty_2Eieee_2Eccode@bool))))) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@(ap@(ap@V0ccode@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EGt))@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2ELt))@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EEq))@(inj__ty_2Eieee_2Eccode @ fo__c_2Eieee_2EUn))))))).
thf(conj_thm_2Eieee_2Eccode__distinct,conjecture,((~~ (fo__c_2Eieee_2EGt = fo__c_2Eieee_2ELt)) & ((~~ (fo__c_2Eieee_2EGt = fo__c_2Eieee_2EEq)) & ((~~ (fo__c_2Eieee_2EGt = fo__c_2Eieee_2EUn)) & ((~~ (fo__c_2Eieee_2ELt = fo__c_2Eieee_2EEq)) & ((~~ (fo__c_2Eieee_2ELt = fo__c_2Eieee_2EUn)) & (~~ (fo__c_2Eieee_2EEq = fo__c_2Eieee_2EUn)))))))).
