include('Axioms/complex+2.ax').
fof(ne_ty_2Eieee_2Eccode,axiom,( ne(ty_2Eieee_2Eccode) )).
fof(ne_ty_2Eieee_2Efloat,axiom,( ne(ty_2Eieee_2Efloat) )).
fof(ne_ty_2Eieee_2Eroundmode,axiom,( ne(ty_2Eieee_2Eroundmode) )).
fof(mem_c_2Eieee_2EEq,axiom,( mem(c_2Eieee_2EEq,ty_2Eieee_2Eccode) )).
fof(mem_c_2Eieee_2EExponent,axiom,( mem(c_2Eieee_2EExponent,arr(ty_2Eieee_2Efloat,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2EFinite,axiom,( mem(c_2Eieee_2EFinite,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2EFloat,axiom,( mem(c_2Eieee_2EFloat,arr(ty_2Erealax_2Ereal,ty_2Eieee_2Efloat)) )).
fof(mem_c_2Eieee_2EFraction,axiom,( mem(c_2Eieee_2EFraction,arr(ty_2Eieee_2Efloat,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2EGt,axiom,( mem(c_2Eieee_2EGt,ty_2Eieee_2Eccode) )).
fof(mem_c_2Eieee_2EInfinity,axiom,( mem(c_2Eieee_2EInfinity,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2EIsdenormal,axiom,( mem(c_2Eieee_2EIsdenormal,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2EIsintegral,axiom,( mem(c_2Eieee_2EIsintegral,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2EIsnan,axiom,( mem(c_2Eieee_2EIsnan,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2EIsnormal,axiom,( mem(c_2Eieee_2EIsnormal,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2EIszero,axiom,( mem(c_2Eieee_2EIszero,arr(ty_2Eieee_2Efloat,bool)) )).
fof(mem_c_2Eieee_2ELt,axiom,( mem(c_2Eieee_2ELt,ty_2Eieee_2Eccode) )).
fof(mem_c_2Eieee_2EMinus__infinity,axiom,( mem(c_2Eieee_2EMinus__infinity,ty_2Eieee_2Efloat) )).
fof(mem_c_2Eieee_2EMinus__zero,axiom,( mem(c_2Eieee_2EMinus__zero,ty_2Eieee_2Efloat) )).
fof(mem_c_2Eieee_2EPlus__infinity,axiom,( mem(c_2Eieee_2EPlus__infinity,ty_2Eieee_2Efloat) )).
fof(mem_c_2Eieee_2EPlus__zero,axiom,( mem(c_2Eieee_2EPlus__zero,ty_2Eieee_2Efloat) )).
fof(mem_c_2Eieee_2EROUNDFLOAT,axiom,( mem(c_2Eieee_2EROUNDFLOAT,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)) )).
fof(mem_c_2Eieee_2ESign,axiom,( mem(c_2Eieee_2ESign,arr(ty_2Eieee_2Efloat,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2ETo__nearest,axiom,( mem(c_2Eieee_2ETo__nearest,ty_2Eieee_2Eroundmode) )).
fof(mem_c_2Eieee_2ETo__ninfinity,axiom,( mem(c_2Eieee_2ETo__ninfinity,ty_2Eieee_2Eroundmode) )).
fof(mem_c_2Eieee_2ETo__pinfinity,axiom,( mem(c_2Eieee_2ETo__pinfinity,ty_2Eieee_2Eroundmode) )).
fof(mem_c_2Eieee_2EUlp,axiom,( mem(c_2Eieee_2EUlp,arr(ty_2Eieee_2Efloat,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Eieee_2EUn,axiom,( mem(c_2Eieee_2EUn,ty_2Eieee_2Eccode) )).
fof(mem_c_2Eieee_2EVal,axiom,( mem(c_2Eieee_2EVal,arr(ty_2Eieee_2Efloat,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Eieee_2Ebias,axiom,( mem(c_2Eieee_2Ebias,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )).
fof(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)))) )).
fof(mem_c_2Eieee_2Eccode2num,axiom,( mem(c_2Eieee_2Eccode2num,arr(ty_2Eieee_2Eccode,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2Eccode__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))))) ) )).
fof(mem_c_2Eieee_2Eccode__size,axiom,( mem(c_2Eieee_2Eccode__size,arr(ty_2Eieee_2Eccode,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2Eclosest,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(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)))) )).
fof(mem_c_2Eieee_2Eemax,axiom,( mem(c_2Eieee_2Eemax,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )).
fof(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))) )).
fof(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)) )).
fof(mem_c_2Eieee_2Eexpwidth,axiom,( mem(c_2Eieee_2Eexpwidth,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )).
fof(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))))))) )).
fof(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)))) )).
fof(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))))))) )).
fof(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)))) )).
fof(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)))) )).
fof(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)))) )).
fof(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)))))) )).
fof(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)))) )).
fof(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)) )).
fof(mem_c_2Eieee_2Efloat__To__zero,axiom,( mem(c_2Eieee_2Efloat__To__zero,ty_2Eieee_2Eroundmode) )).
fof(mem_c_2Eieee_2Efloat__abs,axiom,( mem(c_2Eieee_2Efloat__abs,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)) )).
fof(mem_c_2Eieee_2Efloat__add,axiom,( mem(c_2Eieee_2Efloat__add,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))) )).
fof(mem_c_2Eieee_2Efloat__div,axiom,( mem(c_2Eieee_2Efloat__div,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))) )).
fof(mem_c_2Eieee_2Efloat__eq,axiom,( mem(c_2Eieee_2Efloat__eq,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool))) )).
fof(mem_c_2Eieee_2Efloat__format,axiom,( mem(c_2Eieee_2Efloat__format,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2Efloat__ge,axiom,( mem(c_2Eieee_2Efloat__ge,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool))) )).
fof(mem_c_2Eieee_2Efloat__gt,axiom,( mem(c_2Eieee_2Efloat__gt,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool))) )).
fof(mem_c_2Eieee_2Efloat__le,axiom,( mem(c_2Eieee_2Efloat__le,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool))) )).
fof(mem_c_2Eieee_2Efloat__lt,axiom,( mem(c_2Eieee_2Efloat__lt,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,bool))) )).
fof(mem_c_2Eieee_2Efloat__mul,axiom,( mem(c_2Eieee_2Efloat__mul,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))) )).
fof(mem_c_2Eieee_2Efloat__neg,axiom,( mem(c_2Eieee_2Efloat__neg,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)) )).
fof(mem_c_2Eieee_2Efloat__rem,axiom,( mem(c_2Eieee_2Efloat__rem,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))) )).
fof(mem_c_2Eieee_2Efloat__sqrt,axiom,( mem(c_2Eieee_2Efloat__sqrt,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat)) )).
fof(mem_c_2Eieee_2Efloat__sub,axiom,( mem(c_2Eieee_2Efloat__sub,arr(ty_2Eieee_2Efloat,arr(ty_2Eieee_2Efloat,ty_2Eieee_2Efloat))) )).
fof(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)))) )).
fof(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))))))) )).
fof(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)))))) )).
fof(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)) )).
fof(mem_c_2Eieee_2Efracwidth,axiom,( mem(c_2Eieee_2Efracwidth,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )).
fof(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))))))) )).
fof(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)))))) )).
fof(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))))))) )).
fof(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)))))) )).
fof(mem_c_2Eieee_2Eis__closest,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(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))) )).
fof(mem_c_2Eieee_2Eis__double,axiom,( mem(c_2Eieee_2Eis__double,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) )).
fof(mem_c_2Eieee_2Eis__double__extended,axiom,( mem(c_2Eieee_2Eis__double__extended,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) )).
fof(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))) )).
fof(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))) )).
fof(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))) )).
fof(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))) )).
fof(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))) )).
fof(mem_c_2Eieee_2Eis__single,axiom,( mem(c_2Eieee_2Eis__single,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) )).
fof(mem_c_2Eieee_2Eis__single__extended,axiom,( mem(c_2Eieee_2Eis__single__extended,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) )).
fof(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))) )).
fof(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))) )).
fof(mem_c_2Eieee_2Elargest,axiom,( mem(c_2Eieee_2Elargest,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Erealax_2Ereal)) )).
fof(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))))) )).
fof(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)))) )).
fof(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)))) )).
fof(mem_c_2Eieee_2Enum2ccode,axiom,( mem(c_2Eieee_2Enum2ccode,arr(ty_2Enum_2Enum,ty_2Eieee_2Eccode)) )).
fof(mem_c_2Eieee_2Enum2roundmode,axiom,( mem(c_2Eieee_2Enum2roundmode,arr(ty_2Enum_2Enum,ty_2Eieee_2Eroundmode)) )).
fof(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)))) )).
fof(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)))) )).
fof(mem_c_2Eieee_2Erem,axiom,( mem(c_2Eieee_2Erem,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(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)))))) )).
fof(mem_c_2Eieee_2Eroundmode2num,axiom,( mem(c_2Eieee_2Eroundmode2num,arr(ty_2Eieee_2Eroundmode,ty_2Enum_2Enum)) )).
fof(mem_c_2Eieee_2Eroundmode__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))))) ) )).
fof(mem_c_2Eieee_2Eroundmode__size,axiom,( mem(c_2Eieee_2Eroundmode__size,arr(ty_2Eieee_2Eroundmode,ty_2Enum_2Enum)) )).
fof(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)) )).
fof(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)))) )).
fof(mem_c_2Eieee_2Ethreshold,axiom,( mem(c_2Eieee_2Ethreshold,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Erealax_2Ereal)) )).
fof(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)))) )).
fof(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))) )).
fof(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))) )).
fof(mem_c_2Eieee_2Ewordlength,axiom,( mem(c_2Eieee_2Ewordlength,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )).
fof(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)))))) )).
fof(ax_thm_2Eieee_2Eexpwidth,axiom, ! [V0ew] : ( mem(V0ew,ty_2Enum_2Enum) => ! [V1fw] : ( mem(V1fw,ty_2Enum_2Enum) => ( ap(c_2Eieee_2Eexpwidth,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V0ew),V1fw)) = V0ew ) ) )).
fof(ax_thm_2Eieee_2Efracwidth,axiom, ! [V0ew] : ( mem(V0ew,ty_2Enum_2Enum) => ! [V1fw] : ( mem(V1fw,ty_2Enum_2Enum) => ( ap(c_2Eieee_2Efracwidth,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V0ew),V1fw)) = V1fw ) ) )).
fof(ax_thm_2Eieee_2Ewordlength,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Ewordlength,V0X) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Eieee_2Eexpwidth,V0X)),ap(c_2Eieee_2Efracwidth,V0X))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) )).
fof(ax_thm_2Eieee_2Eemax,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Eemax,V0X) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Eexpwidth,V0X))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) )).
fof(ax_thm_2Eieee_2Ebias,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Ebias,V0X) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Eieee_2Eexpwidth,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) )).
fof(ax_thm_2Eieee_2Eis__single,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( p(ap(c_2Eieee_2Eis__single,V0X)) <=> ( ( ap(c_2Eieee_2Eexpwidth,V0X) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) & ( ap(c_2Eieee_2Ewordlength,V0X) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__double,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( p(ap(c_2Eieee_2Eis__double,V0X)) <=> ( ( ap(c_2Eieee_2Eexpwidth,V0X) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) & ( ap(c_2Eieee_2Ewordlength,V0X) = 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,c_2Earithmetic_2EZERO))))))) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__single__extended,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( p(ap(c_2Eieee_2Eis__single__extended,V0X)) <=> ( p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Eieee_2Eexpwidth,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Eieee_2Ewordlength,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,c_2Earithmetic_2EZERO)))))))) ) ) )).
fof(ax_thm_2Eieee_2Eis__double__extended,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( p(ap(c_2Eieee_2Eis__double__extended,V0X)) <=> ( p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Eieee_2Eexpwidth,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Eieee_2Ewordlength,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,c_2Earithmetic_2EZERO))))))))) ) ) )).
fof(ax_thm_2Eieee_2Esign,axiom, ! [V0s] : ( mem(V0s,ty_2Enum_2Enum) => ! [V1e] : ( mem(V1e,ty_2Enum_2Enum) => ! [V2f] : ( mem(V2f,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)),V0s),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V1e),V2f))) = V0s ) ) ) )).
fof(ax_thm_2Eieee_2Eexponent,axiom, ! [V0s] : ( mem(V0s,ty_2Enum_2Enum) => ! [V1e] : ( mem(V1e,ty_2Enum_2Enum) => ! [V2f] : ( mem(V2f,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)),V0s),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V1e),V2f))) = V1e ) ) ) )).
fof(ax_thm_2Eieee_2Efraction,axiom, ! [V0s] : ( mem(V0s,ty_2Enum_2Enum) => ! [V1e] : ( mem(V1e,ty_2Enum_2Enum) => ! [V2f] : ( mem(V2f,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)),V0s),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V1e),V2f))) = V2f ) ) ) )).
fof(ax_thm_2Eieee_2Eis__nan,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__nan,V0X),V1a)) <=> ( ( ap(c_2Eieee_2Eexponent,V1a) = ap(c_2Eieee_2Eemax,V0X) ) & ( ~~ ( ap(c_2Eieee_2Efraction,V1a) = c_2Enum_2E0 ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__infinity,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__infinity,V0X),V1a)) <=> ( ( ap(c_2Eieee_2Eexponent,V1a) = ap(c_2Eieee_2Eemax,V0X) ) & ( ap(c_2Eieee_2Efraction,V1a) = c_2Enum_2E0 ) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__normal,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__normal,V0X),V1a)) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Eieee_2Eexponent,V1a))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Eieee_2Eexponent,V1a)),ap(c_2Eieee_2Eemax,V0X))) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__denormal,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__denormal,V0X),V1a)) <=> ( ( ap(c_2Eieee_2Eexponent,V1a) = c_2Enum_2E0 ) & ( ~~ ( ap(c_2Eieee_2Efraction,V1a) = c_2Enum_2E0 ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__zero,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__zero,V0X),V1a)) <=> ( ( ap(c_2Eieee_2Eexponent,V1a) = c_2Enum_2E0 ) & ( ap(c_2Eieee_2Efraction,V1a) = c_2Enum_2E0 ) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__valid,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1s] : ( mem(V1s,ty_2Enum_2Enum) => ! [V2e] : ( mem(V2e,ty_2Enum_2Enum) => ! [V3f] : ( mem(V3f,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eieee_2Eis__valid,V0X),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),V1s),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V2e),V3f)))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,V1s),ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,c_2Enum_2E0)))) & ( p(ap(ap(c_2Eprim__rec_2E_3C,V2e),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Eexpwidth,V0X)))) & p(ap(ap(c_2Eprim__rec_2E_3C,V3f),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Efracwidth,V0X)))) ) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__finite,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__finite,V0X),V1a)) <=> ( p(ap(ap(c_2Eieee_2Eis__valid,V0X),V1a)) & ( p(ap(ap(c_2Eieee_2Eis__normal,V0X),V1a)) | ( p(ap(ap(c_2Eieee_2Eis__denormal,V0X),V1a)) | p(ap(ap(c_2Eieee_2Eis__zero,V0X),V1a)) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eplus__infinity,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Eplus__infinity,V0X) = ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Enum_2E0),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Eieee_2Eemax,V0X)),c_2Enum_2E0)) ) )).
fof(ax_thm_2Eieee_2Eminus__infinity,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Eminus__infinity,V0X) = 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,c_2Earithmetic_2EZERO))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Eieee_2Eemax,V0X)),c_2Enum_2E0)) ) )).
fof(ax_thm_2Eieee_2Eplus__zero,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Eplus__zero,V0X) = ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Enum_2E0),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),c_2Enum_2E0)) ) )).
fof(ax_thm_2Eieee_2Eminus__zero,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Eminus__zero,V0X) = 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,c_2Earithmetic_2EZERO))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),c_2Enum_2E0)) ) )).
fof(ax_thm_2Eieee_2Etopfloat,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Etopfloat,V0X) = ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),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,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Efracwidth,V0X))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) )).
fof(ax_thm_2Eieee_2Ebottomfloat,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Ebottomfloat,V0X) = 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,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,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Efracwidth,V0X))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) )).
fof(ax_thm_2Eieee_2Eminus,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(c_2Eieee_2Eminus,V0X),V1a) = 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,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Esign,V1a))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Eieee_2Eexponent,V1a)),ap(c_2Eieee_2Efraction,V1a))) ) ) )).
fof(ax_thm_2Eieee_2Eencoding,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1s] : ( mem(V1s,ty_2Enum_2Enum) => ! [V2e] : ( mem(V2e,ty_2Enum_2Enum) => ! [V3f] : ( mem(V3f,ty_2Enum_2Enum) => ( ap(ap(c_2Eieee_2Eencoding,V0X),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),V1s),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V2e),V3f))) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,V1s),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Eieee_2Ewordlength,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(ap(c_2Earithmetic_2E_2A,V2e),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Efracwidth,V0X))))),V3f) ) ) ) ) )).
fof(ax_thm_2Eieee_2Evalof,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1s] : ( mem(V1s,ty_2Enum_2Enum) => ! [V2e] : ( mem(V2e,ty_2Enum_2Enum) => ! [V3f] : ( mem(V3f,ty_2Enum_2Enum) => ( ap(ap(c_2Eieee_2Evalof,V0X),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),V1s),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),V2e),V3f))) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V2e),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,c_2Earithmetic_2EZERO))))),V1s)),ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Ebias,V0X))))),ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,V3f)),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Efracwidth,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,c_2Earithmetic_2EZERO))))),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,c_2Earithmetic_2EZERO)))),V2e)),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Ebias,V0X))))),ap(ap(c_2Erealax_2Ereal__add,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,V3f)),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Efracwidth,V0X)))))) ) ) ) ) )).
fof(ax_thm_2Eieee_2Elargest,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Elargest,V0X) = 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,c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Eieee_2Eemax,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Ebias,V0X)))),ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,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,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Efracwidth,V0X))))) ) )).
fof(ax_thm_2Eieee_2Ethreshold,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Ethreshold,V0X) = 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,c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Eieee_2Eemax,V0X)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Ebias,V0X)))),ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,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,c_2Earithmetic_2EZERO)))),ap(c_2Enum_2ESUC,ap(c_2Eieee_2Efracwidth,V0X)))))) ) )).
fof(ax_thm_2Eieee_2Eulp,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(c_2Eieee_2Eulp,V0X),V1a) = ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Eieee_2Evalof,V0X),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Enum_2E0),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Eieee_2Eexponent,V1a)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(ap(c_2Eieee_2Evalof,V0X),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Enum_2E0),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Eieee_2Eexponent,V1a)),c_2Enum_2E0)))) ) ) )).
fof(ax_thm_2Eieee_2Eroundmode__TY__DEF,axiom, ? [V0rep] : ( mem(V0rep,arr(ty_2Eieee_2Eroundmode,ty_2Enum_2Enum)) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Enum_2Enum,ty_2Eieee_2Eroundmode),f3035),V0rep)) )).
fof(ax_thm_2Eieee_2Eroundmode__BIJ,axiom, ( ( ! [V0a] : ( mem(V0a,ty_2Eieee_2Eroundmode) => ( ap(c_2Eieee_2Enum2roundmode,ap(c_2Eieee_2Eroundmode2num,V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,ty_2Enum_2Enum) => ( p(ap(f3036,V1r)) <=> ( ap(c_2Eieee_2Eroundmode2num,ap(c_2Eieee_2Enum2roundmode,V1r)) = V1r ) ) ) )).
fof(conj_thm_2Eieee_2Enum2roundmode__roundmode2num,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eroundmode) => ( ap(c_2Eieee_2Enum2roundmode,ap(c_2Eieee_2Eroundmode2num,V0a)) = V0a ) ))).
fof(conj_thm_2Eieee_2Eroundmode2num__num2roundmode,lemma,(! [V0r] : ( mem(V0r,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) <=> ( ap(c_2Eieee_2Eroundmode2num,ap(c_2Eieee_2Enum2roundmode,V0r)) = V0r ) ) ))).
fof(conj_thm_2Eieee_2Enum2roundmode__11,lemma,(! [V0r] : ( mem(V0r,ty_2Enum_2Enum) => ! [V1r_27] : ( mem(V1r_27,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1r_27),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) => ( ( ap(c_2Eieee_2Enum2roundmode,V0r) = ap(c_2Eieee_2Enum2roundmode,V1r_27) ) <=> ( V0r = V1r_27 ) ) ) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode2num__11,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eroundmode) => ! [V1a_27] : ( mem(V1a_27,ty_2Eieee_2Eroundmode) => ( ( ap(c_2Eieee_2Eroundmode2num,V0a) = ap(c_2Eieee_2Eroundmode2num,V1a_27) ) <=> ( V0a = V1a_27 ) ) ) ))).
fof(conj_thm_2Eieee_2Enum2roundmode__ONTO,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eroundmode) => ? [V1r] : ( mem(V1r,ty_2Enum_2Enum) & ( ( V0a = ap(c_2Eieee_2Enum2roundmode,V1r) ) & p(ap(ap(c_2Eprim__rec_2E_3C,V1r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode2num__ONTO,lemma,(! [V0r] : ( mem(V0r,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) <=> ? [V1a] : ( mem(V1a,ty_2Eieee_2Eroundmode) & ( V0r = ap(c_2Eieee_2Eroundmode2num,V1a) ) ) ) ))).
fof(conj_thm_2Eieee_2Enum2roundmode__thm,lemma,(( ( ap(c_2Eieee_2Enum2roundmode,c_2Enum_2E0) = c_2Eieee_2ETo__nearest ) & ( ( ap(c_2Eieee_2Enum2roundmode,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = c_2Eieee_2Efloat__To__zero ) & ( ( ap(c_2Eieee_2Enum2roundmode,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = c_2Eieee_2ETo__pinfinity ) & ( ap(c_2Eieee_2Enum2roundmode,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = c_2Eieee_2ETo__ninfinity ) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode2num__thm,lemma,(( ( ap(c_2Eieee_2Eroundmode2num,c_2Eieee_2ETo__nearest) = c_2Enum_2E0 ) & ( ( ap(c_2Eieee_2Eroundmode2num,c_2Eieee_2Efloat__To__zero) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) & ( ( ap(c_2Eieee_2Eroundmode2num,c_2Eieee_2ETo__pinfinity) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) ) & ( ap(c_2Eieee_2Eroundmode2num,c_2Eieee_2ETo__ninfinity) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode__EQ__roundmode,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eroundmode) => ! [V1a_27] : ( mem(V1a_27,ty_2Eieee_2Eroundmode) => ( ( V0a = V1a_27 ) <=> ( ap(c_2Eieee_2Eroundmode2num,V0a) = ap(c_2Eieee_2Eroundmode2num,V1a_27) ) ) ) ))).
fof(ax_thm_2Eieee_2Eroundmode__size__def,axiom, ! [V0x] : ( mem(V0x,ty_2Eieee_2Eroundmode) => ( ap(c_2Eieee_2Eroundmode__size,V0x) = c_2Enum_2E0 ) )).
fof(ax_thm_2Eieee_2Eroundmode__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eieee_2Eroundmode) => ! [V1v0] : ( mem(V1v0,A_27a) => ! [V2v1] : ( mem(V2v1,A_27a) => ! [V3v2] : ( mem(V3v2,A_27a) => ! [V4v3] : ( mem(V4v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),V0x),V1v0),V2v1),V3v2),V4v3) = ap(f3037(A_27a,V2v1,V3v2,V4v3,V1v0),ap(c_2Eieee_2Eroundmode2num,V0x)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eieee_2Eroundmode__case__def,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0v0] : ( mem(V0v0,A_27a) => ! [V1v1] : ( mem(V1v1,A_27a) => ! [V2v2] : ( mem(V2v2,A_27a) => ! [V3v3] : ( mem(V3v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),c_2Eieee_2ETo__nearest),V0v0),V1v1),V2v2),V3v3) = V0v0 ) ) ) ) ) ) & ( ( ! [V4v0] : ( mem(V4v0,A_27a) => ! [V5v1] : ( mem(V5v1,A_27a) => ! [V6v2] : ( mem(V6v2,A_27a) => ! [V7v3] : ( mem(V7v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),c_2Eieee_2Efloat__To__zero),V4v0),V5v1),V6v2),V7v3) = V5v1 ) ) ) ) ) ) & ( ( ! [V8v0] : ( mem(V8v0,A_27a) => ! [V9v1] : ( mem(V9v1,A_27a) => ! [V10v2] : ( mem(V10v2,A_27a) => ! [V11v3] : ( mem(V11v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),c_2Eieee_2ETo__pinfinity),V8v0),V9v1),V10v2),V11v3) = V10v2 ) ) ) ) ) ) & ! [V12v0] : ( mem(V12v0,A_27a) => ! [V13v1] : ( mem(V13v1,A_27a) => ! [V14v2] : ( mem(V14v2,A_27a) => ! [V15v3] : ( mem(V15v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),c_2Eieee_2ETo__ninfinity),V12v0),V13v1),V14v2),V15v3) = V15v3 ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eieee_2Edatatype__roundmode,lemma,(! [V0roundmode] : ( 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,c_2Eieee_2ETo__nearest),c_2Eieee_2Efloat__To__zero),c_2Eieee_2ETo__pinfinity),c_2Eieee_2ETo__ninfinity))) ))).
fof(conj_thm_2Eieee_2Eroundmode__distinct,lemma,(( ( ~~ ( c_2Eieee_2ETo__nearest = c_2Eieee_2Efloat__To__zero ) ) & ( ( ~~ ( c_2Eieee_2ETo__nearest = c_2Eieee_2ETo__pinfinity ) ) & ( ( ~~ ( c_2Eieee_2ETo__nearest = c_2Eieee_2ETo__ninfinity ) ) & ( ( ~~ ( c_2Eieee_2Efloat__To__zero = c_2Eieee_2ETo__pinfinity ) ) & ( ( ~~ ( c_2Eieee_2Efloat__To__zero = c_2Eieee_2ETo__ninfinity ) ) & ( ~~ ( c_2Eieee_2ETo__pinfinity = c_2Eieee_2ETo__ninfinity ) ) ) ) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode__nchotomy,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eroundmode) => ( ( V0a = c_2Eieee_2ETo__nearest ) | ( ( V0a = c_2Eieee_2Efloat__To__zero ) | ( ( V0a = c_2Eieee_2ETo__pinfinity ) | ( V0a = c_2Eieee_2ETo__ninfinity ) ) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x0] : ( mem(V0x0,A_27a) => ! [V1x1] : ( mem(V1x1,A_27a) => ! [V2x2] : ( mem(V2x2,A_27a) => ! [V3x3] : ( mem(V3x3,A_27a) => ? [V4f] : ( mem(V4f,arr(ty_2Eieee_2Eroundmode,A_27a)) & ( ( ap(V4f,c_2Eieee_2ETo__nearest) = V0x0 ) & ( ( ap(V4f,c_2Eieee_2Efloat__To__zero) = V1x1 ) & ( ( ap(V4f,c_2Eieee_2ETo__pinfinity) = V2x2 ) & ( ap(V4f,c_2Eieee_2ETo__ninfinity) = V3x3 ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eieee_2Eroundmode__induction,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eieee_2Eroundmode,bool)) => ( ( p(ap(V0P,c_2Eieee_2ETo__nearest)) & ( p(ap(V0P,c_2Eieee_2ETo__ninfinity)) & ( p(ap(V0P,c_2Eieee_2ETo__pinfinity)) & p(ap(V0P,c_2Eieee_2Efloat__To__zero)) ) ) ) => ! [V1a] : ( mem(V1a,ty_2Eieee_2Eroundmode) => p(ap(V0P,V1a)) ) ) ))).
fof(conj_thm_2Eieee_2Eroundmode__case__cong,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v0_27] : ( mem(V0v0_27,A_27a) => ! [V1v1_27] : ( mem(V1v1_27,A_27a) => ! [V2v2_27] : ( mem(V2v2_27,A_27a) => ! [V3v3_27] : ( mem(V3v3_27,A_27a) => ! [V4M] : ( mem(V4M,ty_2Eieee_2Eroundmode) => ! [V5M_27] : ( mem(V5M_27,ty_2Eieee_2Eroundmode) => ! [V6v0] : ( mem(V6v0,A_27a) => ! [V7v1] : ( mem(V7v1,A_27a) => ! [V8v2] : ( mem(V8v2,A_27a) => ! [V9v3] : ( mem(V9v3,A_27a) => ( ( ( V4M = V5M_27 ) & ( ( ( V5M_27 = c_2Eieee_2ETo__nearest ) => ( V6v0 = V0v0_27 ) ) & ( ( ( V5M_27 = c_2Eieee_2Efloat__To__zero ) => ( V7v1 = V1v1_27 ) ) & ( ( ( V5M_27 = c_2Eieee_2ETo__pinfinity ) => ( V8v2 = V2v2_27 ) ) & ( ( V5M_27 = c_2Eieee_2ETo__ninfinity ) => ( V9v3 = V3v3_27 ) ) ) ) ) ) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),V4M),V6v0),V7v1),V8v2),V9v3) = ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),V5M_27),V0v0_27),V1v1_27),V2v2_27),V3v3_27) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eieee_2Eroundmode__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eieee_2Eroundmode) => ! [V1v0] : ( mem(V1v0,A_27a) => ! [V2v1] : ( mem(V2v1,A_27a) => ! [V3v2] : ( mem(V3v2,A_27a) => ! [V4v3] : ( mem(V4v3,A_27a) => ! [V5v] : ( mem(V5v,A_27a) => ( ( ap(ap(ap(ap(ap(c_2Eieee_2Eroundmode__CASE(A_27a),V0x),V1v0),V2v1),V3v2),V4v3) = V5v ) <=> ( ( ( V0x = c_2Eieee_2ETo__nearest ) & ( V1v0 = V5v ) ) | ( ( ( V0x = c_2Eieee_2Efloat__To__zero ) & ( V2v1 = V5v ) ) | ( ( ( V0x = c_2Eieee_2ETo__pinfinity ) & ( V3v2 = V5v ) ) | ( ( V0x = c_2Eieee_2ETo__ninfinity ) & ( V4v3 = V5v ) ) ) ) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Eieee_2Eis__closest,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,arr(A_27a,ty_2Erealax_2Ereal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3a] : ( mem(V3a,A_27a) => ( p(ap(ap(ap(ap(c_2Eieee_2Eis__closest(A_27a),V0v),V1s),V2x),V3a)) <=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3a),V1s)) & ! [V4b] : ( mem(V4b,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4b),V1s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,ap(V0v,V3a)),V2x))),ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,ap(V0v,V4b)),V2x)))) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eclosest,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,arr(A_27a,ty_2Erealax_2Ereal)) => ! [V1p] : ( mem(V1p,arr(A_27a,bool)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ! [V3x] : ( mem(V3x,ty_2Erealax_2Ereal) => ( ap(ap(ap(ap(c_2Eieee_2Eclosest(A_27a),V0v),V1p),V2s),V3x) = ap(c_2Emin_2E_40(A_27a),f3150(A_27a,V1p,V2s,V0v,V3x)) ) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eround__def,axiom, ( ( ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eround,V0X),c_2Eieee_2ETo__nearest),V1x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__lte,V1x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Ethreshold,V0X)))),ap(c_2Eieee_2Eminus__infinity,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__ge,V1x),ap(c_2Eieee_2Ethreshold,V0X))),ap(c_2Eieee_2Eplus__infinity,V0X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V0X)),f3151),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3152(V0X))),V1x))) ) ) ) ) & ( ( ! [V4X] : ( mem(V4X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V5x] : ( mem(V5x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eround,V4X),c_2Eieee_2Efloat__To__zero),V5x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Erealax_2Ereal__lt,V5x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Elargest,V4X)))),ap(c_2Eieee_2Ebottomfloat,V4X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__gt,V5x),ap(c_2Eieee_2Elargest,V4X))),ap(c_2Eieee_2Etopfloat,V4X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V4X)),k(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Ebool_2ET)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3153(V4X,V5x))),V5x))) ) ) ) ) & ( ( ! [V8X] : ( mem(V8X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V9x] : ( mem(V9x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eround,V8X),c_2Eieee_2ETo__pinfinity),V9x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Erealax_2Ereal__lt,V9x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Elargest,V8X)))),ap(c_2Eieee_2Ebottomfloat,V8X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__gt,V9x),ap(c_2Eieee_2Elargest,V8X))),ap(c_2Eieee_2Eplus__infinity,V8X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V8X)),k(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Ebool_2ET)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3154(V8X,V9x))),V9x))) ) ) ) ) & ! [V12X] : ( mem(V12X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V13x] : ( mem(V13x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eround,V12X),c_2Eieee_2ETo__ninfinity),V13x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Erealax_2Ereal__lt,V13x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Elargest,V12X)))),ap(c_2Eieee_2Eminus__infinity,V12X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__gt,V13x),ap(c_2Eieee_2Elargest,V12X))),ap(c_2Eieee_2Etopfloat,V12X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V12X)),k(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Ebool_2ET)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3155(V12X,V13x))),V13x))) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eis__integral,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( p(ap(ap(c_2Eieee_2Eis__integral,V0X),V1a)) <=> ( p(ap(ap(c_2Eieee_2Eis__finite,V0X),V1a)) & ? [V2n] : ( mem(V2n,ty_2Enum_2Enum) & ( ap(c_2Ereal_2Eabs,ap(ap(c_2Eieee_2Evalof,V0X),V1a)) = ap(c_2Ereal_2Ereal__of__num,V2n) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Eintround__def,axiom, ( ( ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eintround,V0X),c_2Eieee_2ETo__nearest),V1x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__lte,V1x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Ethreshold,V0X)))),ap(c_2Eieee_2Eminus__infinity,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__ge,V1x),ap(c_2Eieee_2Ethreshold,V0X))),ap(c_2Eieee_2Eplus__infinity,V0X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V0X)),f3157(V0X)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3158(V0X))),V1x))) ) ) ) ) & ( ( ! [V5X] : ( mem(V5X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V6x] : ( mem(V6x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eintround,V5X),c_2Eieee_2Efloat__To__zero),V6x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Erealax_2Ereal__lt,V6x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Elargest,V5X)))),ap(c_2Eieee_2Ebottomfloat,V5X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__gt,V6x),ap(c_2Eieee_2Elargest,V5X))),ap(c_2Eieee_2Etopfloat,V5X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V5X)),k(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Ebool_2ET)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3159(V5X,V6x))),V6x))) ) ) ) ) & ( ( ! [V9X] : ( mem(V9X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V10x] : ( mem(V10x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eintround,V9X),c_2Eieee_2ETo__pinfinity),V10x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Erealax_2Ereal__lt,V10x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Elargest,V9X)))),ap(c_2Eieee_2Ebottomfloat,V9X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__gt,V10x),ap(c_2Eieee_2Elargest,V9X))),ap(c_2Eieee_2Eplus__infinity,V9X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V9X)),k(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Ebool_2ET)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3160(V9X,V10x))),V10x))) ) ) ) ) & ! [V13X] : ( mem(V13X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V14x] : ( mem(V14x,ty_2Erealax_2Ereal) => ( ap(ap(ap(c_2Eieee_2Eintround,V13X),c_2Eieee_2ETo__ninfinity),V14x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Erealax_2Ereal__lt,V14x),ap(c_2Erealax_2Ereal__neg,ap(c_2Eieee_2Elargest,V13X)))),ap(c_2Eieee_2Eminus__infinity,V13X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ereal_2Ereal__gt,V14x),ap(c_2Eieee_2Elargest,V13X))),ap(c_2Eieee_2Etopfloat,V13X)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(c_2Eieee_2Evalof,V13X)),k(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Ebool_2ET)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3161(V13X,V14x))),V14x))) ) ) ) ) ) )).
fof(ax_thm_2Eieee_2Esome__nan,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ( ap(c_2Eieee_2Esome__nan,V0X) = ap(c_2Emin_2E_40(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),f3162(V0X)) ) )).
fof(ax_thm_2Eieee_2Ezerosign,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1s] : ( mem(V1s,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(c_2Eieee_2Ezerosign,V0X),V1s),V2a) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__zero,V0X),V2a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1s),c_2Enum_2E0)),ap(c_2Eieee_2Eplus__zero,V0X)),ap(c_2Eieee_2Eminus__zero,V0X))),V2a) ) ) ) )).
fof(ax_thm_2Eieee_2Erem,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Eieee_2Erem,V0x),V1y) = ap(ap(c_2Ebool_2ELET(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3163(V1y,V0x)),ap(ap(ap(ap(c_2Eieee_2Eclosest(ty_2Erealax_2Ereal),c_2Ecombin_2EI(ty_2Erealax_2Ereal)),f3165),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3167)),ap(ap(c_2Ereal_2E_2F,V0x),V1y))) ) ) )).
fof(ax_thm_2Eieee_2Efintrnd,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(c_2Eieee_2Efintrnd,V0X),V1m),V2a) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),V2a),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(c_2Eieee_2Esign,V2a)),ap(ap(ap(c_2Eieee_2Eintround,V0X),V1m),ap(ap(c_2Eieee_2Evalof,V0X),V2a))))) ) ) ) )).
fof(ax_thm_2Eieee_2Efadd,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ! [V3b] : ( mem(V3b,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(ap(c_2Eieee_2Efadd,V0X),V1m),V2a),V3b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V3b)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)),ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b)))))))),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),V2a),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)),V3b),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__zero,V0X),V2a)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__zero,V0X),V3b)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))))),ap(c_2Eieee_2Esign,V2a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Eieee_2Eroundmode),V1m),c_2Eieee_2ETo__ninfinity)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),c_2Enum_2E0))),ap(ap(ap(c_2Eieee_2Eround,V0X),V1m),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Eieee_2Evalof,V0X),V2a)),ap(ap(c_2Eieee_2Evalof,V0X),V3b))))))) ) ) ) ) )).
fof(ax_thm_2Eieee_2Efsub,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ! [V3b] : ( mem(V3b,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(ap(c_2Eieee_2Efsub,V0X),V1m),V2a),V3b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V3b)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))))))),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),V2a),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)),ap(ap(c_2Eieee_2Eminus,V0X),V3b)),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__zero,V0X),V2a)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__zero,V0X),V3b)),ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b)))))),ap(c_2Eieee_2Esign,V2a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Eieee_2Eroundmode),V1m),c_2Eieee_2ETo__ninfinity)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),c_2Enum_2E0))),ap(ap(ap(c_2Eieee_2Eround,V0X),V1m),ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Eieee_2Evalof,V0X),V2a)),ap(ap(c_2Eieee_2Evalof,V0X),V3b))))))) ) ) ) ) )).
fof(ax_thm_2Eieee_2Efmul,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ! [V3b] : ( mem(V3b,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(ap(c_2Eieee_2Efmul,V0X),V1m),V2a),V3b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V3b)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__zero,V0X),V2a)),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b))),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Eieee_2Eis__zero,V0X),V3b)))))),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))),ap(c_2Eieee_2Eplus__infinity,V0X)),ap(c_2Eieee_2Eminus__infinity,V0X))),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(ap(c_2Eieee_2Eround,V0X),V1m),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Eieee_2Evalof,V0X),V2a)),ap(ap(c_2Eieee_2Evalof,V0X),V3b)))))) ) ) ) ) )).
fof(ax_thm_2Eieee_2Efdiv,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ! [V3b] : ( mem(V3b,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(ap(c_2Eieee_2Efdiv,V0X),V1m),V2a),V3b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V3b)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__zero,V0X),V2a)),ap(ap(c_2Eieee_2Eis__zero,V0X),V3b))),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)))))),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Eieee_2Eis__zero,V0X),V3b))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))),ap(c_2Eieee_2Eplus__infinity,V0X)),ap(c_2Eieee_2Eminus__infinity,V0X))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))),ap(c_2Eieee_2Eplus__zero,V0X)),ap(c_2Eieee_2Eminus__zero,V0X))),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Eieee_2Esign,V3b))),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(ap(c_2Eieee_2Eround,V0X),V1m),ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Eieee_2Evalof,V0X),V2a)),ap(ap(c_2Eieee_2Evalof,V0X),V3b))))))) ) ) ) ) )).
fof(ax_thm_2Eieee_2Efsqrt,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(c_2Eieee_2Efsqrt,V0X),V1m),V2a) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__zero,V0X),V2a)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),c_2Enum_2E0)))),V2a),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Eieee_2Esign,V2a)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(c_2Eieee_2Esign,V2a)),ap(ap(ap(c_2Eieee_2Eround,V0X),V1m),ap(c_2Etransc_2Esqrt,ap(ap(c_2Eieee_2Evalof,V0X),V2a))))))) ) ) ) )).
fof(ax_thm_2Eieee_2Efrem,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ! [V3b] : ( mem(V3b,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(ap(c_2Eieee_2Efrem,V0X),V1m),V2a),V3b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V2a)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__nan,V0X),V3b)),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Eieee_2Eis__infinity,V0X),V2a)),ap(ap(c_2Eieee_2Eis__zero,V0X),V3b))))),ap(c_2Eieee_2Esome__nan,V0X)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),ap(ap(c_2Eieee_2Eis__infinity,V0X),V3b)),V2a),ap(ap(ap(c_2Eieee_2Ezerosign,V0X),ap(c_2Eieee_2Esign,V2a)),ap(ap(ap(c_2Eieee_2Eround,V0X),V1m),ap(ap(c_2Eieee_2Erem,ap(ap(c_2Eieee_2Evalof,V0X),V2a)),ap(ap(c_2Eieee_2Evalof,V0X),V3b)))))) ) ) ) ) )).
fof(ax_thm_2Eieee_2Efneg,axiom, ! [V0X] : ( mem(V0X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => ! [V1m] : ( mem(V1m,ty_2Eieee_2Eroundmode) => ! [V2a] : ( mem(V2a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => ( ap(ap(ap(c_2Eieee_2Efneg,V0X),V1m),V2a) = 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,c_2Earithmetic_2EZERO))),ap(c_2Eieee_2Esign,V2a))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Eieee_2Eexponent,V2a)),ap(c_2Eieee_2Efraction,V2a))) ) ) ) )).
fof(ax_thm_2Eieee_2Eccode__TY__DEF,axiom, ? [V0rep] : ( mem(V0rep,arr(ty_2Eieee_2Eccode,ty_2Enum_2Enum)) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Enum_2Enum,ty_2Eieee_2Eccode),f3035),V0rep)) )).
fof(ax_thm_2Eieee_2Eccode__BIJ,axiom, ( ( ! [V0a] : ( mem(V0a,ty_2Eieee_2Eccode) => ( ap(c_2Eieee_2Enum2ccode,ap(c_2Eieee_2Eccode2num,V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,ty_2Enum_2Enum) => ( p(ap(f3036,V1r)) <=> ( ap(c_2Eieee_2Eccode2num,ap(c_2Eieee_2Enum2ccode,V1r)) = V1r ) ) ) )).
fof(conj_thm_2Eieee_2Enum2ccode__ccode2num,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eccode) => ( ap(c_2Eieee_2Enum2ccode,ap(c_2Eieee_2Eccode2num,V0a)) = V0a ) ))).
fof(conj_thm_2Eieee_2Eccode2num__num2ccode,lemma,(! [V0r] : ( mem(V0r,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) <=> ( ap(c_2Eieee_2Eccode2num,ap(c_2Eieee_2Enum2ccode,V0r)) = V0r ) ) ))).
fof(conj_thm_2Eieee_2Enum2ccode__11,lemma,(! [V0r] : ( mem(V0r,ty_2Enum_2Enum) => ! [V1r_27] : ( mem(V1r_27,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1r_27),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) => ( ( ap(c_2Eieee_2Enum2ccode,V0r) = ap(c_2Eieee_2Enum2ccode,V1r_27) ) <=> ( V0r = V1r_27 ) ) ) ) ) ))).
fof(conj_thm_2Eieee_2Eccode2num__11,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eccode) => ! [V1a_27] : ( mem(V1a_27,ty_2Eieee_2Eccode) => ( ( ap(c_2Eieee_2Eccode2num,V0a) = ap(c_2Eieee_2Eccode2num,V1a_27) ) <=> ( V0a = V1a_27 ) ) ) ))).
fof(conj_thm_2Eieee_2Enum2ccode__ONTO,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eccode) => ? [V1r] : ( mem(V1r,ty_2Enum_2Enum) & ( ( V0a = ap(c_2Eieee_2Enum2ccode,V1r) ) & p(ap(ap(c_2Eprim__rec_2E_3C,V1r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Eieee_2Eccode2num__ONTO,lemma,(! [V0r] : ( mem(V0r,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0r),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) <=> ? [V1a] : ( mem(V1a,ty_2Eieee_2Eccode) & ( V0r = ap(c_2Eieee_2Eccode2num,V1a) ) ) ) ))).
fof(conj_thm_2Eieee_2Enum2ccode__thm,lemma,(( ( ap(c_2Eieee_2Enum2ccode,c_2Enum_2E0) = c_2Eieee_2EGt ) & ( ( ap(c_2Eieee_2Enum2ccode,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = c_2Eieee_2ELt ) & ( ( ap(c_2Eieee_2Enum2ccode,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = c_2Eieee_2EEq ) & ( ap(c_2Eieee_2Enum2ccode,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = c_2Eieee_2EUn ) ) ) ))).
fof(conj_thm_2Eieee_2Eccode2num__thm,lemma,(( ( ap(c_2Eieee_2Eccode2num,c_2Eieee_2EGt) = c_2Enum_2E0 ) & ( ( ap(c_2Eieee_2Eccode2num,c_2Eieee_2ELt) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) & ( ( ap(c_2Eieee_2Eccode2num,c_2Eieee_2EEq) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) ) & ( ap(c_2Eieee_2Eccode2num,c_2Eieee_2EUn) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) ))).
fof(conj_thm_2Eieee_2Eccode__EQ__ccode,lemma,(! [V0a] : ( mem(V0a,ty_2Eieee_2Eccode) => ! [V1a_27] : ( mem(V1a_27,ty_2Eieee_2Eccode) => ( ( V0a = V1a_27 ) <=> ( ap(c_2Eieee_2Eccode2num,V0a) = ap(c_2Eieee_2Eccode2num,V1a_27) ) ) ) ))).
fof(ax_thm_2Eieee_2Eccode__size__def,axiom, ! [V0x] : ( mem(V0x,ty_2Eieee_2Eccode) => ( ap(c_2Eieee_2Eccode__size,V0x) = c_2Enum_2E0 ) )).
fof(ax_thm_2Eieee_2Eccode__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eieee_2Eccode) => ! [V1v0] : ( mem(V1v0,A_27a) => ! [V2v1] : ( mem(V2v1,A_27a) => ! [V3v2] : ( mem(V3v2,A_27a) => ! [V4v3] : ( mem(V4v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eccode__CASE(A_27a),V0x),V1v0),V2v1),V3v2),V4v3) = ap(f3037(A_27a,V2v1,V3v2,V4v3,V1v0),ap(c_2Eieee_2Eccode2num,V0x)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eieee_2Eccode__case__def,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0v0] : ( mem(V0v0,A_27a) => ! [V1v1] : ( mem(V1v1,A_27a) => ! [V2v2] : ( mem(V2v2,A_27a) => ! [V3v3] : ( mem(V3v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eccode__CASE(A_27a),c_2Eieee_2EGt),V0v0),V1v1),V2v2),V3v3) = V0v0 ) ) ) ) ) ) & ( ( ! [V4v0] : ( mem(V4v0,A_27a) => ! [V5v1] : ( mem(V5v1,A_27a) => ! [V6v2] : ( mem(V6v2,A_27a) => ! [V7v3] : ( mem(V7v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eccode__CASE(A_27a),c_2Eieee_2ELt),V4v0),V5v1),V6v2),V7v3) = V5v1 ) ) ) ) ) ) & ( ( ! [V8v0] : ( mem(V8v0,A_27a) => ! [V9v1] : ( mem(V9v1,A_27a) => ! [V10v2] : ( mem(V10v2,A_27a) => ! [V11v3] : ( mem(V11v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eccode__CASE(A_27a),c_2Eieee_2EEq),V8v0),V9v1),V10v2),V11v3) = V10v2 ) ) ) ) ) ) & ! [V12v0] : ( mem(V12v0,A_27a) => ! [V13v1] : ( mem(V13v1,A_27a) => ! [V14v2] : ( mem(V14v2,A_27a) => ! [V15v3] : ( mem(V15v3,A_27a) => ( ap(ap(ap(ap(ap(c_2Eieee_2Eccode__CASE(A_27a),c_2Eieee_2EUn),V12v0),V13v1),V14v2),V15v3) = V15v3 ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eieee_2Edatatype__ccode,lemma,(! [V0ccode] : ( mem(V0ccode,arr(ty_2Eieee_2Eccode,arr(ty_2Eieee_2Eccode,arr(ty_2Eieee_2Eccode,arr(ty_2Eieee_2Eccode,bool))))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(ap(V0ccode,c_2Eieee_2EGt),c_2Eieee_2ELt),c_2Eieee_2EEq),c_2Eieee_2EUn))) ))).
fof(conj_thm_2Eieee_2Eccode__distinct,conjecture,(( ( ~~ ( c_2Eieee_2EGt = c_2Eieee_2ELt ) ) & ( ( ~~ ( c_2Eieee_2EGt = c_2Eieee_2EEq ) ) & ( ( ~~ ( c_2Eieee_2EGt = c_2Eieee_2EUn ) ) & ( ( ~~ ( c_2Eieee_2ELt = c_2Eieee_2EEq ) ) & ( ( ~~ ( c_2Eieee_2ELt = c_2Eieee_2EUn ) ) & ( ~~ ( c_2Eieee_2EEq = c_2Eieee_2EUn ) ) ) ) ) ) ))).
