include('Axioms/transc_2.ax').
tff(tp_ty_2Ebinary__ieee_2Eflags,type,( ty_2Ebinary__ieee_2Eflags: del )).
tff(tp_ty_2Ebinary__ieee_2Efloat,type,( ty_2Ebinary__ieee_2Efloat: ( del * del ) > del )).
tff(tp_ty_2Ebinary__ieee_2Efloat__compare,type,( ty_2Ebinary__ieee_2Efloat__compare: del )).
tff(tp_ty_2Ebinary__ieee_2Efloat__value,type,( ty_2Ebinary__ieee_2Efloat__value: del )).
tff(tp_ty_2Ebinary__ieee_2Efp__op,type,( ty_2Ebinary__ieee_2Efp__op: ( del * del ) > del )).
tff(tp_ty_2Ebinary__ieee_2Erounding,type,( ty_2Ebinary__ieee_2Erounding: del )).
tff(stp_ty_2Ebinary__ieee_2Efloat__compare,type,(tp__ty_2Ebinary__ieee_2Efloat__compare : $tType)).
tff(stp_inj_ty_2Ebinary__ieee_2Efloat__compare,type,(inj__ty_2Ebinary__ieee_2Efloat__compare : tp__ty_2Ebinary__ieee_2Efloat__compare > $i)).
tff(stp_surj_ty_2Ebinary__ieee_2Efloat__compare,type,(surj__ty_2Ebinary__ieee_2Efloat__compare : $i > tp__ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_inj_surj_ty_2Ebinary__ieee_2Efloat__compare,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Efloat__compare] : (surj__ty_2Ebinary__ieee_2Efloat__compare(inj__ty_2Ebinary__ieee_2Efloat__compare(X)) = X))).
tff(stp_inj_mem_ty_2Ebinary__ieee_2Efloat__compare,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Efloat__compare] : (mem(inj__ty_2Ebinary__ieee_2Efloat__compare(X),ty_2Ebinary__ieee_2Efloat__compare)))).
tff(stp_iso_mem_ty_2Ebinary__ieee_2Efloat__compare,axiom,( ! [X:$i] : (mem(X,ty_2Ebinary__ieee_2Efloat__compare) => (X = inj__ty_2Ebinary__ieee_2Efloat__compare(surj__ty_2Ebinary__ieee_2Efloat__compare(X)))))).
tff(tp_c_2Ebinary__ieee_2EEQ,type,(c_2Ebinary__ieee_2EEQ:$i)).
tff(mem_c_2Ebinary__ieee_2EEQ,axiom,mem(c_2Ebinary__ieee_2EEQ,ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_fo_c_2Ebinary__ieee_2EEQ,type,(fo__c_2Ebinary__ieee_2EEQ:tp__ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EEQ,axiom,(inj__ty_2Ebinary__ieee_2Efloat__compare(fo__c_2Ebinary__ieee_2EEQ) = c_2Ebinary__ieee_2EEQ)).
tff(stp_ty_2Ebinary__ieee_2Erounding,type,(tp__ty_2Ebinary__ieee_2Erounding : $tType)).
tff(stp_inj_ty_2Ebinary__ieee_2Erounding,type,(inj__ty_2Ebinary__ieee_2Erounding : tp__ty_2Ebinary__ieee_2Erounding > $i)).
tff(stp_surj_ty_2Ebinary__ieee_2Erounding,type,(surj__ty_2Ebinary__ieee_2Erounding : $i > tp__ty_2Ebinary__ieee_2Erounding)).
tff(stp_inj_surj_ty_2Ebinary__ieee_2Erounding,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Erounding] : (surj__ty_2Ebinary__ieee_2Erounding(inj__ty_2Ebinary__ieee_2Erounding(X)) = X))).
tff(stp_inj_mem_ty_2Ebinary__ieee_2Erounding,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Erounding] : (mem(inj__ty_2Ebinary__ieee_2Erounding(X),ty_2Ebinary__ieee_2Erounding)))).
tff(stp_iso_mem_ty_2Ebinary__ieee_2Erounding,axiom,( ! [X:$i] : (mem(X,ty_2Ebinary__ieee_2Erounding) => (X = inj__ty_2Ebinary__ieee_2Erounding(surj__ty_2Ebinary__ieee_2Erounding(X)))))).
tff(tp_c_2Ebinary__ieee_2EFP__Add,type,(c_2Ebinary__ieee_2EFP__Add:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__Add,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__Add(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2EFP__Div,type,(c_2Ebinary__ieee_2EFP__Div:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__Div,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__Div(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2EFP__Mul,type,(c_2Ebinary__ieee_2EFP__Mul:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__Mul,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__Mul(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2EFP__MulAdd,type,(c_2Ebinary__ieee_2EFP__MulAdd:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__MulAdd,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__MulAdd(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w))))))))).
tff(tp_c_2Ebinary__ieee_2EFP__MulSub,type,(c_2Ebinary__ieee_2EFP__MulSub:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__MulSub,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__MulSub(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w))))))))).
tff(tp_c_2Ebinary__ieee_2EFP__Sqrt,type,(c_2Ebinary__ieee_2EFP__Sqrt:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__Sqrt,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__Sqrt(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w))))))).
tff(tp_c_2Ebinary__ieee_2EFP__Sub,type,(c_2Ebinary__ieee_2EFP__Sub:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EFP__Sub,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EFP__Sub(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w)))))))).
tff(stp_ty_2Ebinary__ieee_2Efloat__value,type,(tp__ty_2Ebinary__ieee_2Efloat__value : $tType)).
tff(stp_inj_ty_2Ebinary__ieee_2Efloat__value,type,(inj__ty_2Ebinary__ieee_2Efloat__value : tp__ty_2Ebinary__ieee_2Efloat__value > $i)).
tff(stp_surj_ty_2Ebinary__ieee_2Efloat__value,type,(surj__ty_2Ebinary__ieee_2Efloat__value : $i > tp__ty_2Ebinary__ieee_2Efloat__value)).
tff(stp_inj_surj_ty_2Ebinary__ieee_2Efloat__value,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Efloat__value] : (surj__ty_2Ebinary__ieee_2Efloat__value(inj__ty_2Ebinary__ieee_2Efloat__value(X)) = X))).
tff(stp_inj_mem_ty_2Ebinary__ieee_2Efloat__value,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Efloat__value] : (mem(inj__ty_2Ebinary__ieee_2Efloat__value(X),ty_2Ebinary__ieee_2Efloat__value)))).
tff(stp_iso_mem_ty_2Ebinary__ieee_2Efloat__value,axiom,( ! [X:$i] : (mem(X,ty_2Ebinary__ieee_2Efloat__value) => (X = inj__ty_2Ebinary__ieee_2Efloat__value(surj__ty_2Ebinary__ieee_2Efloat__value(X)))))).
tff(tp_c_2Ebinary__ieee_2EFloat,type,(c_2Ebinary__ieee_2EFloat:$i)).
tff(mem_c_2Ebinary__ieee_2EFloat,axiom,mem(c_2Ebinary__ieee_2EFloat,arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat__value))).
tff(stp_fo_c_2Ebinary__ieee_2EFloat,type,(fo__c_2Ebinary__ieee_2EFloat:(tp__ty_2Erealax_2Ereal) > tp__ty_2Ebinary__ieee_2Efloat__value)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EFloat,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Ebinary__ieee_2Efloat__value(fo__c_2Ebinary__ieee_2EFloat(X0)) = ap(c_2Ebinary__ieee_2EFloat,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Ebinary__ieee_2EGT,type,(c_2Ebinary__ieee_2EGT:$i)).
tff(mem_c_2Ebinary__ieee_2EGT,axiom,mem(c_2Ebinary__ieee_2EGT,ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_fo_c_2Ebinary__ieee_2EGT,type,(fo__c_2Ebinary__ieee_2EGT:tp__ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EGT,axiom,(inj__ty_2Ebinary__ieee_2Efloat__compare(fo__c_2Ebinary__ieee_2EGT) = c_2Ebinary__ieee_2EGT)).
tff(tp_c_2Ebinary__ieee_2EInfinity,type,(c_2Ebinary__ieee_2EInfinity:$i)).
tff(mem_c_2Ebinary__ieee_2EInfinity,axiom,mem(c_2Ebinary__ieee_2EInfinity,ty_2Ebinary__ieee_2Efloat__value)).
tff(stp_fo_c_2Ebinary__ieee_2EInfinity,type,(fo__c_2Ebinary__ieee_2EInfinity:tp__ty_2Ebinary__ieee_2Efloat__value)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EInfinity,axiom,(inj__ty_2Ebinary__ieee_2Efloat__value(fo__c_2Ebinary__ieee_2EInfinity) = c_2Ebinary__ieee_2EInfinity)).
tff(tp_c_2Ebinary__ieee_2ELT,type,(c_2Ebinary__ieee_2ELT:$i)).
tff(mem_c_2Ebinary__ieee_2ELT,axiom,mem(c_2Ebinary__ieee_2ELT,ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_fo_c_2Ebinary__ieee_2ELT,type,(fo__c_2Ebinary__ieee_2ELT:tp__ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_eq_fo_c_2Ebinary__ieee_2ELT,axiom,(inj__ty_2Ebinary__ieee_2Efloat__compare(fo__c_2Ebinary__ieee_2ELT) = c_2Ebinary__ieee_2ELT)).
tff(tp_c_2Ebinary__ieee_2ENaN,type,(c_2Ebinary__ieee_2ENaN:$i)).
tff(mem_c_2Ebinary__ieee_2ENaN,axiom,mem(c_2Ebinary__ieee_2ENaN,ty_2Ebinary__ieee_2Efloat__value)).
tff(stp_fo_c_2Ebinary__ieee_2ENaN,type,(fo__c_2Ebinary__ieee_2ENaN:tp__ty_2Ebinary__ieee_2Efloat__value)).
tff(stp_eq_fo_c_2Ebinary__ieee_2ENaN,axiom,(inj__ty_2Ebinary__ieee_2Efloat__value(fo__c_2Ebinary__ieee_2ENaN) = c_2Ebinary__ieee_2ENaN)).
tff(tp_c_2Ebinary__ieee_2EULP,type,(c_2Ebinary__ieee_2EULP:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2EULP,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2EULP(A_27t,A_27w),arr(ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27w),ty_2Ebool_2Eitself(A_27t)),ty_2Erealax_2Ereal))))).
tff(tp_c_2Ebinary__ieee_2EUN,type,(c_2Ebinary__ieee_2EUN:$i)).
tff(mem_c_2Ebinary__ieee_2EUN,axiom,mem(c_2Ebinary__ieee_2EUN,ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_fo_c_2Ebinary__ieee_2EUN,type,(fo__c_2Ebinary__ieee_2EUN:tp__ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EUN,axiom,(inj__ty_2Ebinary__ieee_2Efloat__compare(fo__c_2Ebinary__ieee_2EUN) = c_2Ebinary__ieee_2EUN)).
tff(stp_ty_2Ebinary__ieee_2Eflags,type,(tp__ty_2Ebinary__ieee_2Eflags : $tType)).
tff(stp_inj_ty_2Ebinary__ieee_2Eflags,type,(inj__ty_2Ebinary__ieee_2Eflags : tp__ty_2Ebinary__ieee_2Eflags > $i)).
tff(stp_surj_ty_2Ebinary__ieee_2Eflags,type,(surj__ty_2Ebinary__ieee_2Eflags : $i > tp__ty_2Ebinary__ieee_2Eflags)).
tff(stp_inj_surj_ty_2Ebinary__ieee_2Eflags,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Eflags] : (surj__ty_2Ebinary__ieee_2Eflags(inj__ty_2Ebinary__ieee_2Eflags(X)) = X))).
tff(stp_inj_mem_ty_2Ebinary__ieee_2Eflags,axiom,( ! [X:tp__ty_2Ebinary__ieee_2Eflags] : (mem(inj__ty_2Ebinary__ieee_2Eflags(X),ty_2Ebinary__ieee_2Eflags)))).
tff(stp_iso_mem_ty_2Ebinary__ieee_2Eflags,axiom,( ! [X:$i] : (mem(X,ty_2Ebinary__ieee_2Eflags) => (X = inj__ty_2Ebinary__ieee_2Eflags(surj__ty_2Ebinary__ieee_2Eflags(X)))))).
tff(tp_c_2Ebinary__ieee_2Echeck__for__signalling,type,(c_2Ebinary__ieee_2Echeck__for__signalling:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Echeck__for__signalling,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebinary__ieee_2Echeck__for__signalling(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Ebinary__ieee_2Efloat(A_27a,A_27b)),ty_2Ebinary__ieee_2Eflags))))).
tff(tp_c_2Ebinary__ieee_2Eclear__flags,type,(c_2Ebinary__ieee_2Eclear__flags:$i)).
tff(mem_c_2Ebinary__ieee_2Eclear__flags,axiom,mem(c_2Ebinary__ieee_2Eclear__flags,ty_2Ebinary__ieee_2Eflags)).
tff(stp_fo_c_2Ebinary__ieee_2Eclear__flags,type,(fo__c_2Ebinary__ieee_2Eclear__flags:tp__ty_2Ebinary__ieee_2Eflags)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eclear__flags,axiom,(inj__ty_2Ebinary__ieee_2Eflags(fo__c_2Ebinary__ieee_2Eclear__flags) = c_2Ebinary__ieee_2Eclear__flags)).
tff(tp_c_2Ebinary__ieee_2Eclosest,type,(c_2Ebinary__ieee_2Eclosest:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eclosest,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebinary__ieee_2Eclosest(A_27a,A_27b),arr(arr(ty_2Ebinary__ieee_2Efloat(A_27a,A_27b),bool),arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat(A_27a,A_27b))))))).
tff(tp_c_2Ebinary__ieee_2Eclosest__such,type,(c_2Ebinary__ieee_2Eclosest__such:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eclosest__such,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebinary__ieee_2Eclosest__such(A_27a,A_27b),arr(arr(ty_2Ebinary__ieee_2Efloat(A_27a,A_27b),bool),arr(arr(ty_2Ebinary__ieee_2Efloat(A_27a,A_27b),bool),arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat(A_27a,A_27b)))))))).
tff(tp_c_2Ebinary__ieee_2Edividezero__flags,type,(c_2Ebinary__ieee_2Edividezero__flags:$i)).
tff(mem_c_2Ebinary__ieee_2Edividezero__flags,axiom,mem(c_2Ebinary__ieee_2Edividezero__flags,ty_2Ebinary__ieee_2Eflags)).
tff(stp_fo_c_2Ebinary__ieee_2Edividezero__flags,type,(fo__c_2Ebinary__ieee_2Edividezero__flags:tp__ty_2Ebinary__ieee_2Eflags)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Edividezero__flags,axiom,(inj__ty_2Ebinary__ieee_2Eflags(fo__c_2Ebinary__ieee_2Edividezero__flags) = c_2Ebinary__ieee_2Edividezero__flags)).
tff(tp_c_2Ebinary__ieee_2Eexponent__boundary,type,(c_2Ebinary__ieee_2Eexponent__boundary:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eexponent__boundary,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Eexponent__boundary(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool)))))).
tff(tp_c_2Ebinary__ieee_2Eflags__CASE,type,(c_2Ebinary__ieee_2Eflags__CASE:del > $i)).
tff(mem_c_2Ebinary__ieee_2Eflags__CASE,axiom,( ! [A_27a:del] : mem(c_2Ebinary__ieee_2Eflags__CASE(A_27a),arr(ty_2Ebinary__ieee_2Eflags,arr(arr(bool,arr(bool,arr(bool,arr(bool,arr(bool,arr(bool,A_27a)))))),A_27a))))).
tff(tp_c_2Ebinary__ieee_2Eflags__DivideByZero,type,(c_2Ebinary__ieee_2Eflags__DivideByZero:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__DivideByZero,axiom,mem(c_2Ebinary__ieee_2Eflags__DivideByZero,arr(ty_2Ebinary__ieee_2Eflags,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__DivideByZero,type,(fo__c_2Ebinary__ieee_2Eflags__DivideByZero:(tp__ty_2Ebinary__ieee_2Eflags) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__DivideByZero,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__o(fo__c_2Ebinary__ieee_2Eflags__DivideByZero(X0)) = ap(c_2Ebinary__ieee_2Eflags__DivideByZero,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Eflags__DivideByZero__fupd,type,(c_2Ebinary__ieee_2Eflags__DivideByZero__fupd:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__DivideByZero__fupd,axiom,mem(c_2Ebinary__ieee_2Eflags__DivideByZero__fupd,arr(arr(bool,bool),arr(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Eflags)))).
tff(tp_c_2Ebinary__ieee_2Eflags__InvalidOp,type,(c_2Ebinary__ieee_2Eflags__InvalidOp:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__InvalidOp,axiom,mem(c_2Ebinary__ieee_2Eflags__InvalidOp,arr(ty_2Ebinary__ieee_2Eflags,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__InvalidOp,type,(fo__c_2Ebinary__ieee_2Eflags__InvalidOp:(tp__ty_2Ebinary__ieee_2Eflags) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__InvalidOp,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__o(fo__c_2Ebinary__ieee_2Eflags__InvalidOp(X0)) = ap(c_2Ebinary__ieee_2Eflags__InvalidOp,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Eflags__InvalidOp__fupd,type,(c_2Ebinary__ieee_2Eflags__InvalidOp__fupd:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__InvalidOp__fupd,axiom,mem(c_2Ebinary__ieee_2Eflags__InvalidOp__fupd,arr(arr(bool,bool),arr(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Eflags)))).
tff(tp_c_2Ebinary__ieee_2Eflags__Overflow,type,(c_2Ebinary__ieee_2Eflags__Overflow:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Overflow,axiom,mem(c_2Ebinary__ieee_2Eflags__Overflow,arr(ty_2Ebinary__ieee_2Eflags,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__Overflow,type,(fo__c_2Ebinary__ieee_2Eflags__Overflow:(tp__ty_2Ebinary__ieee_2Eflags) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__Overflow,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__o(fo__c_2Ebinary__ieee_2Eflags__Overflow(X0)) = ap(c_2Ebinary__ieee_2Eflags__Overflow,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Eflags__Overflow__fupd,type,(c_2Ebinary__ieee_2Eflags__Overflow__fupd:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Overflow__fupd,axiom,mem(c_2Ebinary__ieee_2Eflags__Overflow__fupd,arr(arr(bool,bool),arr(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Eflags)))).
tff(tp_c_2Ebinary__ieee_2Eflags__Precision,type,(c_2Ebinary__ieee_2Eflags__Precision:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Precision,axiom,mem(c_2Ebinary__ieee_2Eflags__Precision,arr(ty_2Ebinary__ieee_2Eflags,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__Precision,type,(fo__c_2Ebinary__ieee_2Eflags__Precision:(tp__ty_2Ebinary__ieee_2Eflags) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__Precision,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__o(fo__c_2Ebinary__ieee_2Eflags__Precision(X0)) = ap(c_2Ebinary__ieee_2Eflags__Precision,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Eflags__Precision__fupd,type,(c_2Ebinary__ieee_2Eflags__Precision__fupd:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Precision__fupd,axiom,mem(c_2Ebinary__ieee_2Eflags__Precision__fupd,arr(arr(bool,bool),arr(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Eflags)))).
tff(tp_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,type,(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,axiom,mem(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,arr(ty_2Ebinary__ieee_2Eflags,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,type,(fo__c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding:(tp__ty_2Ebinary__ieee_2Eflags) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__o(fo__c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding(X0)) = ap(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding__fupd,type,(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding__fupd:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding__fupd,axiom,mem(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding__fupd,arr(arr(bool,bool),arr(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Eflags)))).
tff(tp_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,type,(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,axiom,mem(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,arr(ty_2Ebinary__ieee_2Eflags,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,type,(fo__c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding:(tp__ty_2Ebinary__ieee_2Eflags) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__o(fo__c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding(X0)) = ap(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding__fupd,type,(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding__fupd:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding__fupd,axiom,mem(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding__fupd,arr(arr(bool,bool),arr(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Eflags)))).
tff(tp_c_2Ebinary__ieee_2Eflags__size,type,(c_2Ebinary__ieee_2Eflags__size:$i)).
tff(mem_c_2Ebinary__ieee_2Eflags__size,axiom,mem(c_2Ebinary__ieee_2Eflags__size,arr(ty_2Ebinary__ieee_2Eflags,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebinary__ieee_2Eflags__size,type,(fo__c_2Ebinary__ieee_2Eflags__size:(tp__ty_2Ebinary__ieee_2Eflags) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eflags__size,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Eflags] : (inj__ty_2Enum_2Enum(fo__c_2Ebinary__ieee_2Eflags__size(X0)) = ap(c_2Ebinary__ieee_2Eflags__size,inj__ty_2Ebinary__ieee_2Eflags(X0))))).
tff(tp_c_2Ebinary__ieee_2Efloat__CASE,type,(c_2Ebinary__ieee_2Efloat__CASE:(del * del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__CASE,axiom,( ! [A_27a:del] : ( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__CASE(A_27a,A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),arr(ty_2Efcp_2Ecart(bool,A_27w),arr(ty_2Efcp_2Ecart(bool,A_27t),A_27a))),A_27a))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__Exponent,type,(c_2Ebinary__ieee_2Efloat__Exponent:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__Exponent,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Efcp_2Ecart(bool,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__Exponent__fupd,type,(c_2Ebinary__ieee_2Efloat__Exponent__fupd:(del * del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__Exponent__fupd,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : ( ! [A_27x:del] : mem(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),arr(arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x)),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__Sign,type,(c_2Ebinary__ieee_2Efloat__Sign:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__Sign,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__Sign__fupd,type,(c_2Ebinary__ieee_2Efloat__Sign__fupd:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__Sign__fupd,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),arr(arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__Significand,type,(c_2Ebinary__ieee_2Efloat__Significand:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__Significand,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Efcp_2Ecart(bool,A_27t)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__Significand__fupd,type,(c_2Ebinary__ieee_2Efloat__Significand__fupd:(del * del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__Significand__fupd,axiom,( ! [A_27t:del] : ( ! [A_27u:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),arr(arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u)),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__abs,type,(c_2Ebinary__ieee_2Efloat__abs:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__abs,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__abs(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__add,type,(c_2Ebinary__ieee_2Efloat__add:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__add,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__add(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__bottom,type,(c_2Ebinary__ieee_2Efloat__bottom:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__bottom,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__bottom(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__compare,type,(c_2Ebinary__ieee_2Efloat__compare:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__compare,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__compare(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat__compare)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__compare2num,type,(c_2Ebinary__ieee_2Efloat__compare2num:$i)).
tff(mem_c_2Ebinary__ieee_2Efloat__compare2num,axiom,mem(c_2Ebinary__ieee_2Efloat__compare2num,arr(ty_2Ebinary__ieee_2Efloat__compare,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebinary__ieee_2Efloat__compare2num,type,(fo__c_2Ebinary__ieee_2Efloat__compare2num:(tp__ty_2Ebinary__ieee_2Efloat__compare) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Efloat__compare2num,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Efloat__compare] : (inj__ty_2Enum_2Enum(fo__c_2Ebinary__ieee_2Efloat__compare2num(X0)) = ap(c_2Ebinary__ieee_2Efloat__compare2num,inj__ty_2Ebinary__ieee_2Efloat__compare(X0))))).
tff(tp_c_2Ebinary__ieee_2Efloat__compare__CASE,type,(c_2Ebinary__ieee_2Efloat__compare__CASE:del > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__compare__CASE,axiom,( ! [A_27a:del] : mem(c_2Ebinary__ieee_2Efloat__compare__CASE(A_27a),arr(ty_2Ebinary__ieee_2Efloat__compare,arr(A_27a,arr(A_27a,arr(A_27a,arr(A_27a,A_27a)))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__compare__size,type,(c_2Ebinary__ieee_2Efloat__compare__size:$i)).
tff(mem_c_2Ebinary__ieee_2Efloat__compare__size,axiom,mem(c_2Ebinary__ieee_2Efloat__compare__size,arr(ty_2Ebinary__ieee_2Efloat__compare,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebinary__ieee_2Efloat__compare__size,type,(fo__c_2Ebinary__ieee_2Efloat__compare__size:(tp__ty_2Ebinary__ieee_2Efloat__compare) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Efloat__compare__size,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Efloat__compare] : (inj__ty_2Enum_2Enum(fo__c_2Ebinary__ieee_2Efloat__compare__size(X0)) = ap(c_2Ebinary__ieee_2Efloat__compare__size,inj__ty_2Ebinary__ieee_2Efloat__compare(X0))))).
tff(tp_c_2Ebinary__ieee_2Efloat__div,type,(c_2Ebinary__ieee_2Efloat__div:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__div,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__div(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__equal,type,(c_2Ebinary__ieee_2Efloat__equal:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__equal,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__equal(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__greater__equal,type,(c_2Ebinary__ieee_2Efloat__greater__equal:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__greater__equal,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__greater__equal(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__greater__than,type,(c_2Ebinary__ieee_2Efloat__greater__than:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__greater__than,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__greater__than(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__finite,type,(c_2Ebinary__ieee_2Efloat__is__finite:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__finite,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__finite(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__infinite,type,(c_2Ebinary__ieee_2Efloat__is__infinite:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__infinite,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__infinite(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__integral,type,(c_2Ebinary__ieee_2Efloat__is__integral:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__integral,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__integral(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__nan,type,(c_2Ebinary__ieee_2Efloat__is__nan:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__nan,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__nan(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__normal,type,(c_2Ebinary__ieee_2Efloat__is__normal:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__normal,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__normal(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__signalling,type,(c_2Ebinary__ieee_2Efloat__is__signalling:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__signalling,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__signalling(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__subnormal,type,(c_2Ebinary__ieee_2Efloat__is__subnormal:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__subnormal,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__subnormal(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__is__zero,type,(c_2Ebinary__ieee_2Efloat__is__zero:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__is__zero,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__is__zero(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool))))).
tff(tp_c_2Ebinary__ieee_2Efloat__less__equal,type,(c_2Ebinary__ieee_2Efloat__less__equal:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__less__equal,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__less__equal(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__less__than,type,(c_2Ebinary__ieee_2Efloat__less__than:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__less__than,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__less__than(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),bool)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__minus__infinity,type,(c_2Ebinary__ieee_2Efloat__minus__infinity:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__minus__infinity,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__minus__infinity(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__minus__min,type,(c_2Ebinary__ieee_2Efloat__minus__min:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__minus__min,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__minus__min(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__minus__zero,type,(c_2Ebinary__ieee_2Efloat__minus__zero:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__minus__zero,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__minus__zero(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__mul,type,(c_2Ebinary__ieee_2Efloat__mul:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__mul,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__mul(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__mul__add,type,(c_2Ebinary__ieee_2Efloat__mul__add:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__mul__add,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__mul__add(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__mul__sub,type,(c_2Ebinary__ieee_2Efloat__mul__sub:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__mul__sub,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__mul__sub(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__negate,type,(c_2Ebinary__ieee_2Efloat__negate:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__negate,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__negate(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__plus__infinity,type,(c_2Ebinary__ieee_2Efloat__plus__infinity:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__plus__infinity,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__plus__infinity(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__plus__min,type,(c_2Ebinary__ieee_2Efloat__plus__min:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__plus__min,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__plus__zero,type,(c_2Ebinary__ieee_2Efloat__plus__zero:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__plus__zero,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__plus__zero(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__round,type,(c_2Ebinary__ieee_2Efloat__round:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__round,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__round(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(bool,arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__round__to__integral,type,(c_2Ebinary__ieee_2Efloat__round__to__integral:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__round__to__integral,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__round__to__integral(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__round__with__flags,type,(c_2Ebinary__ieee_2Efloat__round__with__flags:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__round__with__flags,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__round__with__flags(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(bool,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__size,type,(c_2Ebinary__ieee_2Efloat__size:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__size,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__size(A_27t,A_27w),arr(arr(A_27t,ty_2Enum_2Enum),arr(arr(A_27w,ty_2Enum_2Enum),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Enum_2Enum))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__some__qnan,type,(c_2Ebinary__ieee_2Efloat__some__qnan:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__some__qnan,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__some__qnan(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__sqrt,type,(c_2Ebinary__ieee_2Efloat__sqrt:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__sqrt,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__sqrt(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__sub,type,(c_2Ebinary__ieee_2Efloat__sub:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__sub,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__sub(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))).
tff(stp_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,type,(tp__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint : $tType)).
tff(stp_inj_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,type,(inj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint : tp__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint > $i)).
tff(stp_surj_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,type,(surj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint : $i > tp__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint)).
tff(stp_inj_surj_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint] : (surj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint(inj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint(X)) = X))).
tff(stp_inj_mem_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint] : (mem(inj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint(X),ty_2Eoption_2Eoption(ty_2Einteger_2Eint))))).
tff(stp_iso_mem_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,axiom,( ! [X:$i] : (mem(X,ty_2Eoption_2Eoption(ty_2Einteger_2Eint)) => (X = inj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint(surj__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint(X)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__to__int,type,(c_2Ebinary__ieee_2Efloat__to__int:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__to__int,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__to__int(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Eoption_2Eoption(ty_2Einteger_2Eint))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__to__real,type,(c_2Ebinary__ieee_2Efloat__to__real:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__to__real,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__to__real(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Erealax_2Ereal))))).
tff(tp_c_2Ebinary__ieee_2Efloat__top,type,(c_2Ebinary__ieee_2Efloat__top:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__top,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__top(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))).
tff(tp_c_2Ebinary__ieee_2Efloat__value,type,(c_2Ebinary__ieee_2Efloat__value:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__value,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efloat__value(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat__value))))).
tff(tp_c_2Ebinary__ieee_2Efloat__value__CASE,type,(c_2Ebinary__ieee_2Efloat__value__CASE:del > $i)).
tff(mem_c_2Ebinary__ieee_2Efloat__value__CASE,axiom,( ! [A_27a:del] : mem(c_2Ebinary__ieee_2Efloat__value__CASE(A_27a),arr(ty_2Ebinary__ieee_2Efloat__value,arr(arr(ty_2Erealax_2Ereal,A_27a),arr(A_27a,arr(A_27a,A_27a))))))).
tff(tp_c_2Ebinary__ieee_2Efloat__value__size,type,(c_2Ebinary__ieee_2Efloat__value__size:$i)).
tff(mem_c_2Ebinary__ieee_2Efloat__value__size,axiom,mem(c_2Ebinary__ieee_2Efloat__value__size,arr(ty_2Ebinary__ieee_2Efloat__value,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebinary__ieee_2Efloat__value__size,type,(fo__c_2Ebinary__ieee_2Efloat__value__size:(tp__ty_2Ebinary__ieee_2Efloat__value) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Efloat__value__size,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Efloat__value] : (inj__ty_2Enum_2Enum(fo__c_2Ebinary__ieee_2Efloat__value__size(X0)) = ap(c_2Ebinary__ieee_2Efloat__value__size,inj__ty_2Ebinary__ieee_2Efloat__value(X0))))).
tff(tp_c_2Ebinary__ieee_2Efp__op__CASE,type,(c_2Ebinary__ieee_2Efp__op__CASE:(del * del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efp__op__CASE,axiom,( ! [A_27a:del] : ( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efp__op__CASE(A_27a,A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a)),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a))),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a))),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a))),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a))),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a)))),arr(arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),A_27a)))),A_27a))))))))))))).
tff(tp_c_2Ebinary__ieee_2Efp__op__size,type,(c_2Ebinary__ieee_2Efp__op__size:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Efp__op__size,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Efp__op__size(A_27t,A_27w),arr(arr(A_27t,ty_2Enum_2Enum),arr(arr(A_27w,ty_2Enum_2Enum),arr(ty_2Ebinary__ieee_2Efp__op(A_27t,A_27w),ty_2Enum_2Enum))))))).
tff(tp_c_2Ebinary__ieee_2Eintegral__round,type,(c_2Ebinary__ieee_2Eintegral__round:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eintegral__round,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Eintegral__round(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))).
tff(tp_c_2Ebinary__ieee_2Einvalidop__flags,type,(c_2Ebinary__ieee_2Einvalidop__flags:$i)).
tff(mem_c_2Ebinary__ieee_2Einvalidop__flags,axiom,mem(c_2Ebinary__ieee_2Einvalidop__flags,ty_2Ebinary__ieee_2Eflags)).
tff(stp_fo_c_2Ebinary__ieee_2Einvalidop__flags,type,(fo__c_2Ebinary__ieee_2Einvalidop__flags:tp__ty_2Ebinary__ieee_2Eflags)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Einvalidop__flags,axiom,(inj__ty_2Ebinary__ieee_2Eflags(fo__c_2Ebinary__ieee_2Einvalidop__flags) = c_2Ebinary__ieee_2Einvalidop__flags)).
tff(tp_c_2Ebinary__ieee_2Eis__closest,type,(c_2Ebinary__ieee_2Eis__closest:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eis__closest,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebinary__ieee_2Eis__closest(A_27a,A_27b),arr(arr(ty_2Ebinary__ieee_2Efloat(A_27a,A_27b),bool),arr(ty_2Erealax_2Ereal,arr(ty_2Ebinary__ieee_2Efloat(A_27a,A_27b),bool))))))).
tff(tp_c_2Ebinary__ieee_2Eis__integral,type,(c_2Ebinary__ieee_2Eis__integral:$i)).
tff(mem_c_2Ebinary__ieee_2Eis__integral,axiom,mem(c_2Ebinary__ieee_2Eis__integral,arr(ty_2Erealax_2Ereal,bool))).
tff(stp_fo_c_2Ebinary__ieee_2Eis__integral,type,(fo__c_2Ebinary__ieee_2Eis__integral:(tp__ty_2Erealax_2Ereal) > tp__o)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Eis__integral,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__o(fo__c_2Ebinary__ieee_2Eis__integral(X0)) = ap(c_2Ebinary__ieee_2Eis__integral,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Ebinary__ieee_2Elargest,type,(c_2Ebinary__ieee_2Elargest:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Elargest,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Elargest(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Erealax_2Ereal))))).
tff(tp_c_2Ebinary__ieee_2Enum2float__compare,type,(c_2Ebinary__ieee_2Enum2float__compare:$i)).
tff(mem_c_2Ebinary__ieee_2Enum2float__compare,axiom,mem(c_2Ebinary__ieee_2Enum2float__compare,arr(ty_2Enum_2Enum,ty_2Ebinary__ieee_2Efloat__compare))).
tff(stp_fo_c_2Ebinary__ieee_2Enum2float__compare,type,(fo__c_2Ebinary__ieee_2Enum2float__compare:(tp__ty_2Enum_2Enum) > tp__ty_2Ebinary__ieee_2Efloat__compare)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Enum2float__compare,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Ebinary__ieee_2Efloat__compare(fo__c_2Ebinary__ieee_2Enum2float__compare(X0)) = ap(c_2Ebinary__ieee_2Enum2float__compare,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebinary__ieee_2Enum2rounding,type,(c_2Ebinary__ieee_2Enum2rounding:$i)).
tff(mem_c_2Ebinary__ieee_2Enum2rounding,axiom,mem(c_2Ebinary__ieee_2Enum2rounding,arr(ty_2Enum_2Enum,ty_2Ebinary__ieee_2Erounding))).
tff(stp_fo_c_2Ebinary__ieee_2Enum2rounding,type,(fo__c_2Ebinary__ieee_2Enum2rounding:(tp__ty_2Enum_2Enum) > tp__ty_2Ebinary__ieee_2Erounding)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Enum2rounding,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Ebinary__ieee_2Erounding(fo__c_2Ebinary__ieee_2Enum2rounding(X0)) = ap(c_2Ebinary__ieee_2Enum2rounding,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebinary__ieee_2Ereal__to__float,type,(c_2Ebinary__ieee_2Ereal__to__float:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Ereal__to__float,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebinary__ieee_2Ereal__to__float(A_27a,A_27b),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat(A_27a,A_27b))))))).
tff(tp_c_2Ebinary__ieee_2Ereal__to__float__with__flags,type,(c_2Ebinary__ieee_2Ereal__to__float__with__flags:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Ereal__to__float__with__flags,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ebinary__ieee_2Ereal__to__float__with__flags(A_27a,A_27b),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Ebinary__ieee_2Eflags,ty_2Ebinary__ieee_2Efloat(A_27a,A_27b)))))))).
tff(tp_c_2Ebinary__ieee_2Erecordtype_2Eflags,type,(c_2Ebinary__ieee_2Erecordtype_2Eflags:$i)).
tff(mem_c_2Ebinary__ieee_2Erecordtype_2Eflags,axiom,mem(c_2Ebinary__ieee_2Erecordtype_2Eflags,arr(bool,arr(bool,arr(bool,arr(bool,arr(bool,arr(bool,ty_2Ebinary__ieee_2Eflags)))))))).
tff(stp_fo_c_2Ebinary__ieee_2Erecordtype_2Eflags,type,(fo__c_2Ebinary__ieee_2Erecordtype_2Eflags:(tp__o * tp__o * tp__o * tp__o * tp__o * tp__o) > tp__ty_2Ebinary__ieee_2Eflags)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Erecordtype_2Eflags,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : ( ! [X2:tp__o] : ( ! [X3:tp__o] : ( ! [X4:tp__o] : ( ! [X5:tp__o] : (inj__ty_2Ebinary__ieee_2Eflags(fo__c_2Ebinary__ieee_2Erecordtype_2Eflags(X0,X1,X2,X3,X4,X5)) = ap(ap(ap(ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Eflags,inj__o(X0)),inj__o(X1)),inj__o(X2)),inj__o(X3)),inj__o(X4)),inj__o(X5)))))))))).
tff(tp_c_2Ebinary__ieee_2Erecordtype_2Efloat,type,(c_2Ebinary__ieee_2Erecordtype_2Efloat:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Erecordtype_2Efloat,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),arr(ty_2Efcp_2Ecart(bool,A_27w),arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)))))))).
tff(tp_c_2Ebinary__ieee_2Eround,type,(c_2Ebinary__ieee_2Eround:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eround,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Eround(A_27t,A_27w),arr(ty_2Ebinary__ieee_2Erounding,arr(ty_2Erealax_2Ereal,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))).
tff(tp_c_2Ebinary__ieee_2EroundTiesToEven,type,(c_2Ebinary__ieee_2EroundTiesToEven:$i)).
tff(mem_c_2Ebinary__ieee_2EroundTiesToEven,axiom,mem(c_2Ebinary__ieee_2EroundTiesToEven,ty_2Ebinary__ieee_2Erounding)).
tff(stp_fo_c_2Ebinary__ieee_2EroundTiesToEven,type,(fo__c_2Ebinary__ieee_2EroundTiesToEven:tp__ty_2Ebinary__ieee_2Erounding)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EroundTiesToEven,axiom,(inj__ty_2Ebinary__ieee_2Erounding(fo__c_2Ebinary__ieee_2EroundTiesToEven) = c_2Ebinary__ieee_2EroundTiesToEven)).
tff(tp_c_2Ebinary__ieee_2EroundTowardNegative,type,(c_2Ebinary__ieee_2EroundTowardNegative:$i)).
tff(mem_c_2Ebinary__ieee_2EroundTowardNegative,axiom,mem(c_2Ebinary__ieee_2EroundTowardNegative,ty_2Ebinary__ieee_2Erounding)).
tff(stp_fo_c_2Ebinary__ieee_2EroundTowardNegative,type,(fo__c_2Ebinary__ieee_2EroundTowardNegative:tp__ty_2Ebinary__ieee_2Erounding)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EroundTowardNegative,axiom,(inj__ty_2Ebinary__ieee_2Erounding(fo__c_2Ebinary__ieee_2EroundTowardNegative) = c_2Ebinary__ieee_2EroundTowardNegative)).
tff(tp_c_2Ebinary__ieee_2EroundTowardPositive,type,(c_2Ebinary__ieee_2EroundTowardPositive:$i)).
tff(mem_c_2Ebinary__ieee_2EroundTowardPositive,axiom,mem(c_2Ebinary__ieee_2EroundTowardPositive,ty_2Ebinary__ieee_2Erounding)).
tff(stp_fo_c_2Ebinary__ieee_2EroundTowardPositive,type,(fo__c_2Ebinary__ieee_2EroundTowardPositive:tp__ty_2Ebinary__ieee_2Erounding)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EroundTowardPositive,axiom,(inj__ty_2Ebinary__ieee_2Erounding(fo__c_2Ebinary__ieee_2EroundTowardPositive) = c_2Ebinary__ieee_2EroundTowardPositive)).
tff(tp_c_2Ebinary__ieee_2EroundTowardZero,type,(c_2Ebinary__ieee_2EroundTowardZero:$i)).
tff(mem_c_2Ebinary__ieee_2EroundTowardZero,axiom,mem(c_2Ebinary__ieee_2EroundTowardZero,ty_2Ebinary__ieee_2Erounding)).
tff(stp_fo_c_2Ebinary__ieee_2EroundTowardZero,type,(fo__c_2Ebinary__ieee_2EroundTowardZero:tp__ty_2Ebinary__ieee_2Erounding)).
tff(stp_eq_fo_c_2Ebinary__ieee_2EroundTowardZero,axiom,(inj__ty_2Ebinary__ieee_2Erounding(fo__c_2Ebinary__ieee_2EroundTowardZero) = c_2Ebinary__ieee_2EroundTowardZero)).
tff(tp_c_2Ebinary__ieee_2Erounding2num,type,(c_2Ebinary__ieee_2Erounding2num:$i)).
tff(mem_c_2Ebinary__ieee_2Erounding2num,axiom,mem(c_2Ebinary__ieee_2Erounding2num,arr(ty_2Ebinary__ieee_2Erounding,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebinary__ieee_2Erounding2num,type,(fo__c_2Ebinary__ieee_2Erounding2num:(tp__ty_2Ebinary__ieee_2Erounding) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Erounding2num,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Erounding] : (inj__ty_2Enum_2Enum(fo__c_2Ebinary__ieee_2Erounding2num(X0)) = ap(c_2Ebinary__ieee_2Erounding2num,inj__ty_2Ebinary__ieee_2Erounding(X0))))).
tff(tp_c_2Ebinary__ieee_2Erounding__CASE,type,(c_2Ebinary__ieee_2Erounding__CASE:del > $i)).
tff(mem_c_2Ebinary__ieee_2Erounding__CASE,axiom,( ! [A_27a:del] : mem(c_2Ebinary__ieee_2Erounding__CASE(A_27a),arr(ty_2Ebinary__ieee_2Erounding,arr(A_27a,arr(A_27a,arr(A_27a,arr(A_27a,A_27a)))))))).
tff(tp_c_2Ebinary__ieee_2Erounding__size,type,(c_2Ebinary__ieee_2Erounding__size:$i)).
tff(mem_c_2Ebinary__ieee_2Erounding__size,axiom,mem(c_2Ebinary__ieee_2Erounding__size,arr(ty_2Ebinary__ieee_2Erounding,ty_2Enum_2Enum))).
tff(stp_fo_c_2Ebinary__ieee_2Erounding__size,type,(fo__c_2Ebinary__ieee_2Erounding__size:(tp__ty_2Ebinary__ieee_2Erounding) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Ebinary__ieee_2Erounding__size,axiom,( ! [X0:tp__ty_2Ebinary__ieee_2Erounding] : (inj__ty_2Enum_2Enum(fo__c_2Ebinary__ieee_2Erounding__size(X0)) = ap(c_2Ebinary__ieee_2Erounding__size,inj__ty_2Ebinary__ieee_2Erounding(X0))))).
tff(tp_c_2Ebinary__ieee_2Ethreshold,type,(c_2Ebinary__ieee_2Ethreshold:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Ethreshold,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Ethreshold(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Erealax_2Ereal))))).
tff(tp_c_2Ebinary__ieee_2Eulp,type,(c_2Ebinary__ieee_2Eulp:(del * del) > $i)).
tff(mem_c_2Ebinary__ieee_2Eulp,axiom,( ! [A_27t:del] : ( ! [A_27w:del] : mem(c_2Ebinary__ieee_2Eulp(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Erealax_2Ereal))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__TY__DEF,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: (? [V0rep:$i] : (mem(V0rep,arr(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Eind__type_2Erecspace(ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27t)))))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27t)))),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),f3012(A_27w,A_27t)),V0rep))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__case__def,axiom,( ! [A_27a:del]: ( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0a0:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V1a1:$i] : (mem(V1a1,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V2a2:$i] : (mem(V2a2,ty_2Efcp_2Ecart(bool,A_27t)) => ( ! [V3f:$i] : (mem(V3f,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),arr(ty_2Efcp_2Ecart(bool,A_27w),arr(ty_2Efcp_2Ecart(bool,A_27t),A_27a)))) => (ap(ap(c_2Ebinary__ieee_2Efloat__CASE(A_27a,A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V0a0)),V1a1),V2a2)),V3f) = ap(ap(ap(V3f,inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V0a0)),V1a1),V2a2))))))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__size__def,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27t,ty_2Enum_2Enum)) => ( ! [V1f1:$i] : (mem(V1f1,arr(A_27w,ty_2Enum_2Enum)) => ( ! [V2a0:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V3a1:$i] : (mem(V3a1,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V4a2:$i] : (mem(V4a2,ty_2Efcp_2Ecart(bool,A_27t)) => (surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebinary__ieee_2Efloat__size(A_27t,A_27w),V0f),V1f1),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V2a0)),V3a1),V4a2))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__Sign,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V1c0:$i] : (mem(V1c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V2c1:$i] : (mem(V2c1,ty_2Efcp_2Ecart(bool,A_27t)) => (surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V0c)),V1c0),V2c1))) = V0c))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__Exponent,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V1c0:$i] : (mem(V1c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V2c1:$i] : (mem(V2c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V0c)),V1c0),V2c1)) = V1c0))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__Significand,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V1c0:$i] : (mem(V1c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V2c1:$i] : (mem(V2c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V0c)),V1c0),V2c1)) = V2c1))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__accessors,lemma,(( ! [A_27t:del]: ( ! [A_27w:del]: (( ! [V0c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V1c0:$i] : (mem(V1c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V2c1:$i] : (mem(V2c1,ty_2Efcp_2Ecart(bool,A_27t)) => (surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V0c)),V1c0),V2c1))) = V0c)))))) & (( ! [V3c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V4c0:$i] : (mem(V4c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V5c1:$i] : (mem(V5c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V3c)),V4c0),V5c1)) = V4c0)))))) & ( ! [V6c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V7c0:$i] : (mem(V7c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V8c1:$i] : (mem(V8c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V6c)),V7c0),V8c1)) = V8c1)))))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__Sign__fupd,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V1c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V2c0:$i] : (mem(V2c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V3c1:$i] : (mem(V3c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V0f),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c)),V2c0),V3c1)) = ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),ap(V0f,inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c))),V2c0),V3c1)))))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__Exponent__fupd,axiom,( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V1c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V2c0:$i] : (mem(V2c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V3c1:$i] : (mem(V3c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V0f),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c)),V2c0),V3c1)) = ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27x),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c)),ap(V0f,V2c0)),V3c1))))))))))))).
tff(ax_thm_2Ebinary__ieee_2Efloat__Significand__fupd,axiom,( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V1c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V2c0:$i] : (mem(V2c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V3c1:$i] : (mem(V3c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V0f),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c)),V2c0),V3c1)) = ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27u,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c)),V2c0),ap(V0f,V3c1)))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__fn__updates,lemma,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: (( ! [V0f:$i] : (mem(V0f,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V1c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V2c0:$i] : (mem(V2c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V3c1:$i] : (mem(V3c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V0f),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c)),V2c0),V3c1)) = ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),ap(V0f,inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c))),V2c0),V3c1))))))))) & (( ! [V4f:$i] : (mem(V4f,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V5c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V6c0:$i] : (mem(V6c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V7c1:$i] : (mem(V7c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V4f),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V5c)),V6c0),V7c1)) = ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27x),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V5c)),ap(V4f,V6c0)),V7c1))))))))) & ( ! [V8f:$i] : (mem(V8f,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V9c:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V10c0:$i] : (mem(V10c0,ty_2Efcp_2Ecart(bool,A_27w)) => ( ! [V11c1:$i] : (mem(V11c1,ty_2Efcp_2Ecart(bool,A_27t)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V8f),ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27t,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V9c)),V10c0),V11c1)) = ap(ap(ap(c_2Ebinary__ieee_2Erecordtype_2Efloat(A_27u,A_27w),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V9c)),V10c0),ap(V8f,V11c1)))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__accfupds,lemma,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: (( ! [V0f0:$i] : (mem(V0f0,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V1f:$i] : (mem(V1f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27x),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V0f0),V1f))) = surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),V1f))))))) & (( ! [V2f0:$i] : (mem(V2f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V3f:$i] : (mem(V3f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27u,A_27w),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V2f0),V3f))) = surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),V3f))))))) & (( ! [V4f0:$i] : (mem(V4f0,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V5f:$i] : (mem(V5f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V4f0),V5f)) = ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),V5f)))))) & (( ! [V6f0:$i] : (mem(V6f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V7f:$i] : (mem(V7f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27u,A_27w),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V6f0),V7f)) = ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),V7f)))))) & (( ! [V8f0:$i] : (mem(V8f0,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V9f:$i] : (mem(V9f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V8f0),V9f)) = ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),V9f)))))) & (( ! [V10f0:$i] : (mem(V10f0,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V11f:$i] : (mem(V11f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27x),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V10f0),V11f)) = ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),V11f)))))) & (( ! [V12f0:$i] : (mem(V12f0,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V13f:$i] : (mem(V13f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V12f0),V13f))) = surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(V12f0,ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),V13f)))))))) & (( ! [V14f0:$i] : (mem(V14f0,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V15f:$i] : (mem(V15f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27x),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V14f0),V15f)) = ap(V14f0,ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),V15f))))))) & ( ! [V16f0:$i] : (mem(V16f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V17f:$i] : (mem(V17f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(c_2Ebinary__ieee_2Efloat__Significand(A_27u,A_27w),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V16f0),V17f)) = ap(V16f0,ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),V17f))))))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__fupdfupds,lemma,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27v:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [A_27y:del]: (( ! [V0g:$i] : (mem(V0g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V1f0:$i] : (mem(V1f0,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V2f:$i] : (mem(V2f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V1f0),ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V0g),V2f)) = ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),V1f0),V0g)),V2f)))))))) & (( ! [V3g:$i] : (mem(V3g,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V4f0:$i] : (mem(V4f0,arr(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27y))) => ( ! [V5f:$i] : (mem(V5f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27x,A_27y),V4f0),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V3g),V5f)) = ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27y),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27y),ty_2Efcp_2Ecart(bool,A_27x)),V4f0),V3g)),V5f)))))))) & ( ! [V6g:$i] : (mem(V6g,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V7f0:$i] : (mem(V7f0,arr(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27v))) => ( ! [V8f:$i] : (mem(V8f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27u,A_27v,A_27w),V7f0),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V6g),V8f)) = ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27v,A_27w),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27v),ty_2Efcp_2Ecart(bool,A_27u)),V7f0),V6g)),V8f)))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__fupdfupds__comp,lemma,(( ! [A_27a:del]: ( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27v:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [A_27y:del]: ((( ! [V0g:$i] : (mem(V0g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V1f0:$i] : (mem(V1f0,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => (ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V1f0)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V0g)) = ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),V1f0),V0g))))))) & ( ! [V2h:$i] : (mem(V2h,arr(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) => ( ! [V3g:$i] : (mem(V3g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V4f0:$i] : (mem(V4f0,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => (ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V4f0)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V3g)),V2h)) = ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),V4f0),V3g))),V2h))))))))) & ((( ! [V5g:$i] : (mem(V5g,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V6f0:$i] : (mem(V6f0,arr(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27y))) => (ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27y),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27x,A_27y),V6f0)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V5g)) = ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27y),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27y),ty_2Efcp_2Ecart(bool,A_27x)),V6f0),V5g))))))) & ( ! [V7h:$i] : (mem(V7h,arr(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) => ( ! [V8g:$i] : (mem(V8g,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V9f0:$i] : (mem(V9f0,arr(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27y))) => (ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27y),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27x,A_27y),V9f0)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V8g)),V7h)) = ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27y),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27y),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27y),ty_2Efcp_2Ecart(bool,A_27x)),V9f0),V8g))),V7h))))))))) & (( ! [V10g:$i] : (mem(V10g,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V11f0:$i] : (mem(V11f0,arr(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27v))) => (ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27v,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27u,A_27v,A_27w),V11f0)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V10g)) = ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27v,A_27w),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27v),ty_2Efcp_2Ecart(bool,A_27u)),V11f0),V10g))))))) & ( ! [V12h:$i] : (mem(V12h,arr(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) => ( ! [V13g:$i] : (mem(V13g,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V14f0:$i] : (mem(V14f0,arr(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27v))) => (ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27v,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27u,A_27v,A_27w),V14f0)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V13g)),V12h)) = ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27v,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27v,A_27w),ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27v),ty_2Efcp_2Ecart(bool,A_27u)),V14f0),V13g))),V12h)))))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__fupdcanon,lemma,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: (( ! [V0g:$i] : (mem(V0g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V1f0:$i] : (mem(V1f0,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V2f:$i] : (mem(V2f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V1f0),ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V0g),V2f)) = ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27x),V0g),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V1f0),V2f))))))))) & (( ! [V3g:$i] : (mem(V3g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V4f0:$i] : (mem(V4f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V5f:$i] : (mem(V5f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V4f0),ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V3g),V5f)) = ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27w),V3g),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V4f0),V5f))))))))) & ( ! [V6g:$i] : (mem(V6g,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V7f0:$i] : (mem(V7f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => ( ! [V8f:$i] : (mem(V8f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27x),V7f0),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V6g),V8f)) = ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),V6g),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V7f0),V8f))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__fupdcanon__comp,lemma,(( ! [A_27a:del]: ( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ((( ! [V0g:$i] : (mem(V0g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V1f0:$i] : (mem(V1f0,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => (ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V1f0)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V0g)) = ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27x),V0g)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V1f0))))))) & ( ! [V2h:$i] : (mem(V2h,arr(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) => ( ! [V3g:$i] : (mem(V3g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V4f0:$i] : (mem(V4f0,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => (ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V4f0)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V3g)),V2h)) = ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27x),V3g)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V4f0)),V2h)))))))))) & ((( ! [V5g:$i] : (mem(V5g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V6f0:$i] : (mem(V6f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => (ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V6f0)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V5g)) = ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27w),V5g)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V6f0))))))) & ( ! [V7h:$i] : (mem(V7h,arr(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) => ( ! [V8g:$i] : (mem(V8g,arr(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) => ( ! [V9f0:$i] : (mem(V9f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => (ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V9f0)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27t,A_27w),V8g)),V7h)) = ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27w),V8g)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V9f0)),V7h)))))))))) & (( ! [V10g:$i] : (mem(V10g,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V11f0:$i] : (mem(V11f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => (ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27x),V11f0)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V10g)) = ap(ap(c_2Ecombin_2Eo(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w),ty_2Ebinary__ieee_2Efloat(A_27u,A_27x),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),V10g)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V11f0))))))) & ( ! [V12h:$i] : (mem(V12h,arr(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) => ( ! [V13g:$i] : (mem(V13g,arr(ty_2Efcp_2Ecart(bool,A_27w),ty_2Efcp_2Ecart(bool,A_27x))) => ( ! [V14f0:$i] : (mem(V14f0,arr(ty_2Efcp_2Ecart(bool,A_27t),ty_2Efcp_2Ecart(bool,A_27u))) => (ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27x)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27x),V14f0)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27t,A_27x),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27t,A_27w,A_27x),V13g)),V12h)) = ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27x),ty_2Ebinary__ieee_2Efloat(A_27u,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),V13g)),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Ebinary__ieee_2Efloat(A_27u,A_27w),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)),ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),V14f0)),V12h))))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__component__equality,lemma,(( ! [A_27t:del]: ( ! [A_27w:del]: ( ! [V0f1:$i] : (mem(V0f1,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => ( ! [V1f2:$i] : (mem(V1f2,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => ((V0f1 = V1f2) <=> ((surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),V0f1)) = surj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(ap(c_2Ebinary__ieee_2Efloat__Sign(A_27t,A_27w),V1f2))) & ((ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),V0f1) = ap(c_2Ebinary__ieee_2Efloat__Exponent(A_27t,A_27w),V1f2)) & (ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),V0f1) = ap(c_2Ebinary__ieee_2Efloat__Significand(A_27t,A_27w),V1f2))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__updates__eq__literal,lemma,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Ebinary__ieee_2Efloat(A_27t,A_27w)) => ( ! [V1c1:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V2c0:$i] : (mem(V2c0,ty_2Efcp_2Ecart(bool,A_27x)) => ( ! [V3c:$i] : (mem(V3c,ty_2Efcp_2Ecart(bool,A_27u)) => (ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c1))),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27w)),V2c0)),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27t)),V3c)),V0f))) = ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c1))),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27w)),V2c0)),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27t)),V3c)),c_2Ebool_2EARB(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2Efloat__literal__nchotomy,lemma,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [V0f:$i] : (mem(V0f,ty_2Ebinary__ieee_2Efloat(A_27u,A_27x)) => (? [V1c1:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : (? [V2c0:$i] : (mem(V2c0,ty_2Efcp_2Ecart(bool,A_27x)) & (? [V3c:$i] : (mem(V3c,ty_2Efcp_2Ecart(bool,A_27u)) & (V0f = ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V1c1))),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27w)),V2c0)),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27t)),V3c)),c_2Ebool_2EARB(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))))))))))))).
tff(conj_thm_2Ebinary__ieee_2EFORALL__float,conjecture,(( ! [A_27t:del]: ( ! [A_27u:del]: ( ! [A_27w:del]: ( ! [A_27x:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Ebinary__ieee_2Efloat(A_27u,A_27x),bool)) => (( ! [V1f:$i] : (mem(V1f,ty_2Ebinary__ieee_2Efloat(A_27u,A_27x)) => p(ap(V0P,V1f)))) <=> ( ! [V2c1:tp__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone] : ( ! [V3c0:$i] : (mem(V3c0,ty_2Efcp_2Ecart(bool,A_27x)) => ( ! [V4c:$i] : (mem(V4c,ty_2Efcp_2Ecart(bool,A_27u)) => p(ap(V0P,ap(ap(c_2Ebinary__ieee_2Efloat__Sign__fupd(A_27u,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),inj__c_ty_2Efcp_2Ecart_o_ty_2Eone_2Eone(V2c1))),ap(ap(c_2Ebinary__ieee_2Efloat__Exponent__fupd(A_27u,A_27w,A_27x),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27x),ty_2Efcp_2Ecart(bool,A_27w)),V3c0)),ap(ap(c_2Ebinary__ieee_2Efloat__Significand__fupd(A_27t,A_27u,A_27w),ap(c_2Ecombin_2EK(ty_2Efcp_2Ecart(bool,A_27u),ty_2Efcp_2Ecart(bool,A_27t)),V4c)),c_2Ebool_2EARB(ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))))))))))))))))))))).
