include('Axioms/transc^2.ax').
thf(tp_ty_2Ebinary__ieee_2Eflags,type,( ty_2Ebinary__ieee_2Eflags:del )).
thf(tp_ty_2Ebinary__ieee_2Efloat,type,( ty_2Ebinary__ieee_2Efloat: del > del >del )).
thf(tp_ty_2Ebinary__ieee_2Efloat__compare,type,( ty_2Ebinary__ieee_2Efloat__compare:del )).
thf(tp_ty_2Ebinary__ieee_2Efloat__value,type,( ty_2Ebinary__ieee_2Efloat__value:del )).
thf(tp_ty_2Ebinary__ieee_2Efp__op,type,( ty_2Ebinary__ieee_2Efp__op: del > del >del )).
thf(tp_ty_2Ebinary__ieee_2Erounding,type,( ty_2Ebinary__ieee_2Erounding:del )).
thf(stp_ty_2Ebinary__ieee_2Efloat__compare,type,(tp__ty_2Ebinary__ieee_2Efloat__compare : $tType)).
thf(stp_inj_ty_2Ebinary__ieee_2Efloat__compare,type,(inj__ty_2Ebinary__ieee_2Efloat__compare : (tp__ty_2Ebinary__ieee_2Efloat__compare > $i))).
thf(stp_surj_ty_2Ebinary__ieee_2Efloat__compare,type,(surj__ty_2Ebinary__ieee_2Efloat__compare : ($i > tp__ty_2Ebinary__ieee_2Efloat__compare))).
thf(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))).
thf(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))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2EEQ,type,(c_2Ebinary__ieee_2EEQ:$i)).
thf(mem_c_2Ebinary__ieee_2EEQ,axiom,(mem@c_2Ebinary__ieee_2EEQ@ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_fo_c_2Ebinary__ieee_2EEQ,type,(fo__c_2Ebinary__ieee_2EEQ:tp__ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EEQ,axiom,((inj__ty_2Ebinary__ieee_2Efloat__compare @ fo__c_2Ebinary__ieee_2EEQ) = c_2Ebinary__ieee_2EEQ)).
thf(stp_ty_2Ebinary__ieee_2Erounding,type,(tp__ty_2Ebinary__ieee_2Erounding : $tType)).
thf(stp_inj_ty_2Ebinary__ieee_2Erounding,type,(inj__ty_2Ebinary__ieee_2Erounding : (tp__ty_2Ebinary__ieee_2Erounding > $i))).
thf(stp_surj_ty_2Ebinary__ieee_2Erounding,type,(surj__ty_2Ebinary__ieee_2Erounding : ($i > tp__ty_2Ebinary__ieee_2Erounding))).
thf(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))).
thf(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))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2EFP__Add,type,(c_2Ebinary__ieee_2EFP__Add:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2EFP__Div,type,(c_2Ebinary__ieee_2EFP__Div:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2EFP__Mul,type,(c_2Ebinary__ieee_2EFP__Mul:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2EFP__MulAdd,type,(c_2Ebinary__ieee_2EFP__MulAdd:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Ebinary__ieee_2EFP__MulSub,type,(c_2Ebinary__ieee_2EFP__MulSub:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Ebinary__ieee_2EFP__Sqrt,type,(c_2Ebinary__ieee_2EFP__Sqrt:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2EFP__Sub,type,(c_2Ebinary__ieee_2EFP__Sub:(del>(del>$i)))).
thf(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)))))))).
thf(stp_ty_2Ebinary__ieee_2Efloat__value,type,(tp__ty_2Ebinary__ieee_2Efloat__value : $tType)).
thf(stp_inj_ty_2Ebinary__ieee_2Efloat__value,type,(inj__ty_2Ebinary__ieee_2Efloat__value : (tp__ty_2Ebinary__ieee_2Efloat__value > $i))).
thf(stp_surj_ty_2Ebinary__ieee_2Efloat__value,type,(surj__ty_2Ebinary__ieee_2Efloat__value : ($i > tp__ty_2Ebinary__ieee_2Efloat__value))).
thf(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))).
thf(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))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2EFloat,type,(c_2Ebinary__ieee_2EFloat:$i)).
thf(mem_c_2Ebinary__ieee_2EFloat,axiom,(mem@c_2Ebinary__ieee_2EFloat@(arr@ty_2Erealax_2Ereal@ty_2Ebinary__ieee_2Efloat__value))).
thf(stp_fo_c_2Ebinary__ieee_2EFloat,type,(fo__c_2Ebinary__ieee_2EFloat:(tp__ty_2Erealax_2Ereal > tp__ty_2Ebinary__ieee_2Efloat__value))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2EGT,type,(c_2Ebinary__ieee_2EGT:$i)).
thf(mem_c_2Ebinary__ieee_2EGT,axiom,(mem@c_2Ebinary__ieee_2EGT@ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_fo_c_2Ebinary__ieee_2EGT,type,(fo__c_2Ebinary__ieee_2EGT:tp__ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EGT,axiom,((inj__ty_2Ebinary__ieee_2Efloat__compare @ fo__c_2Ebinary__ieee_2EGT) = c_2Ebinary__ieee_2EGT)).
thf(tp_c_2Ebinary__ieee_2EInfinity,type,(c_2Ebinary__ieee_2EInfinity:$i)).
thf(mem_c_2Ebinary__ieee_2EInfinity,axiom,(mem@c_2Ebinary__ieee_2EInfinity@ty_2Ebinary__ieee_2Efloat__value)).
thf(stp_fo_c_2Ebinary__ieee_2EInfinity,type,(fo__c_2Ebinary__ieee_2EInfinity:tp__ty_2Ebinary__ieee_2Efloat__value)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EInfinity,axiom,((inj__ty_2Ebinary__ieee_2Efloat__value @ fo__c_2Ebinary__ieee_2EInfinity) = c_2Ebinary__ieee_2EInfinity)).
thf(tp_c_2Ebinary__ieee_2ELT,type,(c_2Ebinary__ieee_2ELT:$i)).
thf(mem_c_2Ebinary__ieee_2ELT,axiom,(mem@c_2Ebinary__ieee_2ELT@ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_fo_c_2Ebinary__ieee_2ELT,type,(fo__c_2Ebinary__ieee_2ELT:tp__ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_eq_fo_c_2Ebinary__ieee_2ELT,axiom,((inj__ty_2Ebinary__ieee_2Efloat__compare @ fo__c_2Ebinary__ieee_2ELT) = c_2Ebinary__ieee_2ELT)).
thf(tp_c_2Ebinary__ieee_2ENaN,type,(c_2Ebinary__ieee_2ENaN:$i)).
thf(mem_c_2Ebinary__ieee_2ENaN,axiom,(mem@c_2Ebinary__ieee_2ENaN@ty_2Ebinary__ieee_2Efloat__value)).
thf(stp_fo_c_2Ebinary__ieee_2ENaN,type,(fo__c_2Ebinary__ieee_2ENaN:tp__ty_2Ebinary__ieee_2Efloat__value)).
thf(stp_eq_fo_c_2Ebinary__ieee_2ENaN,axiom,((inj__ty_2Ebinary__ieee_2Efloat__value @ fo__c_2Ebinary__ieee_2ENaN) = c_2Ebinary__ieee_2ENaN)).
thf(tp_c_2Ebinary__ieee_2EULP,type,(c_2Ebinary__ieee_2EULP:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2EUN,type,(c_2Ebinary__ieee_2EUN:$i)).
thf(mem_c_2Ebinary__ieee_2EUN,axiom,(mem@c_2Ebinary__ieee_2EUN@ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_fo_c_2Ebinary__ieee_2EUN,type,(fo__c_2Ebinary__ieee_2EUN:tp__ty_2Ebinary__ieee_2Efloat__compare)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EUN,axiom,((inj__ty_2Ebinary__ieee_2Efloat__compare @ fo__c_2Ebinary__ieee_2EUN) = c_2Ebinary__ieee_2EUN)).
thf(stp_ty_2Ebinary__ieee_2Eflags,type,(tp__ty_2Ebinary__ieee_2Eflags : $tType)).
thf(stp_inj_ty_2Ebinary__ieee_2Eflags,type,(inj__ty_2Ebinary__ieee_2Eflags : (tp__ty_2Ebinary__ieee_2Eflags > $i))).
thf(stp_surj_ty_2Ebinary__ieee_2Eflags,type,(surj__ty_2Ebinary__ieee_2Eflags : ($i > tp__ty_2Ebinary__ieee_2Eflags))).
thf(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))).
thf(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))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Echeck__for__signalling,type,(c_2Ebinary__ieee_2Echeck__for__signalling:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Eclear__flags,type,(c_2Ebinary__ieee_2Eclear__flags:$i)).
thf(mem_c_2Ebinary__ieee_2Eclear__flags,axiom,(mem@c_2Ebinary__ieee_2Eclear__flags@ty_2Ebinary__ieee_2Eflags)).
thf(stp_fo_c_2Ebinary__ieee_2Eclear__flags,type,(fo__c_2Ebinary__ieee_2Eclear__flags:tp__ty_2Ebinary__ieee_2Eflags)).
thf(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)).
thf(tp_c_2Ebinary__ieee_2Eclosest,type,(c_2Ebinary__ieee_2Eclosest:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Eclosest__such,type,(c_2Ebinary__ieee_2Eclosest__such:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Edividezero__flags,type,(c_2Ebinary__ieee_2Edividezero__flags:$i)).
thf(mem_c_2Ebinary__ieee_2Edividezero__flags,axiom,(mem@c_2Ebinary__ieee_2Edividezero__flags@ty_2Ebinary__ieee_2Eflags)).
thf(stp_fo_c_2Ebinary__ieee_2Edividezero__flags,type,(fo__c_2Ebinary__ieee_2Edividezero__flags:tp__ty_2Ebinary__ieee_2Eflags)).
thf(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)).
thf(tp_c_2Ebinary__ieee_2Eexponent__boundary,type,(c_2Ebinary__ieee_2Eexponent__boundary:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Eflags__CASE,type,(c_2Ebinary__ieee_2Eflags__CASE:(del>$i))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Eflags__DivideByZero,type,(c_2Ebinary__ieee_2Eflags__DivideByZero:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__DivideByZero,axiom,(mem@c_2Ebinary__ieee_2Eflags__DivideByZero@(arr@ty_2Ebinary__ieee_2Eflags@bool))).
thf(tp_c_2Ebinary__ieee_2Eflags__DivideByZero__fupd,type,(c_2Ebinary__ieee_2Eflags__DivideByZero__fupd:$i)).
thf(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)))).
thf(tp_c_2Ebinary__ieee_2Eflags__InvalidOp,type,(c_2Ebinary__ieee_2Eflags__InvalidOp:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__InvalidOp,axiom,(mem@c_2Ebinary__ieee_2Eflags__InvalidOp@(arr@ty_2Ebinary__ieee_2Eflags@bool))).
thf(tp_c_2Ebinary__ieee_2Eflags__InvalidOp__fupd,type,(c_2Ebinary__ieee_2Eflags__InvalidOp__fupd:$i)).
thf(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)))).
thf(tp_c_2Ebinary__ieee_2Eflags__Overflow,type,(c_2Ebinary__ieee_2Eflags__Overflow:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__Overflow,axiom,(mem@c_2Ebinary__ieee_2Eflags__Overflow@(arr@ty_2Ebinary__ieee_2Eflags@bool))).
thf(tp_c_2Ebinary__ieee_2Eflags__Overflow__fupd,type,(c_2Ebinary__ieee_2Eflags__Overflow__fupd:$i)).
thf(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)))).
thf(tp_c_2Ebinary__ieee_2Eflags__Precision,type,(c_2Ebinary__ieee_2Eflags__Precision:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__Precision,axiom,(mem@c_2Ebinary__ieee_2Eflags__Precision@(arr@ty_2Ebinary__ieee_2Eflags@bool))).
thf(tp_c_2Ebinary__ieee_2Eflags__Precision__fupd,type,(c_2Ebinary__ieee_2Eflags__Precision__fupd:$i)).
thf(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)))).
thf(tp_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,type,(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding,axiom,(mem@c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding@(arr@ty_2Ebinary__ieee_2Eflags@bool))).
thf(tp_c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding__fupd,type,(c_2Ebinary__ieee_2Eflags__Underflow__AfterRounding__fupd:$i)).
thf(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)))).
thf(tp_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,type,(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding,axiom,(mem@c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding@(arr@ty_2Ebinary__ieee_2Eflags@bool))).
thf(tp_c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding__fupd,type,(c_2Ebinary__ieee_2Eflags__Underflow__BeforeRounding__fupd:$i)).
thf(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)))).
thf(tp_c_2Ebinary__ieee_2Eflags__size,type,(c_2Ebinary__ieee_2Eflags__size:$i)).
thf(mem_c_2Ebinary__ieee_2Eflags__size,axiom,(mem@c_2Ebinary__ieee_2Eflags__size@(arr@ty_2Ebinary__ieee_2Eflags@ty_2Enum_2Enum))).
thf(stp_fo_c_2Ebinary__ieee_2Eflags__size,type,(fo__c_2Ebinary__ieee_2Eflags__size:(tp__ty_2Ebinary__ieee_2Eflags > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__CASE,type,(c_2Ebinary__ieee_2Efloat__CASE:(del>(del>(del>$i))))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Exponent,type,(c_2Ebinary__ieee_2Efloat__Exponent:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Exponent__fupd,type,(c_2Ebinary__ieee_2Efloat__Exponent__fupd:(del>(del>(del>$i))))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Sign,type,(c_2Ebinary__ieee_2Efloat__Sign:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Sign__fupd,type,(c_2Ebinary__ieee_2Efloat__Sign__fupd:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Significand,type,(c_2Ebinary__ieee_2Efloat__Significand:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__Significand__fupd,type,(c_2Ebinary__ieee_2Efloat__Significand__fupd:(del>(del>(del>$i))))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__abs,type,(c_2Ebinary__ieee_2Efloat__abs:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__add,type,(c_2Ebinary__ieee_2Efloat__add:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__bottom,type,(c_2Ebinary__ieee_2Efloat__bottom:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__compare,type,(c_2Ebinary__ieee_2Efloat__compare:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__compare2num,type,(c_2Ebinary__ieee_2Efloat__compare2num:$i)).
thf(mem_c_2Ebinary__ieee_2Efloat__compare2num,axiom,(mem@c_2Ebinary__ieee_2Efloat__compare2num@(arr@ty_2Ebinary__ieee_2Efloat__compare@ty_2Enum_2Enum))).
thf(stp_fo_c_2Ebinary__ieee_2Efloat__compare2num,type,(fo__c_2Ebinary__ieee_2Efloat__compare2num:(tp__ty_2Ebinary__ieee_2Efloat__compare > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__compare__CASE,type,(c_2Ebinary__ieee_2Efloat__compare__CASE:(del>$i))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__compare__size,type,(c_2Ebinary__ieee_2Efloat__compare__size:$i)).
thf(mem_c_2Ebinary__ieee_2Efloat__compare__size,axiom,(mem@c_2Ebinary__ieee_2Efloat__compare__size@(arr@ty_2Ebinary__ieee_2Efloat__compare@ty_2Enum_2Enum))).
thf(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))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__div,type,(c_2Ebinary__ieee_2Efloat__div:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__equal,type,(c_2Ebinary__ieee_2Efloat__equal:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__greater__equal,type,(c_2Ebinary__ieee_2Efloat__greater__equal:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__greater__than,type,(c_2Ebinary__ieee_2Efloat__greater__than:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__finite,type,(c_2Ebinary__ieee_2Efloat__is__finite:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__infinite,type,(c_2Ebinary__ieee_2Efloat__is__infinite:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__integral,type,(c_2Ebinary__ieee_2Efloat__is__integral:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__nan,type,(c_2Ebinary__ieee_2Efloat__is__nan:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__normal,type,(c_2Ebinary__ieee_2Efloat__is__normal:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__signalling,type,(c_2Ebinary__ieee_2Efloat__is__signalling:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__subnormal,type,(c_2Ebinary__ieee_2Efloat__is__subnormal:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__is__zero,type,(c_2Ebinary__ieee_2Efloat__is__zero:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__less__equal,type,(c_2Ebinary__ieee_2Efloat__less__equal:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__less__than,type,(c_2Ebinary__ieee_2Efloat__less__than:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__minus__infinity,type,(c_2Ebinary__ieee_2Efloat__minus__infinity:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__minus__min,type,(c_2Ebinary__ieee_2Efloat__minus__min:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__minus__zero,type,(c_2Ebinary__ieee_2Efloat__minus__zero:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__mul,type,(c_2Ebinary__ieee_2Efloat__mul:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__mul__add,type,(c_2Ebinary__ieee_2Efloat__mul__add:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__mul__sub,type,(c_2Ebinary__ieee_2Efloat__mul__sub:(del>(del>$i)))).
thf(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)))))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__negate,type,(c_2Ebinary__ieee_2Efloat__negate:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__plus__infinity,type,(c_2Ebinary__ieee_2Efloat__plus__infinity:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__plus__min,type,(c_2Ebinary__ieee_2Efloat__plus__min:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__plus__zero,type,(c_2Ebinary__ieee_2Efloat__plus__zero:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__round,type,(c_2Ebinary__ieee_2Efloat__round:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__round__to__integral,type,(c_2Ebinary__ieee_2Efloat__round__to__integral:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__round__with__flags,type,(c_2Ebinary__ieee_2Efloat__round__with__flags:(del>(del>$i)))).
thf(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))))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__size,type,(c_2Ebinary__ieee_2Efloat__size:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__some__qnan,type,(c_2Ebinary__ieee_2Efloat__some__qnan:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__sqrt,type,(c_2Ebinary__ieee_2Efloat__sqrt:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__sub,type,(c_2Ebinary__ieee_2Efloat__sub:(del>(del>$i)))).
thf(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))))))))).
thf(stp_c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint,type,(tp__c_ty_2Eoption_2Eoption_ty_2Einteger_2Eint : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__to__int,type,(c_2Ebinary__ieee_2Efloat__to__int:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__to__real,type,(c_2Ebinary__ieee_2Efloat__to__real:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__top,type,(c_2Ebinary__ieee_2Efloat__top:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Ebinary__ieee_2Efloat__value,type,(c_2Ebinary__ieee_2Efloat__value:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efloat__value__CASE,type,(c_2Ebinary__ieee_2Efloat__value__CASE:(del>$i))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Efloat__value__size,type,(c_2Ebinary__ieee_2Efloat__value__size:$i)).
thf(mem_c_2Ebinary__ieee_2Efloat__value__size,axiom,(mem@c_2Ebinary__ieee_2Efloat__value__size@(arr@ty_2Ebinary__ieee_2Efloat__value@ty_2Enum_2Enum))).
thf(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))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Efp__op__CASE,type,(c_2Ebinary__ieee_2Efp__op__CASE:(del>(del>(del>$i))))).
thf(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))))))))))))).
thf(tp_c_2Ebinary__ieee_2Efp__op__size,type,(c_2Ebinary__ieee_2Efp__op__size:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Eintegral__round,type,(c_2Ebinary__ieee_2Eintegral__round:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Einvalidop__flags,type,(c_2Ebinary__ieee_2Einvalidop__flags:$i)).
thf(mem_c_2Ebinary__ieee_2Einvalidop__flags,axiom,(mem@c_2Ebinary__ieee_2Einvalidop__flags@ty_2Ebinary__ieee_2Eflags)).
thf(stp_fo_c_2Ebinary__ieee_2Einvalidop__flags,type,(fo__c_2Ebinary__ieee_2Einvalidop__flags:tp__ty_2Ebinary__ieee_2Eflags)).
thf(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)).
thf(tp_c_2Ebinary__ieee_2Eis__closest,type,(c_2Ebinary__ieee_2Eis__closest:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Eis__integral,type,(c_2Ebinary__ieee_2Eis__integral:$i)).
thf(mem_c_2Ebinary__ieee_2Eis__integral,axiom,(mem@c_2Ebinary__ieee_2Eis__integral@(arr@ty_2Erealax_2Ereal@bool))).
thf(tp_c_2Ebinary__ieee_2Elargest,type,(c_2Ebinary__ieee_2Elargest:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Enum2float__compare,type,(c_2Ebinary__ieee_2Enum2float__compare:$i)).
thf(mem_c_2Ebinary__ieee_2Enum2float__compare,axiom,(mem@c_2Ebinary__ieee_2Enum2float__compare@(arr@ty_2Enum_2Enum@ty_2Ebinary__ieee_2Efloat__compare))).
thf(stp_fo_c_2Ebinary__ieee_2Enum2float__compare,type,(fo__c_2Ebinary__ieee_2Enum2float__compare:(tp__ty_2Enum_2Enum > tp__ty_2Ebinary__ieee_2Efloat__compare))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Enum2rounding,type,(c_2Ebinary__ieee_2Enum2rounding:$i)).
thf(mem_c_2Ebinary__ieee_2Enum2rounding,axiom,(mem@c_2Ebinary__ieee_2Enum2rounding@(arr@ty_2Enum_2Enum@ty_2Ebinary__ieee_2Erounding))).
thf(stp_fo_c_2Ebinary__ieee_2Enum2rounding,type,(fo__c_2Ebinary__ieee_2Enum2rounding:(tp__ty_2Enum_2Enum > tp__ty_2Ebinary__ieee_2Erounding))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Ereal__to__float,type,(c_2Ebinary__ieee_2Ereal__to__float:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2Ereal__to__float__with__flags,type,(c_2Ebinary__ieee_2Ereal__to__float__with__flags:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Erecordtype_2Eflags,type,(c_2Ebinary__ieee_2Erecordtype_2Eflags:$i)).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Erecordtype_2Efloat,type,(c_2Ebinary__ieee_2Erecordtype_2Efloat:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Eround,type,(c_2Ebinary__ieee_2Eround:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Ebinary__ieee_2EroundTiesToEven,type,(c_2Ebinary__ieee_2EroundTiesToEven:$i)).
thf(mem_c_2Ebinary__ieee_2EroundTiesToEven,axiom,(mem@c_2Ebinary__ieee_2EroundTiesToEven@ty_2Ebinary__ieee_2Erounding)).
thf(stp_fo_c_2Ebinary__ieee_2EroundTiesToEven,type,(fo__c_2Ebinary__ieee_2EroundTiesToEven:tp__ty_2Ebinary__ieee_2Erounding)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EroundTiesToEven,axiom,((inj__ty_2Ebinary__ieee_2Erounding @ fo__c_2Ebinary__ieee_2EroundTiesToEven) = c_2Ebinary__ieee_2EroundTiesToEven)).
thf(tp_c_2Ebinary__ieee_2EroundTowardNegative,type,(c_2Ebinary__ieee_2EroundTowardNegative:$i)).
thf(mem_c_2Ebinary__ieee_2EroundTowardNegative,axiom,(mem@c_2Ebinary__ieee_2EroundTowardNegative@ty_2Ebinary__ieee_2Erounding)).
thf(stp_fo_c_2Ebinary__ieee_2EroundTowardNegative,type,(fo__c_2Ebinary__ieee_2EroundTowardNegative:tp__ty_2Ebinary__ieee_2Erounding)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EroundTowardNegative,axiom,((inj__ty_2Ebinary__ieee_2Erounding @ fo__c_2Ebinary__ieee_2EroundTowardNegative) = c_2Ebinary__ieee_2EroundTowardNegative)).
thf(tp_c_2Ebinary__ieee_2EroundTowardPositive,type,(c_2Ebinary__ieee_2EroundTowardPositive:$i)).
thf(mem_c_2Ebinary__ieee_2EroundTowardPositive,axiom,(mem@c_2Ebinary__ieee_2EroundTowardPositive@ty_2Ebinary__ieee_2Erounding)).
thf(stp_fo_c_2Ebinary__ieee_2EroundTowardPositive,type,(fo__c_2Ebinary__ieee_2EroundTowardPositive:tp__ty_2Ebinary__ieee_2Erounding)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EroundTowardPositive,axiom,((inj__ty_2Ebinary__ieee_2Erounding @ fo__c_2Ebinary__ieee_2EroundTowardPositive) = c_2Ebinary__ieee_2EroundTowardPositive)).
thf(tp_c_2Ebinary__ieee_2EroundTowardZero,type,(c_2Ebinary__ieee_2EroundTowardZero:$i)).
thf(mem_c_2Ebinary__ieee_2EroundTowardZero,axiom,(mem@c_2Ebinary__ieee_2EroundTowardZero@ty_2Ebinary__ieee_2Erounding)).
thf(stp_fo_c_2Ebinary__ieee_2EroundTowardZero,type,(fo__c_2Ebinary__ieee_2EroundTowardZero:tp__ty_2Ebinary__ieee_2Erounding)).
thf(stp_eq_fo_c_2Ebinary__ieee_2EroundTowardZero,axiom,((inj__ty_2Ebinary__ieee_2Erounding @ fo__c_2Ebinary__ieee_2EroundTowardZero) = c_2Ebinary__ieee_2EroundTowardZero)).
thf(tp_c_2Ebinary__ieee_2Erounding2num,type,(c_2Ebinary__ieee_2Erounding2num:$i)).
thf(mem_c_2Ebinary__ieee_2Erounding2num,axiom,(mem@c_2Ebinary__ieee_2Erounding2num@(arr@ty_2Ebinary__ieee_2Erounding@ty_2Enum_2Enum))).
thf(stp_fo_c_2Ebinary__ieee_2Erounding2num,type,(fo__c_2Ebinary__ieee_2Erounding2num:(tp__ty_2Ebinary__ieee_2Erounding > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Erounding__CASE,type,(c_2Ebinary__ieee_2Erounding__CASE:(del>$i))).
thf(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)))))))).
thf(tp_c_2Ebinary__ieee_2Erounding__size,type,(c_2Ebinary__ieee_2Erounding__size:$i)).
thf(mem_c_2Ebinary__ieee_2Erounding__size,axiom,(mem@c_2Ebinary__ieee_2Erounding__size@(arr@ty_2Ebinary__ieee_2Erounding@ty_2Enum_2Enum))).
thf(stp_fo_c_2Ebinary__ieee_2Erounding__size,type,(fo__c_2Ebinary__ieee_2Erounding__size:(tp__ty_2Ebinary__ieee_2Erounding > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Ethreshold,type,(c_2Ebinary__ieee_2Ethreshold:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Ebinary__ieee_2Eulp,type,(c_2Ebinary__ieee_2Eulp:(del>(del>$i)))).
thf(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))))).
thf(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))@(lam@(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))))@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(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))))@bool))@(lam@(arr@(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))))@bool)@(^ [V2_27float_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(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)))))@(lam@(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))))@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_3F@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone))@(lam@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(^ [V4a0:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Efcp_2Ecart@bool@A_27w))@(lam@(ty_2Efcp_2Ecart@bool@A_27w)@(^ [V5a1:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Efcp_2Ecart@bool@A_27t))@(lam@(ty_2Efcp_2Ecart@bool@A_27t)@(^ [V6a2:$i] : (ap@(ap@(c_2Emin_2E_3D@(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)))))@V3a0_27)@(ap@(ap@(ap@(lam@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(^ [V7a0:$i] : (lam@(ty_2Efcp_2Ecart@bool@A_27w)@(^ [V8a1:$i] : (lam@(ty_2Efcp_2Ecart@bool@A_27t)@(^ [V9a2:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(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))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Efcp_2Ecart@bool@ty_2Eone_2Eone)@(ty_2Epair_2Eprod@(ty_2Efcp_2Ecart@bool@A_27w)@(ty_2Efcp_2Ecart@bool@A_27t)))@V7a0)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Efcp_2Ecart@bool@A_27w)@(ty_2Efcp_2Ecart@bool@A_27t))@V8a1)@V9a2)))@(lam@ty_2Enum_2Enum@(^ [V10n:$i] : (c_2Eind__type_2EBOTTOM@(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)))))))))))))@V4a0)@V5a1)@V6a2))))))))))))@(ap@V2_27float_27@V3a0_27))))))@(ap@V2_27float_27@V1a0_27))))))))@V0rep))))))).
thf(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))))))))))))).
thf(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))))))))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))))).
thf(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)))))))))))))))))))).
thf(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))))))))))))))))).
thf(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))))))))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))))))))))).
thf(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)))))))))))).
thf(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)))))))))))))))))).
thf(conj_thm_2Ebinary__ieee_2Efloat__literal__nchotomy,conjecture,( ! [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)))))))))))))))))).
