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,conjecture,( ! [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))))).
