include('Axioms/complex_2.ax').
tff(tp_ty_2Eieee_2Eccode,type,( ty_2Eieee_2Eccode: del )).
tff(tp_ty_2Eieee_2Efloat,type,( ty_2Eieee_2Efloat: del )).
tff(tp_ty_2Eieee_2Eroundmode,type,( ty_2Eieee_2Eroundmode: del )).
tff(stp_ty_2Eieee_2Eccode,type,(tp__ty_2Eieee_2Eccode : $tType)).
tff(stp_inj_ty_2Eieee_2Eccode,type,(inj__ty_2Eieee_2Eccode : tp__ty_2Eieee_2Eccode > $i)).
tff(stp_surj_ty_2Eieee_2Eccode,type,(surj__ty_2Eieee_2Eccode : $i > tp__ty_2Eieee_2Eccode)).
tff(stp_inj_surj_ty_2Eieee_2Eccode,axiom,( ! [X:tp__ty_2Eieee_2Eccode] : (surj__ty_2Eieee_2Eccode(inj__ty_2Eieee_2Eccode(X)) = X))).
tff(stp_inj_mem_ty_2Eieee_2Eccode,axiom,( ! [X:tp__ty_2Eieee_2Eccode] : (mem(inj__ty_2Eieee_2Eccode(X),ty_2Eieee_2Eccode)))).
tff(stp_iso_mem_ty_2Eieee_2Eccode,axiom,( ! [X:$i] : (mem(X,ty_2Eieee_2Eccode) => (X = inj__ty_2Eieee_2Eccode(surj__ty_2Eieee_2Eccode(X)))))).
tff(tp_c_2Eieee_2EEq,type,(c_2Eieee_2EEq:$i)).
tff(mem_c_2Eieee_2EEq,axiom,mem(c_2Eieee_2EEq,ty_2Eieee_2Eccode)).
tff(stp_fo_c_2Eieee_2EEq,type,(fo__c_2Eieee_2EEq:tp__ty_2Eieee_2Eccode)).
tff(stp_eq_fo_c_2Eieee_2EEq,axiom,(inj__ty_2Eieee_2Eccode(fo__c_2Eieee_2EEq) = c_2Eieee_2EEq)).
tff(stp_ty_2Eieee_2Efloat,type,(tp__ty_2Eieee_2Efloat : $tType)).
tff(stp_inj_ty_2Eieee_2Efloat,type,(inj__ty_2Eieee_2Efloat : tp__ty_2Eieee_2Efloat > $i)).
tff(stp_surj_ty_2Eieee_2Efloat,type,(surj__ty_2Eieee_2Efloat : $i > tp__ty_2Eieee_2Efloat)).
tff(stp_inj_surj_ty_2Eieee_2Efloat,axiom,( ! [X:tp__ty_2Eieee_2Efloat] : (surj__ty_2Eieee_2Efloat(inj__ty_2Eieee_2Efloat(X)) = X))).
tff(stp_inj_mem_ty_2Eieee_2Efloat,axiom,( ! [X:tp__ty_2Eieee_2Efloat] : (mem(inj__ty_2Eieee_2Efloat(X),ty_2Eieee_2Efloat)))).
tff(stp_iso_mem_ty_2Eieee_2Efloat,axiom,( ! [X:$i] : (mem(X,ty_2Eieee_2Efloat) => (X = inj__ty_2Eieee_2Efloat(surj__ty_2Eieee_2Efloat(X)))))).
tff(tp_c_2Eieee_2EExponent,type,(c_2Eieee_2EExponent:$i)).
tff(mem_c_2Eieee_2EExponent,axiom,mem(c_2Eieee_2EExponent,arr(ty_2Eieee_2Efloat,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2EExponent,type,(fo__c_2Eieee_2EExponent:(tp__ty_2Eieee_2Efloat) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Eieee_2EFinite,type,(c_2Eieee_2EFinite:$i)).
tff(mem_c_2Eieee_2EFinite,axiom,mem(c_2Eieee_2EFinite,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EFinite,type,(fo__c_2Eieee_2EFinite:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EFinite,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EFinite(X0)) = ap(c_2Eieee_2EFinite,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2EFloat,type,(c_2Eieee_2EFloat:$i)).
tff(mem_c_2Eieee_2EFloat,axiom,mem(c_2Eieee_2EFloat,arr(ty_2Erealax_2Ereal,ty_2Eieee_2Efloat))).
tff(stp_fo_c_2Eieee_2EFloat,type,(fo__c_2Eieee_2EFloat:(tp__ty_2Erealax_2Ereal) > tp__ty_2Eieee_2Efloat)).
tff(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))))).
tff(tp_c_2Eieee_2EFraction,type,(c_2Eieee_2EFraction:$i)).
tff(mem_c_2Eieee_2EFraction,axiom,mem(c_2Eieee_2EFraction,arr(ty_2Eieee_2Efloat,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2EFraction,type,(fo__c_2Eieee_2EFraction:(tp__ty_2Eieee_2Efloat) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Eieee_2EGt,type,(c_2Eieee_2EGt:$i)).
tff(mem_c_2Eieee_2EGt,axiom,mem(c_2Eieee_2EGt,ty_2Eieee_2Eccode)).
tff(stp_fo_c_2Eieee_2EGt,type,(fo__c_2Eieee_2EGt:tp__ty_2Eieee_2Eccode)).
tff(stp_eq_fo_c_2Eieee_2EGt,axiom,(inj__ty_2Eieee_2Eccode(fo__c_2Eieee_2EGt) = c_2Eieee_2EGt)).
tff(tp_c_2Eieee_2EInfinity,type,(c_2Eieee_2EInfinity:$i)).
tff(mem_c_2Eieee_2EInfinity,axiom,mem(c_2Eieee_2EInfinity,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EInfinity,type,(fo__c_2Eieee_2EInfinity:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EInfinity,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EInfinity(X0)) = ap(c_2Eieee_2EInfinity,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2EIsdenormal,type,(c_2Eieee_2EIsdenormal:$i)).
tff(mem_c_2Eieee_2EIsdenormal,axiom,mem(c_2Eieee_2EIsdenormal,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EIsdenormal,type,(fo__c_2Eieee_2EIsdenormal:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EIsdenormal,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EIsdenormal(X0)) = ap(c_2Eieee_2EIsdenormal,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2EIsintegral,type,(c_2Eieee_2EIsintegral:$i)).
tff(mem_c_2Eieee_2EIsintegral,axiom,mem(c_2Eieee_2EIsintegral,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EIsintegral,type,(fo__c_2Eieee_2EIsintegral:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EIsintegral,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EIsintegral(X0)) = ap(c_2Eieee_2EIsintegral,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2EIsnan,type,(c_2Eieee_2EIsnan:$i)).
tff(mem_c_2Eieee_2EIsnan,axiom,mem(c_2Eieee_2EIsnan,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EIsnan,type,(fo__c_2Eieee_2EIsnan:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EIsnan,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EIsnan(X0)) = ap(c_2Eieee_2EIsnan,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2EIsnormal,type,(c_2Eieee_2EIsnormal:$i)).
tff(mem_c_2Eieee_2EIsnormal,axiom,mem(c_2Eieee_2EIsnormal,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EIsnormal,type,(fo__c_2Eieee_2EIsnormal:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EIsnormal,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EIsnormal(X0)) = ap(c_2Eieee_2EIsnormal,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2EIszero,type,(c_2Eieee_2EIszero:$i)).
tff(mem_c_2Eieee_2EIszero,axiom,mem(c_2Eieee_2EIszero,arr(ty_2Eieee_2Efloat,bool))).
tff(stp_fo_c_2Eieee_2EIszero,type,(fo__c_2Eieee_2EIszero:(tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2EIszero,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2EIszero(X0)) = ap(c_2Eieee_2EIszero,inj__ty_2Eieee_2Efloat(X0))))).
tff(tp_c_2Eieee_2ELt,type,(c_2Eieee_2ELt:$i)).
tff(mem_c_2Eieee_2ELt,axiom,mem(c_2Eieee_2ELt,ty_2Eieee_2Eccode)).
tff(stp_fo_c_2Eieee_2ELt,type,(fo__c_2Eieee_2ELt:tp__ty_2Eieee_2Eccode)).
tff(stp_eq_fo_c_2Eieee_2ELt,axiom,(inj__ty_2Eieee_2Eccode(fo__c_2Eieee_2ELt) = c_2Eieee_2ELt)).
tff(tp_c_2Eieee_2EMinus__infinity,type,(c_2Eieee_2EMinus__infinity:$i)).
tff(mem_c_2Eieee_2EMinus__infinity,axiom,mem(c_2Eieee_2EMinus__infinity,ty_2Eieee_2Efloat)).
tff(stp_fo_c_2Eieee_2EMinus__infinity,type,(fo__c_2Eieee_2EMinus__infinity:tp__ty_2Eieee_2Efloat)).
tff(stp_eq_fo_c_2Eieee_2EMinus__infinity,axiom,(inj__ty_2Eieee_2Efloat(fo__c_2Eieee_2EMinus__infinity) = c_2Eieee_2EMinus__infinity)).
tff(tp_c_2Eieee_2EMinus__zero,type,(c_2Eieee_2EMinus__zero:$i)).
tff(mem_c_2Eieee_2EMinus__zero,axiom,mem(c_2Eieee_2EMinus__zero,ty_2Eieee_2Efloat)).
tff(stp_fo_c_2Eieee_2EMinus__zero,type,(fo__c_2Eieee_2EMinus__zero:tp__ty_2Eieee_2Efloat)).
tff(stp_eq_fo_c_2Eieee_2EMinus__zero,axiom,(inj__ty_2Eieee_2Efloat(fo__c_2Eieee_2EMinus__zero) = c_2Eieee_2EMinus__zero)).
tff(tp_c_2Eieee_2EPlus__infinity,type,(c_2Eieee_2EPlus__infinity:$i)).
tff(mem_c_2Eieee_2EPlus__infinity,axiom,mem(c_2Eieee_2EPlus__infinity,ty_2Eieee_2Efloat)).
tff(stp_fo_c_2Eieee_2EPlus__infinity,type,(fo__c_2Eieee_2EPlus__infinity:tp__ty_2Eieee_2Efloat)).
tff(stp_eq_fo_c_2Eieee_2EPlus__infinity,axiom,(inj__ty_2Eieee_2Efloat(fo__c_2Eieee_2EPlus__infinity) = c_2Eieee_2EPlus__infinity)).
tff(tp_c_2Eieee_2EPlus__zero,type,(c_2Eieee_2EPlus__zero:$i)).
tff(mem_c_2Eieee_2EPlus__zero,axiom,mem(c_2Eieee_2EPlus__zero,ty_2Eieee_2Efloat)).
tff(stp_fo_c_2Eieee_2EPlus__zero,type,(fo__c_2Eieee_2EPlus__zero:tp__ty_2Eieee_2Efloat)).
tff(stp_eq_fo_c_2Eieee_2EPlus__zero,axiom,(inj__ty_2Eieee_2Efloat(fo__c_2Eieee_2EPlus__zero) = c_2Eieee_2EPlus__zero)).
tff(tp_c_2Eieee_2EROUNDFLOAT,type,(c_2Eieee_2EROUNDFLOAT:$i)).
tff(mem_c_2Eieee_2EROUNDFLOAT,axiom,mem(c_2Eieee_2EROUNDFLOAT,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))).
tff(stp_fo_c_2Eieee_2EROUNDFLOAT,type,(fo__c_2Eieee_2EROUNDFLOAT:(tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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))))).
tff(tp_c_2Eieee_2ESign,type,(c_2Eieee_2ESign:$i)).
tff(mem_c_2Eieee_2ESign,axiom,mem(c_2Eieee_2ESign,arr(ty_2Eieee_2Efloat,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2ESign,type,(fo__c_2Eieee_2ESign:(tp__ty_2Eieee_2Efloat) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(stp_ty_2Eieee_2Eroundmode,type,(tp__ty_2Eieee_2Eroundmode : $tType)).
tff(stp_inj_ty_2Eieee_2Eroundmode,type,(inj__ty_2Eieee_2Eroundmode : tp__ty_2Eieee_2Eroundmode > $i)).
tff(stp_surj_ty_2Eieee_2Eroundmode,type,(surj__ty_2Eieee_2Eroundmode : $i > tp__ty_2Eieee_2Eroundmode)).
tff(stp_inj_surj_ty_2Eieee_2Eroundmode,axiom,( ! [X:tp__ty_2Eieee_2Eroundmode] : (surj__ty_2Eieee_2Eroundmode(inj__ty_2Eieee_2Eroundmode(X)) = X))).
tff(stp_inj_mem_ty_2Eieee_2Eroundmode,axiom,( ! [X:tp__ty_2Eieee_2Eroundmode] : (mem(inj__ty_2Eieee_2Eroundmode(X),ty_2Eieee_2Eroundmode)))).
tff(stp_iso_mem_ty_2Eieee_2Eroundmode,axiom,( ! [X:$i] : (mem(X,ty_2Eieee_2Eroundmode) => (X = inj__ty_2Eieee_2Eroundmode(surj__ty_2Eieee_2Eroundmode(X)))))).
tff(tp_c_2Eieee_2ETo__nearest,type,(c_2Eieee_2ETo__nearest:$i)).
tff(mem_c_2Eieee_2ETo__nearest,axiom,mem(c_2Eieee_2ETo__nearest,ty_2Eieee_2Eroundmode)).
tff(stp_fo_c_2Eieee_2ETo__nearest,type,(fo__c_2Eieee_2ETo__nearest:tp__ty_2Eieee_2Eroundmode)).
tff(stp_eq_fo_c_2Eieee_2ETo__nearest,axiom,(inj__ty_2Eieee_2Eroundmode(fo__c_2Eieee_2ETo__nearest) = c_2Eieee_2ETo__nearest)).
tff(tp_c_2Eieee_2ETo__ninfinity,type,(c_2Eieee_2ETo__ninfinity:$i)).
tff(mem_c_2Eieee_2ETo__ninfinity,axiom,mem(c_2Eieee_2ETo__ninfinity,ty_2Eieee_2Eroundmode)).
tff(stp_fo_c_2Eieee_2ETo__ninfinity,type,(fo__c_2Eieee_2ETo__ninfinity:tp__ty_2Eieee_2Eroundmode)).
tff(stp_eq_fo_c_2Eieee_2ETo__ninfinity,axiom,(inj__ty_2Eieee_2Eroundmode(fo__c_2Eieee_2ETo__ninfinity) = c_2Eieee_2ETo__ninfinity)).
tff(tp_c_2Eieee_2ETo__pinfinity,type,(c_2Eieee_2ETo__pinfinity:$i)).
tff(mem_c_2Eieee_2ETo__pinfinity,axiom,mem(c_2Eieee_2ETo__pinfinity,ty_2Eieee_2Eroundmode)).
tff(stp_fo_c_2Eieee_2ETo__pinfinity,type,(fo__c_2Eieee_2ETo__pinfinity:tp__ty_2Eieee_2Eroundmode)).
tff(stp_eq_fo_c_2Eieee_2ETo__pinfinity,axiom,(inj__ty_2Eieee_2Eroundmode(fo__c_2Eieee_2ETo__pinfinity) = c_2Eieee_2ETo__pinfinity)).
tff(tp_c_2Eieee_2EUlp,type,(c_2Eieee_2EUlp:$i)).
tff(mem_c_2Eieee_2EUlp,axiom,mem(c_2Eieee_2EUlp,arr(ty_2Eieee_2Efloat,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Eieee_2EUlp,type,(fo__c_2Eieee_2EUlp:(tp__ty_2Eieee_2Efloat) > tp__ty_2Erealax_2Ereal)).
tff(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))))).
tff(tp_c_2Eieee_2EUn,type,(c_2Eieee_2EUn:$i)).
tff(mem_c_2Eieee_2EUn,axiom,mem(c_2Eieee_2EUn,ty_2Eieee_2Eccode)).
tff(stp_fo_c_2Eieee_2EUn,type,(fo__c_2Eieee_2EUn:tp__ty_2Eieee_2Eccode)).
tff(stp_eq_fo_c_2Eieee_2EUn,axiom,(inj__ty_2Eieee_2Eccode(fo__c_2Eieee_2EUn) = c_2Eieee_2EUn)).
tff(tp_c_2Eieee_2EVal,type,(c_2Eieee_2EVal:$i)).
tff(mem_c_2Eieee_2EVal,axiom,mem(c_2Eieee_2EVal,arr(ty_2Eieee_2Efloat,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Eieee_2EVal,type,(fo__c_2Eieee_2EVal:(tp__ty_2Eieee_2Efloat) > tp__ty_2Erealax_2Ereal)).
tff(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))))).
tff(tp_c_2Eieee_2Ebias,type,(c_2Eieee_2Ebias:$i)).
tff(mem_c_2Eieee_2Ebias,axiom,mem(c_2Eieee_2Ebias,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Ebottomfloat,type,(c_2Eieee_2Ebottomfloat:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Eccode2num,type,(c_2Eieee_2Eccode2num:$i)).
tff(mem_c_2Eieee_2Eccode2num,axiom,mem(c_2Eieee_2Eccode2num,arr(ty_2Eieee_2Eccode,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2Eccode2num,type,(fo__c_2Eieee_2Eccode2num:(tp__ty_2Eieee_2Eccode) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Eieee_2Eccode__CASE,type,(c_2Eieee_2Eccode__CASE:del > $i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Eccode__size,type,(c_2Eieee_2Eccode__size:$i)).
tff(mem_c_2Eieee_2Eccode__size,axiom,mem(c_2Eieee_2Eccode__size,arr(ty_2Eieee_2Eccode,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2Eccode__size,type,(fo__c_2Eieee_2Eccode__size:(tp__ty_2Eieee_2Eccode) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Eieee_2Eclosest,type,(c_2Eieee_2Eclosest:del > $i)).
tff(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))))))).
tff(tp_c_2Eieee_2Edefloat,type,(c_2Eieee_2Edefloat:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Eemax,type,(c_2Eieee_2Eemax:$i)).
tff(mem_c_2Eieee_2Eemax,axiom,mem(c_2Eieee_2Eemax,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Eencoding,type,(c_2Eieee_2Eencoding:$i)).
tff(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)))).
tff(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)).
tff(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)))))).
tff(tp_c_2Eieee_2Eexponent,type,(c_2Eieee_2Eexponent:$i)).
tff(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))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Eexpwidth,type,(c_2Eieee_2Eexpwidth:$i)).
tff(mem_c_2Eieee_2Eexpwidth,axiom,mem(c_2Eieee_2Eexpwidth,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Efadd,type,(c_2Eieee_2Efadd:$i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Efcompare,type,(c_2Eieee_2Efcompare:$i)).
tff(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))))).
tff(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)).
tff(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))))))).
tff(tp_c_2Eieee_2Efdiv,type,(c_2Eieee_2Efdiv:$i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Efeq,type,(c_2Eieee_2Efeq:$i)).
tff(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))))).
tff(stp_fo_c_2Eieee_2Efeq,type,(fo__c_2Eieee_2Efeq:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Efeq,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__o(fo__c_2Eieee_2Efeq(X0,X1,X2)) = ap(ap(ap(c_2Eieee_2Efeq,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))))))).
tff(tp_c_2Eieee_2Efge,type,(c_2Eieee_2Efge:$i)).
tff(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))))).
tff(stp_fo_c_2Eieee_2Efge,type,(fo__c_2Eieee_2Efge:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Efge,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__o(fo__c_2Eieee_2Efge(X0,X1,X2)) = ap(ap(ap(c_2Eieee_2Efge,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))))))).
tff(tp_c_2Eieee_2Efgt,type,(c_2Eieee_2Efgt:$i)).
tff(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))))).
tff(stp_fo_c_2Eieee_2Efgt,type,(fo__c_2Eieee_2Efgt:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Efgt,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__o(fo__c_2Eieee_2Efgt(X0,X1,X2)) = ap(ap(ap(c_2Eieee_2Efgt,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))))))).
tff(tp_c_2Eieee_2Efintrnd,type,(c_2Eieee_2Efintrnd:$i)).
tff(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))))))).
tff(tp_c_2Eieee_2Efle,type,(c_2Eieee_2Efle:$i)).
tff(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))))).
tff(stp_fo_c_2Eieee_2Efle,type,(fo__c_2Eieee_2Efle:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Efle,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__o(fo__c_2Eieee_2Efle(X0,X1,X2)) = ap(ap(ap(c_2Eieee_2Efle,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))))))).
tff(tp_c_2Eieee_2Efloat,type,(c_2Eieee_2Efloat:$i)).
tff(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))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Efloat__To__zero,type,(c_2Eieee_2Efloat__To__zero:$i)).
tff(mem_c_2Eieee_2Efloat__To__zero,axiom,mem(c_2Eieee_2Efloat__To__zero,ty_2Eieee_2Eroundmode)).
tff(stp_fo_c_2Eieee_2Efloat__To__zero,type,(fo__c_2Eieee_2Efloat__To__zero:tp__ty_2Eieee_2Eroundmode)).
tff(stp_eq_fo_c_2Eieee_2Efloat__To__zero,axiom,(inj__ty_2Eieee_2Eroundmode(fo__c_2Eieee_2Efloat__To__zero) = c_2Eieee_2Efloat__To__zero)).
tff(tp_c_2Eieee_2Efloat__abs,type,(c_2Eieee_2Efloat__abs:$i)).
tff(mem_c_2Eieee_2Efloat__abs,axiom,mem(c_2Eieee_2Efloat__abs,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))).
tff(stp_fo_c_2Eieee_2Efloat__abs,type,(fo__c_2Eieee_2Efloat__abs:(tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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))))).
tff(tp_c_2Eieee_2Efloat__add,type,(c_2Eieee_2Efloat__add:$i)).
tff(mem_c_2Eieee_2Efloat__add,axiom,mem(c_2Eieee_2Efloat__add,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)))).
tff(stp_fo_c_2Eieee_2Efloat__add,type,(fo__c_2Eieee_2Efloat__add:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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)))))).
tff(tp_c_2Eieee_2Efloat__div,type,(c_2Eieee_2Efloat__div:$i)).
tff(mem_c_2Eieee_2Efloat__div,axiom,mem(c_2Eieee_2Efloat__div,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)))).
tff(stp_fo_c_2Eieee_2Efloat__div,type,(fo__c_2Eieee_2Efloat__div:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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)))))).
tff(tp_c_2Eieee_2Efloat__eq,type,(c_2Eieee_2Efloat__eq:$i)).
tff(mem_c_2Eieee_2Efloat__eq,axiom,mem(c_2Eieee_2Efloat__eq,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool)))).
tff(stp_fo_c_2Eieee_2Efloat__eq,type,(fo__c_2Eieee_2Efloat__eq:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Efloat__eq,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2Efloat__eq(X0,X1)) = ap(ap(c_2Eieee_2Efloat__eq,inj__ty_2Eieee_2Efloat(X0)),inj__ty_2Eieee_2Efloat(X1)))))).
tff(tp_c_2Eieee_2Efloat__format,type,(c_2Eieee_2Efloat__format:$i)).
tff(mem_c_2Eieee_2Efloat__format,axiom,mem(c_2Eieee_2Efloat__format,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(tp_c_2Eieee_2Efloat__ge,type,(c_2Eieee_2Efloat__ge:$i)).
tff(mem_c_2Eieee_2Efloat__ge,axiom,mem(c_2Eieee_2Efloat__ge,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool)))).
tff(stp_fo_c_2Eieee_2Efloat__ge,type,(fo__c_2Eieee_2Efloat__ge:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Efloat__ge,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2Efloat__ge(X0,X1)) = ap(ap(c_2Eieee_2Efloat__ge,inj__ty_2Eieee_2Efloat(X0)),inj__ty_2Eieee_2Efloat(X1)))))).
tff(tp_c_2Eieee_2Efloat__gt,type,(c_2Eieee_2Efloat__gt:$i)).
tff(mem_c_2Eieee_2Efloat__gt,axiom,mem(c_2Eieee_2Efloat__gt,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool)))).
tff(stp_fo_c_2Eieee_2Efloat__gt,type,(fo__c_2Eieee_2Efloat__gt:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Efloat__gt,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2Efloat__gt(X0,X1)) = ap(ap(c_2Eieee_2Efloat__gt,inj__ty_2Eieee_2Efloat(X0)),inj__ty_2Eieee_2Efloat(X1)))))).
tff(tp_c_2Eieee_2Efloat__le,type,(c_2Eieee_2Efloat__le:$i)).
tff(mem_c_2Eieee_2Efloat__le,axiom,mem(c_2Eieee_2Efloat__le,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool)))).
tff(stp_fo_c_2Eieee_2Efloat__le,type,(fo__c_2Eieee_2Efloat__le:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Efloat__le,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2Efloat__le(X0,X1)) = ap(ap(c_2Eieee_2Efloat__le,inj__ty_2Eieee_2Efloat(X0)),inj__ty_2Eieee_2Efloat(X1)))))).
tff(tp_c_2Eieee_2Efloat__lt,type,(c_2Eieee_2Efloat__lt:$i)).
tff(mem_c_2Eieee_2Efloat__lt,axiom,mem(c_2Eieee_2Efloat__lt,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool)))).
tff(stp_fo_c_2Eieee_2Efloat__lt,type,(fo__c_2Eieee_2Efloat__lt:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Efloat__lt,axiom,( ! [X0:tp__ty_2Eieee_2Efloat] : ( ! [X1:tp__ty_2Eieee_2Efloat] : (inj__o(fo__c_2Eieee_2Efloat__lt(X0,X1)) = ap(ap(c_2Eieee_2Efloat__lt,inj__ty_2Eieee_2Efloat(X0)),inj__ty_2Eieee_2Efloat(X1)))))).
tff(tp_c_2Eieee_2Efloat__mul,type,(c_2Eieee_2Efloat__mul:$i)).
tff(mem_c_2Eieee_2Efloat__mul,axiom,mem(c_2Eieee_2Efloat__mul,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)))).
tff(stp_fo_c_2Eieee_2Efloat__mul,type,(fo__c_2Eieee_2Efloat__mul:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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)))))).
tff(tp_c_2Eieee_2Efloat__neg,type,(c_2Eieee_2Efloat__neg:$i)).
tff(mem_c_2Eieee_2Efloat__neg,axiom,mem(c_2Eieee_2Efloat__neg,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))).
tff(stp_fo_c_2Eieee_2Efloat__neg,type,(fo__c_2Eieee_2Efloat__neg:(tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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))))).
tff(tp_c_2Eieee_2Efloat__rem,type,(c_2Eieee_2Efloat__rem:$i)).
tff(mem_c_2Eieee_2Efloat__rem,axiom,mem(c_2Eieee_2Efloat__rem,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)))).
tff(stp_fo_c_2Eieee_2Efloat__rem,type,(fo__c_2Eieee_2Efloat__rem:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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)))))).
tff(tp_c_2Eieee_2Efloat__sqrt,type,(c_2Eieee_2Efloat__sqrt:$i)).
tff(mem_c_2Eieee_2Efloat__sqrt,axiom,mem(c_2Eieee_2Efloat__sqrt,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))).
tff(stp_fo_c_2Eieee_2Efloat__sqrt,type,(fo__c_2Eieee_2Efloat__sqrt:(tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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))))).
tff(tp_c_2Eieee_2Efloat__sub,type,(c_2Eieee_2Efloat__sub:$i)).
tff(mem_c_2Eieee_2Efloat__sub,axiom,mem(c_2Eieee_2Efloat__sub,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)))).
tff(stp_fo_c_2Eieee_2Efloat__sub,type,(fo__c_2Eieee_2Efloat__sub:(tp__ty_2Eieee_2Efloat * tp__ty_2Eieee_2Efloat) > tp__ty_2Eieee_2Efloat)).
tff(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)))))).
tff(tp_c_2Eieee_2Eflt,type,(c_2Eieee_2Eflt:$i)).
tff(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))))).
tff(stp_fo_c_2Eieee_2Eflt,type,(fo__c_2Eieee_2Eflt:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eflt,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__o(fo__c_2Eieee_2Eflt(X0,X1,X2)) = ap(ap(ap(c_2Eieee_2Eflt,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))))))).
tff(tp_c_2Eieee_2Efmul,type,(c_2Eieee_2Efmul:$i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Efneg,type,(c_2Eieee_2Efneg:$i)).
tff(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))))))).
tff(tp_c_2Eieee_2Efraction,type,(c_2Eieee_2Efraction:$i)).
tff(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))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Efracwidth,type,(c_2Eieee_2Efracwidth:$i)).
tff(mem_c_2Eieee_2Efracwidth,axiom,mem(c_2Eieee_2Efracwidth,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Efrem,type,(c_2Eieee_2Efrem:$i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Efsqrt,type,(c_2Eieee_2Efsqrt:$i)).
tff(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))))))).
tff(tp_c_2Eieee_2Efsub,type,(c_2Eieee_2Efsub:$i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Eintround,type,(c_2Eieee_2Eintround:$i)).
tff(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))))))).
tff(tp_c_2Eieee_2Eis__closest,type,(c_2Eieee_2Eis__closest:del > $i)).
tff(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))))))).
tff(tp_c_2Eieee_2Eis__denormal,type,(c_2Eieee_2Eis__denormal:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__denormal,type,(fo__c_2Eieee_2Eis__denormal:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__denormal,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__o(fo__c_2Eieee_2Eis__denormal(X0,X1)) = ap(ap(c_2Eieee_2Eis__denormal,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)))))).
tff(tp_c_2Eieee_2Eis__double,type,(c_2Eieee_2Eis__double:$i)).
tff(mem_c_2Eieee_2Eis__double,axiom,mem(c_2Eieee_2Eis__double,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))).
tff(stp_fo_c_2Eieee_2Eis__double,type,(fo__c_2Eieee_2Eis__double:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__double,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Eieee_2Eis__double(X0)) = ap(c_2Eieee_2Eis__double,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eieee_2Eis__double__extended,type,(c_2Eieee_2Eis__double__extended:$i)).
tff(mem_c_2Eieee_2Eis__double__extended,axiom,mem(c_2Eieee_2Eis__double__extended,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))).
tff(stp_fo_c_2Eieee_2Eis__double__extended,type,(fo__c_2Eieee_2Eis__double__extended:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__double__extended,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Eieee_2Eis__double__extended(X0)) = ap(c_2Eieee_2Eis__double__extended,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eieee_2Eis__finite,type,(c_2Eieee_2Eis__finite:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__finite,type,(fo__c_2Eieee_2Eis__finite:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__finite,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__o(fo__c_2Eieee_2Eis__finite(X0,X1)) = ap(ap(c_2Eieee_2Eis__finite,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)))))).
tff(tp_c_2Eieee_2Eis__infinity,type,(c_2Eieee_2Eis__infinity:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__infinity,type,(fo__c_2Eieee_2Eis__infinity:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__infinity,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__o(fo__c_2Eieee_2Eis__infinity(X0,X1)) = ap(ap(c_2Eieee_2Eis__infinity,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)))))).
tff(tp_c_2Eieee_2Eis__integral,type,(c_2Eieee_2Eis__integral:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__integral,type,(fo__c_2Eieee_2Eis__integral:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__integral,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__o(fo__c_2Eieee_2Eis__integral(X0,X1)) = ap(ap(c_2Eieee_2Eis__integral,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)))))).
tff(tp_c_2Eieee_2Eis__nan,type,(c_2Eieee_2Eis__nan:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__nan,type,(fo__c_2Eieee_2Eis__nan:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__nan,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__o(fo__c_2Eieee_2Eis__nan(X0,X1)) = ap(ap(c_2Eieee_2Eis__nan,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)))))).
tff(tp_c_2Eieee_2Eis__normal,type,(c_2Eieee_2Eis__normal:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__normal,type,(fo__c_2Eieee_2Eis__normal:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__normal,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__o(fo__c_2Eieee_2Eis__normal(X0,X1)) = ap(ap(c_2Eieee_2Eis__normal,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)))))).
tff(tp_c_2Eieee_2Eis__single,type,(c_2Eieee_2Eis__single:$i)).
tff(mem_c_2Eieee_2Eis__single,axiom,mem(c_2Eieee_2Eis__single,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))).
tff(stp_fo_c_2Eieee_2Eis__single,type,(fo__c_2Eieee_2Eis__single:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__single,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Eieee_2Eis__single(X0)) = ap(c_2Eieee_2Eis__single,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eieee_2Eis__single__extended,type,(c_2Eieee_2Eis__single__extended:$i)).
tff(mem_c_2Eieee_2Eis__single__extended,axiom,mem(c_2Eieee_2Eis__single__extended,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))).
tff(stp_fo_c_2Eieee_2Eis__single__extended,type,(fo__c_2Eieee_2Eis__single__extended:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__single__extended,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Eieee_2Eis__single__extended(X0)) = ap(c_2Eieee_2Eis__single__extended,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eieee_2Eis__valid,type,(c_2Eieee_2Eis__valid:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__valid,type,(fo__c_2Eieee_2Eis__valid:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__valid,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__o(fo__c_2Eieee_2Eis__valid(X0,X1)) = ap(ap(c_2Eieee_2Eis__valid,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)))))).
tff(tp_c_2Eieee_2Eis__zero,type,(c_2Eieee_2Eis__zero:$i)).
tff(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)))).
tff(stp_fo_c_2Eieee_2Eis__zero,type,(fo__c_2Eieee_2Eis__zero:(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__o)).
tff(stp_eq_fo_c_2Eieee_2Eis__zero,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__o(fo__c_2Eieee_2Eis__zero(X0,X1)) = ap(ap(c_2Eieee_2Eis__zero,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)))))).
tff(tp_c_2Eieee_2Elargest,type,(c_2Eieee_2Elargest:$i)).
tff(mem_c_2Eieee_2Elargest,axiom,mem(c_2Eieee_2Elargest,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Erealax_2Ereal))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Eminus,type,(c_2Eieee_2Eminus:$i)).
tff(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)))))).
tff(tp_c_2Eieee_2Eminus__infinity,type,(c_2Eieee_2Eminus__infinity:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Eminus__zero,type,(c_2Eieee_2Eminus__zero:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Enum2ccode,type,(c_2Eieee_2Enum2ccode:$i)).
tff(mem_c_2Eieee_2Enum2ccode,axiom,mem(c_2Eieee_2Enum2ccode,arr(ty_2Enum_2Enum,ty_2Eieee_2Eccode))).
tff(stp_fo_c_2Eieee_2Enum2ccode,type,(fo__c_2Eieee_2Enum2ccode:(tp__ty_2Enum_2Enum) > tp__ty_2Eieee_2Eccode)).
tff(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))))).
tff(tp_c_2Eieee_2Enum2roundmode,type,(c_2Eieee_2Enum2roundmode:$i)).
tff(mem_c_2Eieee_2Enum2roundmode,axiom,mem(c_2Eieee_2Enum2roundmode,arr(ty_2Enum_2Enum,ty_2Eieee_2Eroundmode))).
tff(stp_fo_c_2Eieee_2Enum2roundmode,type,(fo__c_2Eieee_2Enum2roundmode:(tp__ty_2Enum_2Enum) > tp__ty_2Eieee_2Eroundmode)).
tff(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))))).
tff(tp_c_2Eieee_2Eplus__infinity,type,(c_2Eieee_2Eplus__infinity:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Eplus__zero,type,(c_2Eieee_2Eplus__zero:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Erem,type,(c_2Eieee_2Erem:$i)).
tff(mem_c_2Eieee_2Erem,axiom,mem(c_2Eieee_2Erem,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Eieee_2Erem,type,(fo__c_2Eieee_2Erem:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(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)))))).
tff(tp_c_2Eieee_2Eround,type,(c_2Eieee_2Eround:$i)).
tff(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))))))).
tff(tp_c_2Eieee_2Eroundmode2num,type,(c_2Eieee_2Eroundmode2num:$i)).
tff(mem_c_2Eieee_2Eroundmode2num,axiom,mem(c_2Eieee_2Eroundmode2num,arr(ty_2Eieee_2Eroundmode,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2Eroundmode2num,type,(fo__c_2Eieee_2Eroundmode2num:(tp__ty_2Eieee_2Eroundmode) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Eieee_2Eroundmode__CASE,type,(c_2Eieee_2Eroundmode__CASE:del > $i)).
tff(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)))))))).
tff(tp_c_2Eieee_2Eroundmode__size,type,(c_2Eieee_2Eroundmode__size:$i)).
tff(mem_c_2Eieee_2Eroundmode__size,axiom,mem(c_2Eieee_2Eroundmode__size,arr(ty_2Eieee_2Eroundmode,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eieee_2Eroundmode__size,type,(fo__c_2Eieee_2Eroundmode__size:(tp__ty_2Eieee_2Eroundmode) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Eieee_2Esign,type,(c_2Eieee_2Esign:$i)).
tff(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))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Esome__nan,type,(c_2Eieee_2Esome__nan:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Ethreshold,type,(c_2Eieee_2Ethreshold:$i)).
tff(mem_c_2Eieee_2Ethreshold,axiom,mem(c_2Eieee_2Ethreshold,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Erealax_2Ereal))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Etopfloat,type,(c_2Eieee_2Etopfloat:$i)).
tff(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))))).
tff(tp_c_2Eieee_2Eulp,type,(c_2Eieee_2Eulp:$i)).
tff(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)))).
tff(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)).
tff(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)))))).
tff(tp_c_2Eieee_2Evalof,type,(c_2Eieee_2Evalof:$i)).
tff(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)))).
tff(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)).
tff(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)))))).
tff(tp_c_2Eieee_2Ewordlength,type,(c_2Eieee_2Ewordlength:$i)).
tff(mem_c_2Eieee_2Ewordlength,axiom,mem(c_2Eieee_2Ewordlength,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(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)).
tff(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))))).
tff(tp_c_2Eieee_2Ezerosign,type,(c_2Eieee_2Ezerosign:$i)).
tff(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))))))).
tff(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)))).
tff(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)))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))).
tff(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))))).
tff(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))))).
tff(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))))))).
tff(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)))))).
tff(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))))))))).
tff(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))))))).
tff(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)))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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),f3035),V0rep))))).
tff(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(f3036,inj__ty_2Enum_2Enum(V1r))) <=> (surj__ty_2Enum_2Enum(ap(c_2Eieee_2Eroundmode2num,ap(c_2Eieee_2Enum2roundmode,inj__ty_2Enum_2Enum(V1r)))) = V1r))))).
tff(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)))).
tff(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))))).
tff(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)))))))).
tff(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)))))).
tff(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))))))))))).
tff(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))))))))).
tff(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)))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))).
tff(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(f3037(A_27a,V2v1,V3v2,V4v3,V1v0),ap(c_2Eieee_2Eroundmode2num,inj__ty_2Eieee_2Eroundmode(V0x))))))))))))))).
tff(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))))))))))))))).
tff(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)))))))).
tff(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))))))))).
tff(conj_thm_2Eieee_2Eroundmode__nchotomy,conjecture,(( ! [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))))))).
