tt('type/binary_ieee/float', ty, $t > $t > $t).
tt('type/binary_ieee/float_compare', ty, $t).
tt('type/binary_ieee/float_value', ty, $t).
tt('type/binary_ieee/rounding', ty, $t).
tt('const/binary_ieee/EQ', ty, 'type/binary_ieee/float_compare').
tt('const/binary_ieee/Float', ty, ('type/realax/real' > 'type/binary_ieee/float_value')).
tt('const/binary_ieee/GT', ty, 'type/binary_ieee/float_compare').
tt('const/binary_ieee/Infinity', ty, 'type/binary_ieee/float_value').
tt('const/binary_ieee/LT', ty, 'type/binary_ieee/float_compare').
tt('const/binary_ieee/NaN', ty, 'type/binary_ieee/float_value').
tt('const/binary_ieee/ULP', ty, ![T : $t, W : $t]: (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > 'type/realax/real')).
tt('const/binary_ieee/UN', ty, 'type/binary_ieee/float_compare').
tt('const/binary_ieee/closest', ty, ![A : $t, B : $t]: ((('type/binary_ieee/float' A B) > $o) > ('type/realax/real' > ('type/binary_ieee/float' A B)))).
tt('const/binary_ieee/closest_such', ty, ![A : $t, B : $t]: ((('type/binary_ieee/float' A B) > $o) > ((('type/binary_ieee/float' A B) > $o) > ('type/realax/real' > ('type/binary_ieee/float' A B))))).
tt('const/binary_ieee/exponent_boundary', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > $o))).
tt('const/binary_ieee/float_CASE', ty, ![A : $t, T : $t, W : $t]: (('type/binary_ieee/float' T W) > ((('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > A))) > A))).
tt('const/binary_ieee/float_Exponent', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > ('type/fcp/cart' $o W))).
tt('const/binary_ieee/float_Exponent_fupd', ty, ![T : $t, W : $t]: ((('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/float_Sign', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > ('type/fcp/cart' $o 'type/one/one'))).
tt('const/binary_ieee/float_Sign_fupd', ty, ![T : $t, W : $t]: ((('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/float_Significand', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > ('type/fcp/cart' $o T))).
tt('const/binary_ieee/float_Significand_fupd', ty, ![T : $t, W : $t]: ((('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/float_abs', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_add', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W))))).
tt('const/binary_ieee/float_bottom', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_compare', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > 'type/binary_ieee/float_compare'))).
tt('const/binary_ieee/float_compare2num', ty, ('type/binary_ieee/float_compare' > 'type/num/num')).
tt('const/binary_ieee/float_compare_CASE', ty, ![A : $t]: ('type/binary_ieee/float_compare' > (A > (A > (A > (A > A)))))).
tt('const/binary_ieee/float_compare_size', ty, ('type/binary_ieee/float_compare' > 'type/num/num')).
tt('const/binary_ieee/float_div', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W))))).
tt('const/binary_ieee/float_equal', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > $o))).
tt('const/binary_ieee/float_greater_equal', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > $o))).
tt('const/binary_ieee/float_greater_than', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > $o))).
tt('const/binary_ieee/float_is_finite', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_is_infinite', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_is_integral', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_is_nan', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_is_normal', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_is_subnormal', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_is_zero', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > $o)).
tt('const/binary_ieee/float_less_equal', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > $o))).
tt('const/binary_ieee/float_less_than', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > $o))).
tt('const/binary_ieee/float_minus_infinity', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_minus_min', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_minus_zero', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_mul', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W))))).
tt('const/binary_ieee/float_mul_add', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W)))))).
tt('const/binary_ieee/float_negate', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_plus_infinity', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_plus_min', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_plus_zero', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_round', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > ($o > ('type/realax/real' > ('type/binary_ieee/float' T W))))).
tt('const/binary_ieee/float_round_to_integral', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/float_size', ty, ![T : $t, W : $t]: ((T > 'type/num/num') > ((W > 'type/num/num') > (('type/binary_ieee/float' T W) > 'type/num/num')))).
tt('const/binary_ieee/float_some_nan', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_sqrt', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/float_sub', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > (('type/binary_ieee/float' T W) > (('type/binary_ieee/float' T W) > ('type/binary_ieee/float' T W))))).
tt('const/binary_ieee/float_to_real', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > 'type/realax/real')).
tt('const/binary_ieee/float_top', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > ('type/binary_ieee/float' T W))).
tt('const/binary_ieee/float_value', ty, ![T : $t, W : $t]: (('type/binary_ieee/float' T W) > 'type/binary_ieee/float_value')).
tt('const/binary_ieee/float_value_CASE', ty, ![A : $t]: ('type/binary_ieee/float_value' > (('type/realax/real' > A) > (A > (A > A))))).
tt('const/binary_ieee/float_value_size', ty, ('type/binary_ieee/float_value' > 'type/num/num')).
tt('const/binary_ieee/integral_round', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > ('type/realax/real' > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/is_closest', ty, ![A : $t, B : $t]: ((('type/binary_ieee/float' A B) > $o) > ('type/realax/real' > (('type/binary_ieee/float' A B) > $o)))).
tt('const/binary_ieee/largest', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > 'type/realax/real')).
tt('const/binary_ieee/num2float_compare', ty, ('type/num/num' > 'type/binary_ieee/float_compare')).
tt('const/binary_ieee/num2rounding', ty, ('type/num/num' > 'type/binary_ieee/rounding')).
tt('const/binary_ieee/recordtype.float', ty, ![T : $t, W : $t]: (('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > ('type/binary_ieee/float' T W))))).
tt('const/binary_ieee/round', ty, ![T : $t, W : $t]: ('type/binary_ieee/rounding' > ('type/realax/real' > ('type/binary_ieee/float' T W)))).
tt('const/binary_ieee/roundTiesToEven', ty, 'type/binary_ieee/rounding').
tt('const/binary_ieee/roundTowardNegative', ty, 'type/binary_ieee/rounding').
tt('const/binary_ieee/roundTowardPositive', ty, 'type/binary_ieee/rounding').
tt('const/binary_ieee/roundTowardZero', ty, 'type/binary_ieee/rounding').
tt('const/binary_ieee/rounding2num', ty, ('type/binary_ieee/rounding' > 'type/num/num')).
tt('const/binary_ieee/rounding_CASE', ty, ![A : $t]: ('type/binary_ieee/rounding' > (A > (A > (A > (A > A)))))).
tt('const/binary_ieee/rounding_size', ty, ('type/binary_ieee/rounding' > 'type/num/num')).
tt('const/binary_ieee/threshold', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > 'type/realax/real')).
tt('const/binary_ieee/ulp', ty, ![T : $t, W : $t]: (('type/bool/itself' ('type/pair/prod' T W)) > 'type/realax/real')).
tt('thm/binary_ieee/float_TY_DEF_', def, ![T : $t, W : $t]: (?[rep : (('type/binary_ieee/float' T W) > ('type/ind_type/recspace' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T)))))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T)))) ('type/binary_ieee/float' T W)) (^['a0\'' : ('type/ind_type/recspace' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T))))]: (!['\'float\'' : (('type/ind_type/recspace' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T)))) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T))))]: ((?[a0 : ('type/fcp/cart' $o 'type/one/one'), a1 : ('type/fcp/cart' $o W), a2 : ('type/fcp/cart' $o T)]: ('a0\'0' = ((^[a00 : ('type/fcp/cart' $o 'type/one/one'), a10 : ('type/fcp/cart' $o W), a20 : ('type/fcp/cart' $o T)]: (('const/ind_type/CONSTR' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T)))) 'const/num/0' (('const/pair/,' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T))) a00 (('const/pair/,' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T)) a10 a20)) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' ('type/fcp/cart' $o 'type/one/one') ('type/pair/prod' ('type/fcp/cart' $o W) ('type/fcp/cart' $o T))))))) a0 a1 a2))) => ('\'float\'' 'a0\'0'))) => ('\'float\'' 'a0\'')))) rep))).
tt('thm/binary_ieee/float_case_def_', def, ![T : $t, W : $t, A : $t]: (![a0 : ('type/fcp/cart' $o 'type/one/one'), a1 : ('type/fcp/cart' $o W), a2 : ('type/fcp/cart' $o T), f : (('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > A)))]: ((('const/binary_ieee/float_CASE' A T W) (('const/binary_ieee/recordtype.float' T W) a0 a1 a2) f) = (f a0 a1 a2)))).
tt('thm/binary_ieee/float_size_def_', def, ![T : $t, W : $t]: (![f : (T > 'type/num/num'), f1 : (W > 'type/num/num'), a0 : ('type/fcp/cart' $o 'type/one/one'), a1 : ('type/fcp/cart' $o W), a2 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_size' T W) f f1 (('const/binary_ieee/recordtype.float' T W) a0 a1 a2)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_Sign_', def, ![T : $t, W : $t]: (![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = c))).
tt('thm/binary_ieee/float_Exponent_', def, ![W : $t, T : $t]: (![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = c0))).
tt('thm/binary_ieee/float_Significand_', def, ![T : $t, W : $t]: (![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = c1))).
tt('thm/binary_ieee/float_accessors_0', ax, ![T : $t, W : $t]: (![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = c))).
tt('thm/binary_ieee/float_accessors_1', ax, ![W : $t, T : $t]: (![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = c0))).
tt('thm/binary_ieee/float_accessors_e2', ax, ![T : $t, W : $t]: (![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = c1))).
tt('thm/binary_ieee/float_Sign_fupd_', def, ![T : $t, W : $t]: (![f : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Sign_fupd' T W) f (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = (('const/binary_ieee/recordtype.float' T W) (f c) c0 c1)))).
tt('thm/binary_ieee/float_Exponent_fupd_', def, ![T : $t, W : $t]: (![f : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Exponent_fupd' T W) f (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = (('const/binary_ieee/recordtype.float' T W) c (f c0) c1)))).
tt('thm/binary_ieee/float_Significand_fupd_', def, ![T : $t, W : $t]: (![f : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Significand_fupd' T W) f (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = (('const/binary_ieee/recordtype.float' T W) c c0 (f c1))))).
tt('thm/binary_ieee/float_fn_updates_0', ax, ![T : $t, W : $t]: (![f : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Sign_fupd' T W) f (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = (('const/binary_ieee/recordtype.float' T W) (f c) c0 c1)))).
tt('thm/binary_ieee/float_fn_updates_1', ax, ![T : $t, W : $t]: (![f : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Exponent_fupd' T W) f (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = (('const/binary_ieee/recordtype.float' T W) c (f c0) c1)))).
tt('thm/binary_ieee/float_fn_updates_e2', ax, ![T : $t, W : $t]: (![f : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Significand_fupd' T W) f (('const/binary_ieee/recordtype.float' T W) c c0 c1)) = (('const/binary_ieee/recordtype.float' T W) c c0 (f c1))))).
tt('thm/binary_ieee/float_accfupds_0', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_Exponent_fupd' T W) f0 f)) = (('const/binary_ieee/float_Sign' T W) f)))).
tt('thm/binary_ieee/float_accfupds_1', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_Significand_fupd' T W) f0 f)) = (('const/binary_ieee/float_Sign' T W) f)))).
tt('thm/binary_ieee/float_accfupds_2', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_Sign_fupd' T W) f0 f)) = (('const/binary_ieee/float_Exponent' T W) f)))).
tt('thm/binary_ieee/float_accfupds_3', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_Significand_fupd' T W) f0 f)) = (('const/binary_ieee/float_Exponent' T W) f)))).
tt('thm/binary_ieee/float_accfupds_4', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_Sign_fupd' T W) f0 f)) = (('const/binary_ieee/float_Significand' T W) f)))).
tt('thm/binary_ieee/float_accfupds_5', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_Exponent_fupd' T W) f0 f)) = (('const/binary_ieee/float_Significand' T W) f)))).
tt('thm/binary_ieee/float_accfupds_6', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_Sign_fupd' T W) f0 f)) = (f0 (('const/binary_ieee/float_Sign' T W) f))))).
tt('thm/binary_ieee/float_accfupds_7', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_Exponent_fupd' T W) f0 f)) = (f0 (('const/binary_ieee/float_Exponent' T W) f))))).
tt('thm/binary_ieee/float_accfupds_e8', ax, ![T : $t, W : $t]: (![f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_Significand_fupd' T W) f0 f)) = (f0 (('const/binary_ieee/float_Significand' T W) f))))).
tt('thm/binary_ieee/float_fupdfupds_0', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Sign_fupd' T W) f0 (('const/binary_ieee/float_Sign_fupd' T W) g f)) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) f0 g) f)))).
tt('thm/binary_ieee/float_fupdfupds_1', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Exponent_fupd' T W) f0 (('const/binary_ieee/float_Exponent_fupd' T W) g f)) = (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) f0 g) f)))).
tt('thm/binary_ieee/float_fupdfupds_e2', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Significand_fupd' T W) f0 (('const/binary_ieee/float_Significand_fupd' T W) g f)) = (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) f0 g) f)))).
tt('thm/binary_ieee/float_fupdfupds_comp_tLL', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one'))]: ((('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) f0) (('const/binary_ieee/float_Sign_fupd' T W) g)) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) f0 g))))).
tt('thm/binary_ieee/float_fupdfupds_comp_tRL', ax, ![A : $t, T : $t, W : $t]: (![h : (A > ('type/binary_ieee/float' T W)), g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one'))]: ((('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) f0) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) h)) = (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) f0 g)) h)))).
tt('thm/binary_ieee/float_fupdfupds_comp_tLLR', ax, ![W : $t, T : $t]: (![g : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W))]: ((('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) f0) (('const/binary_ieee/float_Exponent_fupd' T W) g)) = (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) f0 g))))).
tt('thm/binary_ieee/float_fupdfupds_comp_tRLR', ax, ![A : $t, T : $t, W : $t]: (![h : (A > ('type/binary_ieee/float' T W)), g : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W))]: ((('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) f0) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) g) h)) = (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) f0 g)) h)))).
tt('thm/binary_ieee/float_fupdfupds_comp_2', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T))]: ((('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) (('const/binary_ieee/float_Significand_fupd' T W) g)) = (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) f0 g))))).
tt('thm/binary_ieee/float_fupdfupds_comp_e3', ax, ![A : $t, T : $t, W : $t]: (![h : (A > ('type/binary_ieee/float' T W)), g : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T))]: ((('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) g) h)) = (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/o' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) f0 g)) h)))).
tt('thm/binary_ieee/float_fupdcanon_0', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Exponent_fupd' T W) f0 (('const/binary_ieee/float_Sign_fupd' T W) g f)) = (('const/binary_ieee/float_Sign_fupd' T W) g (('const/binary_ieee/float_Exponent_fupd' T W) f0 f))))).
tt('thm/binary_ieee/float_fupdcanon_1', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Significand_fupd' T W) f0 (('const/binary_ieee/float_Sign_fupd' T W) g f)) = (('const/binary_ieee/float_Sign_fupd' T W) g (('const/binary_ieee/float_Significand_fupd' T W) f0 f))))).
tt('thm/binary_ieee/float_fupdcanon_e2', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T)), f : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_Significand_fupd' T W) f0 (('const/binary_ieee/float_Exponent_fupd' T W) g f)) = (('const/binary_ieee/float_Exponent_fupd' T W) g (('const/binary_ieee/float_Significand_fupd' T W) f0 f))))).
tt('thm/binary_ieee/float_fupdcanon_comp_tLL', ax, ![W : $t, T : $t]: (![g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W))]: ((('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) f0) (('const/binary_ieee/float_Sign_fupd' T W) g)) = (('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) (('const/binary_ieee/float_Exponent_fupd' T W) f0))))).
tt('thm/binary_ieee/float_fupdcanon_comp_tRL', ax, ![A : $t, T : $t, W : $t]: (![h : (A > ('type/binary_ieee/float' T W)), g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W))]: ((('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) f0) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) h)) = (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) f0) h))))).
tt('thm/binary_ieee/float_fupdcanon_comp_tLLR', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T))]: ((('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) (('const/binary_ieee/float_Sign_fupd' T W) g)) = (('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) (('const/binary_ieee/float_Significand_fupd' T W) f0))))).
tt('thm/binary_ieee/float_fupdcanon_comp_tRLR', ax, ![A : $t, T : $t, W : $t]: (![h : (A > ('type/binary_ieee/float' T W)), g : (('type/fcp/cart' $o 'type/one/one') > ('type/fcp/cart' $o 'type/one/one')), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T))]: ((('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) h)) = (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Sign_fupd' T W) g) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) h))))).
tt('thm/binary_ieee/float_fupdcanon_comp_2', ax, ![T : $t, W : $t]: (![g : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T))]: ((('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) (('const/binary_ieee/float_Exponent_fupd' T W) g)) = (('const/combin/o' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) g) (('const/binary_ieee/float_Significand_fupd' T W) f0))))).
tt('thm/binary_ieee/float_fupdcanon_comp_e3', ax, ![A : $t, T : $t, W : $t]: (![h : (A > ('type/binary_ieee/float' T W)), g : (('type/fcp/cart' $o W) > ('type/fcp/cart' $o W)), f0 : (('type/fcp/cart' $o T) > ('type/fcp/cart' $o T))]: ((('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) g) h)) = (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Exponent_fupd' T W) g) (('const/combin/o' A ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_Significand_fupd' T W) f0) h))))).
tt('thm/binary_ieee/float_component_equality_', ax, ![T : $t, W : $t]: (![f1 : ('type/binary_ieee/float' T W), f2 : ('type/binary_ieee/float' T W)]: ((f1 = f2) = (((('const/binary_ieee/float_Sign' T W) f1) = (('const/binary_ieee/float_Sign' T W) f2)) & (((('const/binary_ieee/float_Exponent' T W) f1) = (('const/binary_ieee/float_Exponent' T W) f2)) & ((('const/binary_ieee/float_Significand' T W) f1) = (('const/binary_ieee/float_Significand' T W) f2))))))).
tt('thm/binary_ieee/float_updates_eq_literal_', ax, ![T : $t, W : $t]: (![f : ('type/binary_ieee/float' T W), c1 : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c1) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c0) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c) f))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c1) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c0) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c) ('const/bool/ARB' ('type/binary_ieee/float' T W)))))))).
tt('thm/binary_ieee/float_literal_nchotomy_', ax, ![T : $t, W : $t]: (![f : ('type/binary_ieee/float' T W)]: (?[c1 : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c : ('type/fcp/cart' $o T)]: (f = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c1) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c0) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))))).
tt('thm/binary_ieee/FORALL_float_', ax, ![T : $t, W : $t]: (![P : (('type/binary_ieee/float' T W) > $o)]: ((![f : ('type/binary_ieee/float' T W)]: (P f)) = (![c1 : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c : ('type/fcp/cart' $o T)]: (P (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c1) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c0) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c) ('const/bool/ARB' ('type/binary_ieee/float' T W)))))))))).
tt('thm/binary_ieee/EXISTS_float_', ax, ![T : $t, W : $t]: (![P : (('type/binary_ieee/float' T W) > $o)]: ((?[f : ('type/binary_ieee/float' T W)]: (P f)) = (?[c1 : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c : ('type/fcp/cart' $o T)]: (P (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c1) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c0) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c) ('const/bool/ARB' ('type/binary_ieee/float' T W)))))))))).
tt('thm/binary_ieee/float_literal_11_', ax, ![T : $t, W : $t]: (![c11 : ('type/fcp/cart' $o 'type/one/one'), c01 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T), c12 : ('type/fcp/cart' $o 'type/one/one'), c02 : ('type/fcp/cart' $o W), c2 : ('type/fcp/cart' $o T)]: (((('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c11) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c01) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c1) ('const/bool/ARB' ('type/binary_ieee/float' T W))))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) c12) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) c02) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) c2) ('const/bool/ARB' ('type/binary_ieee/float' T W)))))) = ((c11 = c12) & ((c01 = c02) & (c1 = c2)))))).
tt('thm/binary_ieee/datatype_float_', ax, ![T : $t, W : $t]: (![record : ('type/min/ind' > (('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > $o)))), float : 'type/min/ind', Significand : ('type/fcp/cart' $o T), Sign : ('type/fcp/cart' $o 'type/one/one'), Exponent : ('type/fcp/cart' $o W)]: (('const/bool/DATATYPE' $o) (record float Sign Exponent Significand)))).
tt('thm/binary_ieee/float_11_', ax, ![T : $t, W : $t]: (![a0 : ('type/fcp/cart' $o 'type/one/one'), a1 : ('type/fcp/cart' $o W), a2 : ('type/fcp/cart' $o T), 'a0\'' : ('type/fcp/cart' $o 'type/one/one'), 'a1\'' : ('type/fcp/cart' $o W), 'a2\'' : ('type/fcp/cart' $o T)]: (((('const/binary_ieee/recordtype.float' T W) a0 a1 a2) = (('const/binary_ieee/recordtype.float' T W) 'a0\'' 'a1\'' 'a2\'')) = ((a0 = 'a0\'') & ((a1 = 'a1\'') & (a2 = 'a2\'')))))).
tt('thm/binary_ieee/float_case_cong_', ax, ![W : $t, T : $t, A : $t]: (!['f\'' : (('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > A))), M : ('type/binary_ieee/float' T W), 'M\'' : ('type/binary_ieee/float' T W), f : (('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > A)))]: (((M = 'M\'') & (![a0 : ('type/fcp/cart' $o 'type/one/one'), a1 : ('type/fcp/cart' $o W), a2 : ('type/fcp/cart' $o T)]: (('M\'' = (('const/binary_ieee/recordtype.float' T W) a0 a1 a2)) => ((f a0 a1 a2) = ('f\'' a0 a1 a2))))) => ((('const/binary_ieee/float_CASE' A T W) M f) = (('const/binary_ieee/float_CASE' A T W) 'M\'' 'f\''))))).
tt('thm/binary_ieee/float_nchotomy_', ax, ![T : $t, W : $t]: (![ff : ('type/binary_ieee/float' T W)]: (?[c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: (ff = (('const/binary_ieee/recordtype.float' T W) c c0 c1))))).
tt('thm/binary_ieee/float_Axiom_', ax, ![T : $t, W : $t, A : $t]: (![f : (('type/fcp/cart' $o 'type/one/one') > (('type/fcp/cart' $o W) > (('type/fcp/cart' $o T) > A)))]: (?[fn : (('type/binary_ieee/float' T W) > A)]: (![a0 : ('type/fcp/cart' $o 'type/one/one'), a1 : ('type/fcp/cart' $o W), a2 : ('type/fcp/cart' $o T)]: ((fn (('const/binary_ieee/recordtype.float' T W) a0 a1 a2)) = (f a0 a1 a2)))))).
tt('thm/binary_ieee/float_induction_', ax, ![T : $t, W : $t]: (![P : (('type/binary_ieee/float' T W) > $o)]: ((![c : ('type/fcp/cart' $o 'type/one/one'), c0 : ('type/fcp/cart' $o W), c1 : ('type/fcp/cart' $o T)]: (P (('const/binary_ieee/recordtype.float' T W) c c0 c1))) => (![f : ('type/binary_ieee/float' T W)]: (P f))))).
tt('thm/binary_ieee/float_value_TY_DEF_', def, (?[rep : ('type/binary_ieee/float_value' > ('type/ind_type/recspace' 'type/realax/real'))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' 'type/realax/real') 'type/binary_ieee/float_value') (^[a0 : ('type/ind_type/recspace' 'type/realax/real')]: (!['\'float_value\'' : (('type/ind_type/recspace' 'type/realax/real') > $o)]: ((![a00 : ('type/ind_type/recspace' 'type/realax/real')]: (((?[a : 'type/realax/real']: (a00 = ((^[a1 : 'type/realax/real']: (('const/ind_type/CONSTR' 'type/realax/real') 'const/num/0' a1 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' 'type/realax/real')))) a))) | ((a00 = (('const/ind_type/CONSTR' 'type/realax/real') ('const/num/SUC' 'const/num/0') ('const/bool/ARB' 'type/realax/real') (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' 'type/realax/real')))) | (a00 = (('const/ind_type/CONSTR' 'type/realax/real') ('const/num/SUC' ('const/num/SUC' 'const/num/0')) ('const/bool/ARB' 'type/realax/real') (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' 'type/realax/real')))))) => ('\'float_value\'' a00))) => ('\'float_value\'' a0)))) rep))).
tt('thm/binary_ieee/float_value_case_def_0', def, ![A : $t]: (![a : 'type/realax/real', f : ('type/realax/real' > A), v : A, v1 : A]: ((('const/binary_ieee/float_value_CASE' A) ('const/binary_ieee/Float' a) f v v1) = (f a)))).
tt('thm/binary_ieee/float_value_case_def_1', def, ![A : $t]: (![f : ('type/realax/real' > A), v : A, v1 : A]: ((('const/binary_ieee/float_value_CASE' A) 'const/binary_ieee/Infinity' f v v1) = v))).
tt('thm/binary_ieee/float_value_case_def_e2', def, ![A : $t]: (![f : ('type/realax/real' > A), v : A, v1 : A]: ((('const/binary_ieee/float_value_CASE' A) 'const/binary_ieee/NaN' f v v1) = v1))).
tt('thm/binary_ieee/float_value_size_def_0', def, (![a : 'type/realax/real']: (('const/binary_ieee/float_value_size' ('const/binary_ieee/Float' a)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_value_size_def_1', def, (('const/binary_ieee/float_value_size' 'const/binary_ieee/Infinity') = 'const/num/0')).
tt('thm/binary_ieee/float_value_size_def_e2', def, (('const/binary_ieee/float_value_size' 'const/binary_ieee/NaN') = 'const/num/0')).
tt('thm/binary_ieee/datatype_float_value_', ax, (![float_value : (('type/realax/real' > 'type/binary_ieee/float_value') > ('type/binary_ieee/float_value' > ('type/binary_ieee/float_value' > $o)))]: (('const/bool/DATATYPE' $o) (float_value 'const/binary_ieee/Float' 'const/binary_ieee/Infinity' 'const/binary_ieee/NaN')))).
tt('thm/binary_ieee/float_value_11_', ax, (![a : 'type/realax/real', 'a\'' : 'type/realax/real']: ((('const/binary_ieee/Float' a) = ('const/binary_ieee/Float' 'a\'')) = (a = 'a\'')))).
tt('thm/binary_ieee/float_value_distinct_0', ax, (![a : 'type/realax/real']: (~ (('const/binary_ieee/Float' a) = 'const/binary_ieee/Infinity')))).
tt('thm/binary_ieee/float_value_distinct_1', ax, (![a : 'type/realax/real']: (~ (('const/binary_ieee/Float' a) = 'const/binary_ieee/NaN')))).
tt('thm/binary_ieee/float_value_distinct_e2', ax, (~ ('const/binary_ieee/Infinity' = 'const/binary_ieee/NaN'))).
tt('thm/binary_ieee/float_value_case_cong_', ax, ![A : $t]: (!['v1\'' : A, 'v\'' : A, 'f\'' : ('type/realax/real' > A), M : 'type/binary_ieee/float_value', 'M\'' : 'type/binary_ieee/float_value', f : ('type/realax/real' > A), v : A, v1 : A]: (((M = 'M\'') & ((![a : 'type/realax/real']: (('M\'' = ('const/binary_ieee/Float' a)) => ((f a) = ('f\'' a)))) & ((('M\'' = 'const/binary_ieee/Infinity') => (v = 'v\'')) & (('M\'' = 'const/binary_ieee/NaN') => (v1 = 'v1\''))))) => ((('const/binary_ieee/float_value_CASE' A) M f v v1) = (('const/binary_ieee/float_value_CASE' A) 'M\'' 'f\'' 'v\'' 'v1\''))))).
tt('thm/binary_ieee/float_value_nchotomy_', ax, (![ff : 'type/binary_ieee/float_value']: ((?[r : 'type/realax/real']: (ff = ('const/binary_ieee/Float' r))) | ((ff = 'const/binary_ieee/Infinity') | (ff = 'const/binary_ieee/NaN'))))).
tt('thm/binary_ieee/float_value_Axiom_', ax, ![A : $t]: (![f0 : ('type/realax/real' > A), f1 : A, f2 : A]: (?[fn : ('type/binary_ieee/float_value' > A)]: ((![a : 'type/realax/real']: ((fn ('const/binary_ieee/Float' a)) = (f0 a))) & (((fn 'const/binary_ieee/Infinity') = f1) & ((fn 'const/binary_ieee/NaN') = f2)))))).
tt('thm/binary_ieee/float_value_induction_', ax, (![P : ('type/binary_ieee/float_value' > $o)]: (((![r : 'type/realax/real']: (P ('const/binary_ieee/Float' r))) & ((P 'const/binary_ieee/Infinity') & (P 'const/binary_ieee/NaN'))) => (![f : 'type/binary_ieee/float_value']: (P f))))).
tt('thm/binary_ieee/float_to_real_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_to_real' T W) x) = (('const/bool/COND' 'type/realax/real') ((('const/binary_ieee/float_Exponent' T W) x) = (('const/words/n2w' W) 'const/num/0')) ('const/realax/real_mul' ('const/realax/real_mul' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/words/w2n' 'type/one/one') (('const/binary_ieee/float_Sign' T W) x))) ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/words/INT_MAX' W) ('const/bool/the_value' W))))) ('const/real/#slash#' ('const/real/real_of_num' (('const/words/w2n' T) (('const/binary_ieee/float_Significand' T W) x))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/fcp/dimindex' T) ('const/bool/the_value' T))))) ('const/realax/real_mul' ('const/realax/real_mul' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/words/w2n' 'type/one/one') (('const/binary_ieee/float_Sign' T W) x))) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/words/w2n' W) (('const/binary_ieee/float_Exponent' T W) x))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/words/INT_MAX' W) ('const/bool/the_value' W))))) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/#slash#' ('const/real/real_of_num' (('const/words/w2n' T) (('const/binary_ieee/float_Significand' T W) x))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/fcp/dimindex' T) ('const/bool/the_value' T)))))))))).
tt('thm/binary_ieee/float_value_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_value' T W) x) = (('const/bool/COND' 'type/binary_ieee/float_value') ((('const/binary_ieee/float_Exponent' T W) x) = ('const/words/word_T' W)) (('const/bool/COND' 'type/binary_ieee/float_value') ((('const/binary_ieee/float_Significand' T W) x) = (('const/words/n2w' T) 'const/num/0')) 'const/binary_ieee/Infinity' 'const/binary_ieee/NaN') ('const/binary_ieee/Float' (('const/binary_ieee/float_to_real' T W) x)))))).
tt('thm/binary_ieee/float_is_nan_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_nan' T W) x) = (('const/binary_ieee/float_value_CASE' $o) (('const/binary_ieee/float_value' T W) x) (^[v1 : 'type/realax/real']: $false) $false $true)))).
tt('thm/binary_ieee/float_is_infinite_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_infinite' T W) x) = (('const/binary_ieee/float_value_CASE' $o) (('const/binary_ieee/float_value' T W) x) (^[v1 : 'type/realax/real']: $false) $true $false)))).
tt('thm/binary_ieee/float_is_normal_def_', def, ![W : $t, T : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_normal' T W) x) = ((~ ((('const/binary_ieee/float_Exponent' T W) x) = (('const/words/n2w' W) 'const/num/0'))) & (~ ((('const/binary_ieee/float_Exponent' T W) x) = ('const/words/word_T' W))))))).
tt('thm/binary_ieee/float_is_subnormal_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_subnormal' T W) x) = (((('const/binary_ieee/float_Exponent' T W) x) = (('const/words/n2w' W) 'const/num/0')) & (~ ((('const/binary_ieee/float_Significand' T W) x) = (('const/words/n2w' T) 'const/num/0'))))))).
tt('thm/binary_ieee/float_is_zero_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_zero' T W) x) = (('const/binary_ieee/float_value_CASE' $o) (('const/binary_ieee/float_value' T W) x) (^[r : 'type/realax/real']: (r = ('const/real/real_of_num' 'const/num/0'))) $false $false)))).
tt('thm/binary_ieee/float_is_finite_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_finite' T W) x) = (('const/binary_ieee/float_value_CASE' $o) (('const/binary_ieee/float_value' T W) x) (^[v1 : 'type/realax/real']: $true) $false $false)))).
tt('thm/binary_ieee/float_is_integral_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_is_integral' T W) x) = (('const/binary_ieee/float_value_CASE' $o) (('const/binary_ieee/float_value' T W) x) (^[r : 'type/realax/real']: (?[n : 'type/num/num']: (('const/real/abs' r) = ('const/real/real_of_num' n)))) $false $false)))).
tt('thm/binary_ieee/float_negate_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_negate' T W) x) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/word_1comp' 'type/one/one') (('const/binary_ieee/float_Sign' T W) x))) x)))).
tt('thm/binary_ieee/float_abs_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_abs' T W) x) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') 'const/num/0')) x)))).
tt('thm/binary_ieee/float_plus_infinity_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) ('const/words/word_T' W)) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) (('const/words/n2w' T) 'const/num/0')) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))).
tt('thm/binary_ieee/float_plus_zero_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) (('const/words/n2w' W) 'const/num/0')) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) (('const/words/n2w' T) 'const/num/0')) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))).
tt('thm/binary_ieee/float_top_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) (('const/words/word_sub' W) ('const/words/word_T' W) (('const/words/n2w' W) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) ('const/words/word_T' T)) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))).
tt('thm/binary_ieee/float_plus_min_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) (('const/words/n2w' W) 'const/num/0')) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) (('const/words/n2w' T) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))).
tt('thm/binary_ieee/float_minus_infinity_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_minus_zero_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_bottom_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_minus_min_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_some_nan_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/min/@' ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/binary_ieee/float_is_nan' T W) a))))).
tt('thm/binary_ieee/rounding_TY_DEF_', def, (?[rep : ('type/binary_ieee/rounding' > 'type/num/num')]: (('const/bool/TYPE_DEFINITION' 'type/num/num' 'type/binary_ieee/rounding') (^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) rep))).
tt('thm/binary_ieee/rounding_BIJ_0', def, (![a : 'type/binary_ieee/rounding']: (('const/binary_ieee/num2rounding' ('const/binary_ieee/rounding2num' a)) = a))).
tt('thm/binary_ieee/rounding_BIJ_e1', def, (![r : 'type/num/num']: (((^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) r) = (('const/binary_ieee/rounding2num' ('const/binary_ieee/num2rounding' r)) = r)))).
tt('thm/binary_ieee/num2rounding_rounding2num_', ax, (![a : 'type/binary_ieee/rounding']: (('const/binary_ieee/num2rounding' ('const/binary_ieee/rounding2num' a)) = a))).
tt('thm/binary_ieee/rounding2num_num2rounding_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (('const/binary_ieee/rounding2num' ('const/binary_ieee/num2rounding' r)) = r)))).
tt('thm/binary_ieee/num2rounding_11_', ax, (![r : 'type/num/num', 'r\'' : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (('const/prim_rec/<' 'r\'' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => ((('const/binary_ieee/num2rounding' r) = ('const/binary_ieee/num2rounding' 'r\'')) = (r = 'r\'')))))).
tt('thm/binary_ieee/rounding2num_11_', ax, (![a : 'type/binary_ieee/rounding', 'a\'' : 'type/binary_ieee/rounding']: ((('const/binary_ieee/rounding2num' a) = ('const/binary_ieee/rounding2num' 'a\'')) = (a = 'a\'')))).
tt('thm/binary_ieee/num2rounding_ONTO_', ax, (![a : 'type/binary_ieee/rounding']: (?[r : 'type/num/num']: ((a = ('const/binary_ieee/num2rounding' r)) & ('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/binary_ieee/rounding2num_ONTO_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (?[a : 'type/binary_ieee/rounding']: (r = ('const/binary_ieee/rounding2num' a)))))).
tt('thm/binary_ieee/num2rounding_thm_0', ax, (('const/binary_ieee/num2rounding' 'const/num/0') = 'const/binary_ieee/roundTiesToEven')).
tt('thm/binary_ieee/num2rounding_thm_1', ax, (('const/binary_ieee/num2rounding' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = 'const/binary_ieee/roundTowardPositive')).
tt('thm/binary_ieee/num2rounding_thm_2', ax, (('const/binary_ieee/num2rounding' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = 'const/binary_ieee/roundTowardNegative')).
tt('thm/binary_ieee/num2rounding_thm_e3', ax, (('const/binary_ieee/num2rounding' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = 'const/binary_ieee/roundTowardZero')).
tt('thm/binary_ieee/rounding2num_thm_0', ax, (('const/binary_ieee/rounding2num' 'const/binary_ieee/roundTiesToEven') = 'const/num/0')).
tt('thm/binary_ieee/rounding2num_thm_1', ax, (('const/binary_ieee/rounding2num' 'const/binary_ieee/roundTowardPositive') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/binary_ieee/rounding2num_thm_2', ax, (('const/binary_ieee/rounding2num' 'const/binary_ieee/roundTowardNegative') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))).
tt('thm/binary_ieee/rounding2num_thm_e3', ax, (('const/binary_ieee/rounding2num' 'const/binary_ieee/roundTowardZero') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/rounding_EQ_rounding_', ax, (![a : 'type/binary_ieee/rounding', 'a\'' : 'type/binary_ieee/rounding']: ((a = 'a\'') = (('const/binary_ieee/rounding2num' a) = ('const/binary_ieee/rounding2num' 'a\''))))).
tt('thm/binary_ieee/rounding_size_def_', def, (![x : 'type/binary_ieee/rounding']: (('const/binary_ieee/rounding_size' x) = 'const/num/0'))).
tt('thm/binary_ieee/rounding_CASE_', def, ![A : $t]: (![x : 'type/binary_ieee/rounding', v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/rounding_CASE' A) x v0 v1 v2 v3) = ((^[m : 'type/num/num']: (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) v0 (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v1 (('const/bool/COND' A) (m = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v2 v3)))) ('const/binary_ieee/rounding2num' x))))).
tt('thm/binary_ieee/rounding_case_def_0', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/rounding_CASE' A) 'const/binary_ieee/roundTiesToEven' v0 v1 v2 v3) = v0))).
tt('thm/binary_ieee/rounding_case_def_1', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/rounding_CASE' A) 'const/binary_ieee/roundTowardPositive' v0 v1 v2 v3) = v1))).
tt('thm/binary_ieee/rounding_case_def_2', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/rounding_CASE' A) 'const/binary_ieee/roundTowardNegative' v0 v1 v2 v3) = v2))).
tt('thm/binary_ieee/rounding_case_def_e3', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/rounding_CASE' A) 'const/binary_ieee/roundTowardZero' v0 v1 v2 v3) = v3))).
tt('thm/binary_ieee/datatype_rounding_', ax, (![rounding : ('type/binary_ieee/rounding' > ('type/binary_ieee/rounding' > ('type/binary_ieee/rounding' > ('type/binary_ieee/rounding' > $o))))]: (('const/bool/DATATYPE' $o) (rounding 'const/binary_ieee/roundTiesToEven' 'const/binary_ieee/roundTowardPositive' 'const/binary_ieee/roundTowardNegative' 'const/binary_ieee/roundTowardZero')))).
tt('thm/binary_ieee/rounding_distinct_0', ax, (~ ('const/binary_ieee/roundTiesToEven' = 'const/binary_ieee/roundTowardPositive'))).
tt('thm/binary_ieee/rounding_distinct_1', ax, (~ ('const/binary_ieee/roundTiesToEven' = 'const/binary_ieee/roundTowardNegative'))).
tt('thm/binary_ieee/rounding_distinct_2', ax, (~ ('const/binary_ieee/roundTiesToEven' = 'const/binary_ieee/roundTowardZero'))).
tt('thm/binary_ieee/rounding_distinct_3', ax, (~ ('const/binary_ieee/roundTowardPositive' = 'const/binary_ieee/roundTowardNegative'))).
tt('thm/binary_ieee/rounding_distinct_4', ax, (~ ('const/binary_ieee/roundTowardPositive' = 'const/binary_ieee/roundTowardZero'))).
tt('thm/binary_ieee/rounding_distinct_e5', ax, (~ ('const/binary_ieee/roundTowardNegative' = 'const/binary_ieee/roundTowardZero'))).
tt('thm/binary_ieee/rounding_case_cong_', ax, ![A : $t]: (!['v3\'' : A, 'v2\'' : A, 'v1\'' : A, 'v0\'' : A, M : 'type/binary_ieee/rounding', 'M\'' : 'type/binary_ieee/rounding', v0 : A, v1 : A, v2 : A, v3 : A]: (((M = 'M\'') & ((('M\'' = 'const/binary_ieee/roundTiesToEven') => (v0 = 'v0\'')) & ((('M\'' = 'const/binary_ieee/roundTowardPositive') => (v1 = 'v1\'')) & ((('M\'' = 'const/binary_ieee/roundTowardNegative') => (v2 = 'v2\'')) & (('M\'' = 'const/binary_ieee/roundTowardZero') => (v3 = 'v3\'')))))) => ((('const/binary_ieee/rounding_CASE' A) M v0 v1 v2 v3) = (('const/binary_ieee/rounding_CASE' A) 'M\'' 'v0\'' 'v1\'' 'v2\'' 'v3\''))))).
tt('thm/binary_ieee/rounding_nchotomy_', ax, (![a : 'type/binary_ieee/rounding']: ((a = 'const/binary_ieee/roundTiesToEven') | ((a = 'const/binary_ieee/roundTowardPositive') | ((a = 'const/binary_ieee/roundTowardNegative') | (a = 'const/binary_ieee/roundTowardZero')))))).
tt('thm/binary_ieee/rounding_Axiom_', ax, ![A : $t]: (![x0 : A, x1 : A, x2 : A, x3 : A]: (?[f : ('type/binary_ieee/rounding' > A)]: (((f 'const/binary_ieee/roundTiesToEven') = x0) & (((f 'const/binary_ieee/roundTowardPositive') = x1) & (((f 'const/binary_ieee/roundTowardNegative') = x2) & ((f 'const/binary_ieee/roundTowardZero') = x3))))))).
tt('thm/binary_ieee/rounding_induction_', ax, (![P : ('type/binary_ieee/rounding' > $o)]: (((P 'const/binary_ieee/roundTiesToEven') & ((P 'const/binary_ieee/roundTowardNegative') & ((P 'const/binary_ieee/roundTowardPositive') & (P 'const/binary_ieee/roundTowardZero')))) => (![a : 'type/binary_ieee/rounding']: (P a))))).
tt('thm/binary_ieee/is_closest_def_', def, ![A : $t, B : $t]: (![s : (('type/binary_ieee/float' A B) > $o), x : 'type/realax/real', a : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/is_closest' A B) s x a) = ((('const/bool/IN' ('type/binary_ieee/float' A B)) a s) & (![b : ('type/binary_ieee/float' A B)]: ((('const/bool/IN' ('type/binary_ieee/float' A B)) b s) => ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' A B) a) x)) ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' A B) b) x))))))))).
tt('thm/binary_ieee/closest_such_def_', def, ![A : $t, B : $t]: (![p : (('type/binary_ieee/float' A B) > $o), s : (('type/binary_ieee/float' A B) > $o), x : 'type/realax/real']: ((('const/binary_ieee/closest_such' A B) p s x) = (('const/min/@' ('type/binary_ieee/float' A B)) (^[a : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/is_closest' A B) s x a) & (![b : ('type/binary_ieee/float' A B)]: (((('const/binary_ieee/is_closest' A B) s x b) & (p b)) => (p a))))))))).
tt('thm/binary_ieee/closest_def_', def, ![A : $t, B : $t]: (('const/binary_ieee/closest' A B) = (('const/binary_ieee/closest_such' A B) (('const/combin/K' $o ('type/binary_ieee/float' A B)) $true)))).
tt('thm/binary_ieee/largest_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = ('const/realax/real_mul' ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/-' (('const/words/UINT_MAX' W) ('const/bool/the_value' W)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/words/INT_MAX' W) ('const/bool/the_value' W)))) ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/fcp/dimindex' T) ('const/bool/the_value' T)))))))).
tt('thm/binary_ieee/threshold_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = ('const/realax/real_mul' ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/-' (('const/words/UINT_MAX' W) ('const/bool/the_value' W)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/words/INT_MAX' W) ('const/bool/the_value' W)))) ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' (('const/fcp/dimindex' T) ('const/bool/the_value' T))))))))).
tt('thm/binary_ieee/ULP_primitive_def_', def, ![T : $t, W : $t]: (('const/binary_ieee/ULP' T W) = (('const/relation/WFREC' ('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) 'type/realax/real') (('const/min/@' (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > $o))) (^[R : (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > $o))]: (('const/relation/WF' ('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T))) R))) (^[ULP : (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > 'type/realax/real'), a : ('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T))]: (('const/pair/pair_CASE' 'type/realax/real' ('type/fcp/cart' $o W) ('type/bool/itself' T)) a (^[e : ('type/fcp/cart' $o W), v1 : ('type/bool/itself' T)]: (('const/combin/I' 'type/realax/real') ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' 'type/num/num') (e = (('const/words/n2w' W) 'const/num/0')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/words/w2n' W) e))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/+' (('const/words/INT_MAX' W) ('const/bool/the_value' W)) (('const/fcp/dimindex' T) ('const/bool/the_value' T)))))))))))).
tt('thm/binary_ieee/ULP_ind_', ax, ![T : $t, W : $t]: (![P : (('type/pair/prod' ('type/fcp/cart' $o W) ('type/bool/itself' T)) > $o)]: ((![e : ('type/fcp/cart' $o W)]: (P (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) e ('const/bool/the_value' T)))) => (![v : ('type/fcp/cart' $o W), v1 : ('type/bool/itself' T)]: (P (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) v v1)))))).
tt('thm/binary_ieee/ULP_def_', ax, ![T : $t, W : $t]: (![e : ('type/fcp/cart' $o W)]: ((('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) e ('const/bool/the_value' T))) = ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' 'type/num/num') (e = (('const/words/n2w' W) 'const/num/0')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/words/w2n' W) e))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/+' (('const/words/INT_MAX' W) ('const/bool/the_value' W)) (('const/fcp/dimindex' T) ('const/bool/the_value' T)))))))).
tt('thm/binary_ieee/ulp_def_', def, ![T : $t, W : $t]: ((('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/words/n2w' W) 'const/num/0') ('const/bool/the_value' T))))).
tt('thm/binary_ieee/round_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : 'type/realax/real']: ((('const/binary_ieee/round' T W) mode x) = (('const/binary_ieee/rounding_CASE' ('type/binary_ieee/float' T W)) mode (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_lte' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_ge' x t) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest_such' T W) (^[a : ('type/binary_ieee/float' T W)]: (~ (('const/words/word_lsb' T) (('const/binary_ieee/float_Significand' T W) a)))) ('const/binary_ieee/float_is_finite' T W) x)))) (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/realax/real_lt' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_gt' x t) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest' T W) (('const/pred_set/GSPEC' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/pair/,' ('type/binary_ieee/float' T W) $o) a ((('const/binary_ieee/float_is_finite' T W) a) & ('const/real/real_ge' (('const/binary_ieee/float_to_real' T W) a) x))))) x)))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/realax/real_lt' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_gt' x t) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest' T W) (('const/pred_set/GSPEC' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/pair/,' ('type/binary_ieee/float' T W) $o) a ((('const/binary_ieee/float_is_finite' T W) a) & ('const/real/real_lte' (('const/binary_ieee/float_to_real' T W) a) x))))) x)))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/realax/real_lt' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_gt' x t) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest' T W) (('const/pred_set/GSPEC' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/pair/,' ('type/binary_ieee/float' T W) $o) a ((('const/binary_ieee/float_is_finite' T W) a) & ('const/real/real_lte' ('const/real/abs' (('const/binary_ieee/float_to_real' T W) a)) ('const/real/abs' x)))))) x)))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/integral_round_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : 'type/realax/real']: ((('const/binary_ieee/integral_round' T W) mode x) = (('const/binary_ieee/rounding_CASE' ('type/binary_ieee/float' T W)) mode (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_lte' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_ge' x t) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest_such' T W) (^[a : ('type/binary_ieee/float' T W)]: (?[n : 'type/num/num']: (('const/arithmetic/EVEN' n) & (('const/real/abs' (('const/binary_ieee/float_to_real' T W) a)) = ('const/real/real_of_num' n))))) ('const/binary_ieee/float_is_integral' T W) x)))) (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/realax/real_lt' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_gt' x t) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest' T W) (('const/pred_set/GSPEC' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/pair/,' ('type/binary_ieee/float' T W) $o) a ((('const/binary_ieee/float_is_integral' T W) a) & ('const/real/real_ge' (('const/binary_ieee/float_to_real' T W) a) x))))) x)))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/realax/real_lt' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_gt' x t) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest' T W) (('const/pred_set/GSPEC' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/pair/,' ('type/binary_ieee/float' T W) $o) a ((('const/binary_ieee/float_is_integral' T W) a) & ('const/real/real_lte' (('const/binary_ieee/float_to_real' T W) a) x))))) x)))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/bool/LET' 'type/realax/real' ('type/binary_ieee/float' T W)) (^[t : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/realax/real_lt' x ('const/realax/real_neg' t)) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('const/real/real_gt' x t) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/closest' T W) (('const/pred_set/GSPEC' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[a : ('type/binary_ieee/float' T W)]: (('const/pair/,' ('type/binary_ieee/float' T W) $o) a ((('const/binary_ieee/float_is_integral' T W) a) & ('const/real/real_lte' ('const/real/abs' (('const/binary_ieee/float_to_real' T W) a)) ('const/real/abs' x)))))) x)))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/float_round_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', toneg : $o, r : 'type/realax/real']: ((('const/binary_ieee/float_round' T W) mode toneg r) = (('const/bool/LET' ('type/binary_ieee/float' T W) ('type/binary_ieee/float' T W)) (^[x : ('type/binary_ieee/float' T W)]: (('const/bool/COND' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_is_zero' T W) x) (('const/bool/COND' ('type/binary_ieee/float' T W)) toneg (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) x)) (('const/binary_ieee/round' T W) mode r))))).
tt('thm/binary_ieee/float_round_to_integral_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_round_to_integral' T W) mode x) = (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_value' T W) x) (^[r : 'type/realax/real']: (('const/binary_ieee/integral_round' T W) mode r)) x x)))).
tt('thm/binary_ieee/float_sqrt_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_sqrt' T W) mode x) = (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_value' T W) x) (^[r : 'type/realax/real']: (('const/binary_ieee/float_round' T W) mode ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/transc/sqrt' r))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_add_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_add' T W) mode x y) = (('const/pair/pair_CASE' ('type/binary_ieee/float' T W) 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/pair/,' 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/binary_ieee/float_value' T W) x) (('const/binary_ieee/float_value' T W) y)) (^[v : 'type/binary_ieee/float_value', v1 : 'type/binary_ieee/float_value']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v (^[r1 : 'type/realax/real']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[r2 : 'type/realax/real']: (('const/binary_ieee/float_round' T W) mode (('const/bool/COND' $o) ((r1 = ('const/real/real_of_num' 'const/num/0')) & ((r2 = ('const/real/real_of_num' 'const/num/0')) & ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)))) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (mode = 'const/binary_ieee/roundTowardNegative')) ('const/realax/real_add' r1 r2))) y (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[v7 : 'type/realax/real']: x) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) x (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_sub_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_sub' T W) mode x y) = (('const/pair/pair_CASE' ('type/binary_ieee/float' T W) 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/pair/,' 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/binary_ieee/float_value' T W) x) (('const/binary_ieee/float_value' T W) y)) (^[v : 'type/binary_ieee/float_value', v1 : 'type/binary_ieee/float_value']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v (^[r1 : 'type/realax/real']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[r2 : 'type/realax/real']: (('const/binary_ieee/float_round' T W) mode (('const/bool/COND' $o) ((r1 = ('const/real/real_of_num' 'const/num/0')) & ((r2 = ('const/real/real_of_num' 'const/num/0')) & (~ ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y))))) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (mode = 'const/binary_ieee/roundTowardNegative')) ('const/real/real_sub' r1 r2))) (('const/binary_ieee/float_negate' T W) y) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[v7 : 'type/realax/real']: x) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_mul_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_mul' T W) mode x y) = (('const/pair/pair_CASE' ('type/binary_ieee/float' T W) 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/pair/,' 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/binary_ieee/float_value' T W) x) (('const/binary_ieee/float_value' T W) y)) (^[v : 'type/binary_ieee/float_value', v1 : 'type/binary_ieee/float_value']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v (^['r\'' : 'type/realax/real']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[r2 : 'type/realax/real']: (('const/binary_ieee/float_round' T W) mode (~ ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y))) ('const/realax/real_mul' 'r\'' r2))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ('r\'' = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[r : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) (r = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_div_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_div' T W) mode x y) = (('const/pair/pair_CASE' ('type/binary_ieee/float' T W) 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/pair/,' 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/binary_ieee/float_value' T W) x) (('const/binary_ieee/float_value' T W) y)) (^[v : 'type/binary_ieee/float_value', v1 : 'type/binary_ieee/float_value']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v (^[r1 : 'type/realax/real']: (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[r2 : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) (r2 = ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' ('type/binary_ieee/float' T W)) (r1 = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_round' T W) mode (~ ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y))) ('const/real/#slash#' r1 r2)))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_value_CASE' ('type/binary_ieee/float' T W)) v1 (^[v7 : 'type/realax/real']: (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_mul_add_def_', def, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W), z : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_mul_add' T W) mode x y z) = (('const/bool/LET' ('type/fcp/cart' $o 'type/one/one') ('type/binary_ieee/float' T W)) (^[signP : ('type/fcp/cart' $o 'type/one/one')]: (('const/bool/LET' $o ('type/binary_ieee/float' T W)) (^[infP : $o]: (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_is_nan' T W) x) | ((('const/binary_ieee/float_is_nan' T W) y) | ((('const/binary_ieee/float_is_nan' T W) z) | (((('const/binary_ieee/float_is_infinite' T W) x) & (('const/binary_ieee/float_is_zero' T W) y)) | (((('const/binary_ieee/float_is_zero' T W) x) & (('const/binary_ieee/float_is_infinite' T W) y)) | ((('const/binary_ieee/float_is_infinite' T W) z) & (infP & (~ ((('const/binary_ieee/float_Sign' T W) z) = signP))))))))) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) (((('const/binary_ieee/float_is_infinite' T W) z) & ((('const/binary_ieee/float_Sign' T W) z) = (('const/words/n2w' 'type/one/one') 'const/num/0'))) | (infP & (signP = (('const/words/n2w' 'type/one/one') 'const/num/0')))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) (((('const/binary_ieee/float_is_infinite' T W) z) & ((('const/binary_ieee/float_Sign' T W) z) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) | (infP & (signP = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_is_zero' T W) z) & (((('const/binary_ieee/float_is_zero' T W) x) | (('const/binary_ieee/float_is_zero' T W) y)) & ((('const/binary_ieee/float_Sign' T W) x) = signP))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) (('const/binary_ieee/float_round' T W) mode (mode = 'const/binary_ieee/roundTowardNegative') ('const/realax/real_add' (('const/binary_ieee/float_to_real' T W) z) ('const/realax/real_mul' (('const/binary_ieee/float_to_real' T W) x) (('const/binary_ieee/float_to_real' T W) y))))))))) ((('const/binary_ieee/float_is_infinite' T W) x) | (('const/binary_ieee/float_is_infinite' T W) y)))) (('const/words/word_xor' 'type/one/one') (('const/binary_ieee/float_Sign' T W) x) (('const/binary_ieee/float_Sign' T W) y)))))).
tt('thm/binary_ieee/float_compare_TY_DEF_', def, (?[rep : ('type/binary_ieee/float_compare' > 'type/num/num')]: (('const/bool/TYPE_DEFINITION' 'type/num/num' 'type/binary_ieee/float_compare') (^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) rep))).
tt('thm/binary_ieee/float_compare_BIJ_0', def, (![a : 'type/binary_ieee/float_compare']: (('const/binary_ieee/num2float_compare' ('const/binary_ieee/float_compare2num' a)) = a))).
tt('thm/binary_ieee/float_compare_BIJ_e1', def, (![r : 'type/num/num']: (((^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) r) = (('const/binary_ieee/float_compare2num' ('const/binary_ieee/num2float_compare' r)) = r)))).
tt('thm/binary_ieee/num2float_compare_float_compare2num_', ax, (![a : 'type/binary_ieee/float_compare']: (('const/binary_ieee/num2float_compare' ('const/binary_ieee/float_compare2num' a)) = a))).
tt('thm/binary_ieee/float_compare2num_num2float_compare_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (('const/binary_ieee/float_compare2num' ('const/binary_ieee/num2float_compare' r)) = r)))).
tt('thm/binary_ieee/num2float_compare_11_', ax, (![r : 'type/num/num', 'r\'' : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (('const/prim_rec/<' 'r\'' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => ((('const/binary_ieee/num2float_compare' r) = ('const/binary_ieee/num2float_compare' 'r\'')) = (r = 'r\'')))))).
tt('thm/binary_ieee/float_compare2num_11_', ax, (![a : 'type/binary_ieee/float_compare', 'a\'' : 'type/binary_ieee/float_compare']: ((('const/binary_ieee/float_compare2num' a) = ('const/binary_ieee/float_compare2num' 'a\'')) = (a = 'a\'')))).
tt('thm/binary_ieee/num2float_compare_ONTO_', ax, (![a : 'type/binary_ieee/float_compare']: (?[r : 'type/num/num']: ((a = ('const/binary_ieee/num2float_compare' r)) & ('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/binary_ieee/float_compare2num_ONTO_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (?[a : 'type/binary_ieee/float_compare']: (r = ('const/binary_ieee/float_compare2num' a)))))).
tt('thm/binary_ieee/num2float_compare_thm_0', ax, (('const/binary_ieee/num2float_compare' 'const/num/0') = 'const/binary_ieee/LT')).
tt('thm/binary_ieee/num2float_compare_thm_1', ax, (('const/binary_ieee/num2float_compare' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = 'const/binary_ieee/GT')).
tt('thm/binary_ieee/num2float_compare_thm_2', ax, (('const/binary_ieee/num2float_compare' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = 'const/binary_ieee/EQ')).
tt('thm/binary_ieee/num2float_compare_thm_e3', ax, (('const/binary_ieee/num2float_compare' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = 'const/binary_ieee/UN')).
tt('thm/binary_ieee/float_compare2num_thm_0', ax, (('const/binary_ieee/float_compare2num' 'const/binary_ieee/LT') = 'const/num/0')).
tt('thm/binary_ieee/float_compare2num_thm_1', ax, (('const/binary_ieee/float_compare2num' 'const/binary_ieee/GT') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/binary_ieee/float_compare2num_thm_2', ax, (('const/binary_ieee/float_compare2num' 'const/binary_ieee/EQ') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))).
tt('thm/binary_ieee/float_compare2num_thm_e3', ax, (('const/binary_ieee/float_compare2num' 'const/binary_ieee/UN') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_compare_EQ_float_compare_', ax, (![a : 'type/binary_ieee/float_compare', 'a\'' : 'type/binary_ieee/float_compare']: ((a = 'a\'') = (('const/binary_ieee/float_compare2num' a) = ('const/binary_ieee/float_compare2num' 'a\''))))).
tt('thm/binary_ieee/float_compare_size_def_', def, (![x : 'type/binary_ieee/float_compare']: (('const/binary_ieee/float_compare_size' x) = 'const/num/0'))).
tt('thm/binary_ieee/float_compare_CASE_', def, ![A : $t]: (![x : 'type/binary_ieee/float_compare', v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/float_compare_CASE' A) x v0 v1 v2 v3) = ((^[m : 'type/num/num']: (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) v0 (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v1 (('const/bool/COND' A) (m = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v2 v3)))) ('const/binary_ieee/float_compare2num' x))))).
tt('thm/binary_ieee/float_compare_case_def_0', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/float_compare_CASE' A) 'const/binary_ieee/LT' v0 v1 v2 v3) = v0))).
tt('thm/binary_ieee/float_compare_case_def_1', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/float_compare_CASE' A) 'const/binary_ieee/GT' v0 v1 v2 v3) = v1))).
tt('thm/binary_ieee/float_compare_case_def_2', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/float_compare_CASE' A) 'const/binary_ieee/EQ' v0 v1 v2 v3) = v2))).
tt('thm/binary_ieee/float_compare_case_def_e3', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/binary_ieee/float_compare_CASE' A) 'const/binary_ieee/UN' v0 v1 v2 v3) = v3))).
tt('thm/binary_ieee/datatype_float_compare_', ax, (![float_compare : ('type/binary_ieee/float_compare' > ('type/binary_ieee/float_compare' > ('type/binary_ieee/float_compare' > ('type/binary_ieee/float_compare' > $o))))]: (('const/bool/DATATYPE' $o) (float_compare 'const/binary_ieee/LT' 'const/binary_ieee/GT' 'const/binary_ieee/EQ' 'const/binary_ieee/UN')))).
tt('thm/binary_ieee/float_compare_distinct_0', ax, (~ ('const/binary_ieee/LT' = 'const/binary_ieee/GT'))).
tt('thm/binary_ieee/float_compare_distinct_1', ax, (~ ('const/binary_ieee/LT' = 'const/binary_ieee/EQ'))).
tt('thm/binary_ieee/float_compare_distinct_2', ax, (~ ('const/binary_ieee/LT' = 'const/binary_ieee/UN'))).
tt('thm/binary_ieee/float_compare_distinct_3', ax, (~ ('const/binary_ieee/GT' = 'const/binary_ieee/EQ'))).
tt('thm/binary_ieee/float_compare_distinct_4', ax, (~ ('const/binary_ieee/GT' = 'const/binary_ieee/UN'))).
tt('thm/binary_ieee/float_compare_distinct_e5', ax, (~ ('const/binary_ieee/EQ' = 'const/binary_ieee/UN'))).
tt('thm/binary_ieee/float_compare_case_cong_', ax, ![A : $t]: (!['v3\'' : A, 'v2\'' : A, 'v1\'' : A, 'v0\'' : A, M : 'type/binary_ieee/float_compare', 'M\'' : 'type/binary_ieee/float_compare', v0 : A, v1 : A, v2 : A, v3 : A]: (((M = 'M\'') & ((('M\'' = 'const/binary_ieee/LT') => (v0 = 'v0\'')) & ((('M\'' = 'const/binary_ieee/GT') => (v1 = 'v1\'')) & ((('M\'' = 'const/binary_ieee/EQ') => (v2 = 'v2\'')) & (('M\'' = 'const/binary_ieee/UN') => (v3 = 'v3\'')))))) => ((('const/binary_ieee/float_compare_CASE' A) M v0 v1 v2 v3) = (('const/binary_ieee/float_compare_CASE' A) 'M\'' 'v0\'' 'v1\'' 'v2\'' 'v3\''))))).
tt('thm/binary_ieee/float_compare_nchotomy_', ax, (![a : 'type/binary_ieee/float_compare']: ((a = 'const/binary_ieee/LT') | ((a = 'const/binary_ieee/GT') | ((a = 'const/binary_ieee/EQ') | (a = 'const/binary_ieee/UN')))))).
tt('thm/binary_ieee/float_compare_Axiom_', ax, ![A : $t]: (![x0 : A, x1 : A, x2 : A, x3 : A]: (?[f : ('type/binary_ieee/float_compare' > A)]: (((f 'const/binary_ieee/LT') = x0) & (((f 'const/binary_ieee/GT') = x1) & (((f 'const/binary_ieee/EQ') = x2) & ((f 'const/binary_ieee/UN') = x3))))))).
tt('thm/binary_ieee/float_compare_induction_', ax, (![P : ('type/binary_ieee/float_compare' > $o)]: (((P 'const/binary_ieee/EQ') & ((P 'const/binary_ieee/GT') & ((P 'const/binary_ieee/LT') & (P 'const/binary_ieee/UN')))) => (![a : 'type/binary_ieee/float_compare']: (P a))))).
tt('thm/binary_ieee/float_compare_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_compare' T W) x y) = (('const/pair/pair_CASE' 'type/binary_ieee/float_compare' 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/pair/,' 'type/binary_ieee/float_value' 'type/binary_ieee/float_value') (('const/binary_ieee/float_value' T W) x) (('const/binary_ieee/float_value' T W) y)) (^[v : 'type/binary_ieee/float_value', v1 : 'type/binary_ieee/float_value']: (('const/binary_ieee/float_value_CASE' 'type/binary_ieee/float_compare') v (^[r1 : 'type/realax/real']: (('const/binary_ieee/float_value_CASE' 'type/binary_ieee/float_compare') v1 (^[r2 : 'type/realax/real']: (('const/bool/COND' 'type/binary_ieee/float_compare') ('const/realax/real_lt' r1 r2) 'const/binary_ieee/LT' (('const/bool/COND' 'type/binary_ieee/float_compare') (r1 = r2) 'const/binary_ieee/EQ' 'const/binary_ieee/GT'))) (('const/bool/COND' 'type/binary_ieee/float_compare') ((('const/binary_ieee/float_Sign' T W) y) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/binary_ieee/GT' 'const/binary_ieee/LT') 'const/binary_ieee/UN')) (('const/binary_ieee/float_value_CASE' 'type/binary_ieee/float_compare') v1 (^[v7 : 'type/realax/real']: (('const/bool/COND' 'type/binary_ieee/float_compare') ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/binary_ieee/LT' 'const/binary_ieee/GT')) (('const/bool/COND' 'type/binary_ieee/float_compare') ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) 'const/binary_ieee/EQ' (('const/bool/COND' 'type/binary_ieee/float_compare') ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/binary_ieee/LT' 'const/binary_ieee/GT')) 'const/binary_ieee/UN') 'const/binary_ieee/UN')))))).
tt('thm/binary_ieee/float_less_than_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_less_than' T W) x y) = ((('const/binary_ieee/float_compare' T W) x y) = 'const/binary_ieee/LT')))).
tt('thm/binary_ieee/float_less_equal_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_less_equal' T W) x y) = (('const/binary_ieee/float_compare_CASE' $o) (('const/binary_ieee/float_compare' T W) x y) $true $false $true $false)))).
tt('thm/binary_ieee/float_greater_than_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_greater_than' T W) x y) = ((('const/binary_ieee/float_compare' T W) x y) = 'const/binary_ieee/GT')))).
tt('thm/binary_ieee/float_greater_equal_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_greater_equal' T W) x y) = (('const/binary_ieee/float_compare_CASE' $o) (('const/binary_ieee/float_compare' T W) x y) $false $true $true $false)))).
tt('thm/binary_ieee/float_equal_def_', def, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_equal' T W) x y) = ((('const/binary_ieee/float_compare' T W) x y) = 'const/binary_ieee/EQ')))).
tt('thm/binary_ieee/exponent_boundary_def_', def, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/exponent_boundary' T W) y x) = (((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) & (((('const/words/w2n' W) (('const/binary_ieee/float_Exponent' T W) x)) = ('const/arithmetic/+' (('const/words/w2n' W) (('const/binary_ieee/float_Exponent' T W) y)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) & ((~ ((('const/binary_ieee/float_Exponent' T W) x) = (('const/words/n2w' W) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (((('const/binary_ieee/float_Significand' T W) y) = (('const/words/word_2comp' T) (('const/words/n2w' T) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & ((('const/binary_ieee/float_Significand' T W) x) = (('const/words/n2w' T) 'const/num/0'))))))))).
tt('thm/binary_ieee/zero_lt_twopow_', ax, (![n : 'type/num/num']: ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))).
tt('thm/binary_ieee/zero_le_twopow_', ax, (![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))).
tt('thm/binary_ieee/zero_neq_twopow_', ax, (![n : 'type/num/num']: (~ (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/binary_ieee/zero_le_pos_div_twopow_', ax, (![m : 'type/num/num', n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' m) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n))))).
tt('thm/binary_ieee/div_eq0_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') b) => ((('const/real/#slash#' a b) = ('const/real/real_of_num' 'const/num/0')) = (a = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/binary_ieee/exp_ge2_', ax, (![b : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) b)) = ('const/arithmetic/<=' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b)))).
tt('thm/binary_ieee/exp_gt2_', ax, (![b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) b)) = ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b)))).
tt('thm/binary_ieee/le2_', ax, (![n : 'type/realax/real', m : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) & ('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) m)) => ('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/realax/real_mul' n m))))).
tt('thm/binary_ieee/float_components_0', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') 'const/num/0'))).
tt('thm/binary_ieee/float_components_1', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/words/word_T' W))).
tt('thm/binary_ieee/float_components_2', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) 'const/num/0'))).
tt('thm/binary_ieee/float_components_3', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_components_4', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/words/word_T' W))).
tt('thm/binary_ieee/float_components_5', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) 'const/num/0'))).
tt('thm/binary_ieee/float_components_6', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') 'const/num/0'))).
tt('thm/binary_ieee/float_components_7', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' W) 'const/num/0'))).
tt('thm/binary_ieee/float_components_8', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) 'const/num/0'))).
tt('thm/binary_ieee/float_components_9', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_components_10', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' W) 'const/num/0'))).
tt('thm/binary_ieee/float_components_11', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) 'const/num/0'))).
tt('thm/binary_ieee/float_components_12', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') 'const/num/0'))).
tt('thm/binary_ieee/float_components_13', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' W) 'const/num/0'))).
tt('thm/binary_ieee/float_components_14', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_components_15', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_components_16', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' W) 'const/num/0'))).
tt('thm/binary_ieee/float_components_17', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_components_18', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') 'const/num/0'))).
tt('thm/binary_ieee/float_components_19', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/word_sub' W) ('const/words/word_T' W) (('const/words/n2w' W) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/binary_ieee/float_components_20', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/words/word_T' T))).
tt('thm/binary_ieee/float_components_21', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Sign' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/float_components_22', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/word_sub' W) ('const/words/word_T' W) (('const/words/n2w' W) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/binary_ieee/float_components_23', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/words/word_T' T))).
tt('thm/binary_ieee/float_components_24', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_Exponent' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/words/word_T' W))).
tt('thm/binary_ieee/float_components_25', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_Significand' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/words/n2w' T) 'const/num/0')))).
tt('thm/binary_ieee/float_components_26', ax, ![A : $t, B : $t]: (![x : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/float_Sign' A B) (('const/binary_ieee/float_negate' A B) x)) = (('const/words/word_1comp' 'type/one/one') (('const/binary_ieee/float_Sign' A B) x))))).
tt('thm/binary_ieee/float_components_27', ax, ![C : $t, D : $t]: (![x : ('type/binary_ieee/float' C D)]: ((('const/binary_ieee/float_Exponent' C D) (('const/binary_ieee/float_negate' C D) x)) = (('const/binary_ieee/float_Exponent' C D) x)))).
tt('thm/binary_ieee/float_components_e28', ax, ![E : $t, F : $t]: (![x : ('type/binary_ieee/float' E F)]: ((('const/binary_ieee/float_Significand' E F) (('const/binary_ieee/float_negate' E F) x)) = (('const/binary_ieee/float_Significand' E F) x)))).
tt('thm/binary_ieee/float_distinct_0', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_1', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_2', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_3', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_4', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_5', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_6', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_7', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_8', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_9', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_10', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_11', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_12', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_13', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_14', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_15', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_16', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_17', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_18', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_19', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_20', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_21', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_22', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_23', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_24', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_25', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_26', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_27', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_28', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_29', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_30', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_31', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_32', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_33', ax, ![T : $t, W : $t]: (~ ((('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_distinct_e34', ax, ![A : $t, B : $t]: (![x : ('type/binary_ieee/float' A B)]: (~ ((('const/binary_ieee/float_negate' A B) x) = x)))).
tt('thm/binary_ieee/float_values_0', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = 'const/binary_ieee/Infinity')).
tt('thm/binary_ieee/float_values_1', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = 'const/binary_ieee/Infinity')).
tt('thm/binary_ieee/float_values_2', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = 'const/binary_ieee/NaN')).
tt('thm/binary_ieee/float_values_3', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/binary_ieee/Float' ('const/real/real_of_num' 'const/num/0')))).
tt('thm/binary_ieee/float_values_4', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/binary_ieee/Float' ('const/real/real_of_num' 'const/num/0')))).
tt('thm/binary_ieee/float_values_5', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/binary_ieee/Float' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/+' (('const/words/INT_MAX' W) ('const/bool/the_value' W)) (('const/fcp/dimindex' T) ('const/bool/the_value' T)))))))).
tt('thm/binary_ieee/float_values_e6', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_value' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/binary_ieee/Float' ('const/real/#slash#' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/+' (('const/words/INT_MAX' W) ('const/bool/the_value' W)) (('const/fcp/dimindex' T) ('const/bool/the_value' T)))))))).
tt('thm/binary_ieee/zero_to_real_0', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_to_real' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/binary_ieee/zero_to_real_e1', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_to_real' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/binary_ieee/sign_not_zero_', ax, (![s : ('type/fcp/cart' $o 'type/one/one')]: (~ (('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/words/w2n' 'type/one/one') s)) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/binary_ieee/float_sets_0', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_zero' T W) = (('const/pred_set/INSERT' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/pred_set/INSERT' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) ('const/pred_set/EMPTY' ('type/binary_ieee/float' T W)))))).
tt('thm/binary_ieee/float_sets_e1', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_infinite' T W) = (('const/pred_set/INSERT' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/pred_set/INSERT' ('type/binary_ieee/float' T W)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) ('const/pred_set/EMPTY' ('type/binary_ieee/float' T W)))))).
tt('thm/binary_ieee/infinity_properties_0', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_1', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_2', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_3', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_4', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_5', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_6', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_7', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_8', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_9', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_10', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_11', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/infinity_properties_12', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/infinity_properties_e13', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_0', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_1', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_2', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_3', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_4', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_5', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/zero_properties_6', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_7', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_8', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_9', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_10', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_11', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_12', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/zero_properties_e13', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/some_nan_properties_0', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/some_nan_properties_1', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/some_nan_properties_2', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/some_nan_properties_3', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/some_nan_properties_4', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/some_nan_properties_5', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/some_nan_properties_e6', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_0', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_1', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/min_properties_2', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (((('const/fcp/dimindex' W) ('const/bool/the_value' W)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & ((('const/fcp/dimindex' T) ('const/bool/the_value' T)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/binary_ieee/min_properties_3', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_4', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_5', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/min_properties_6', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_7', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_8', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/min_properties_9', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_is_integral' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (((('const/fcp/dimindex' W) ('const/bool/the_value' W)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & ((('const/fcp/dimindex' T) ('const/bool/the_value' T)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/binary_ieee/min_properties_10', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_11', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/min_properties_12', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/min_properties_e13', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_minus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/top_properties_0', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/top_properties_1', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/top_properties_2', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/top_properties_3', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (~ ((('const/fcp/dimindex' W) ('const/bool/the_value' W)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/binary_ieee/top_properties_4', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ((('const/fcp/dimindex' W) ('const/bool/the_value' W)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/top_properties_e5', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/bottom_properties_0', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_zero' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/bottom_properties_1', ax, ![T : $t, W : $t]: (('const/binary_ieee/float_is_finite' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/bottom_properties_2', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_nan' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/bottom_properties_3', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_is_normal' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (~ ((('const/fcp/dimindex' W) ('const/bool/the_value' W)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/binary_ieee/bottom_properties_4', ax, ![W : $t, T : $t]: ((('const/binary_ieee/float_is_subnormal' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = ((('const/fcp/dimindex' W) ('const/bool/the_value' W)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/binary_ieee/bottom_properties_e5', ax, ![T : $t, W : $t]: (~ (('const/binary_ieee/float_is_infinite' T W) (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_to_real_negate_', ax, ![A : $t, B : $t]: (![x : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/float_to_real' A B) (('const/binary_ieee/float_negate' A B) x)) = ('const/realax/real_neg' (('const/binary_ieee/float_to_real' A B) x))))).
tt('thm/binary_ieee/float_negate_negate_', ax, ![A : $t, B : $t]: (![x : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/float_negate' A B) (('const/binary_ieee/float_negate' A B) x)) = x))).
tt('thm/binary_ieee/ulp_', ax, ![T : $t, W : $t]: ((('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_to_real' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/neg_ulp_', ax, ![T : $t, W : $t]: (('const/realax/real_neg' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_to_real' T W) (('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_plus_min' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/ULP_le_mono_', ax, ![A : $t, T : $t]: (![e1 : ('type/fcp/cart' $o A), e2 : ('type/fcp/cart' $o A)]: ((~ (e2 = (('const/words/n2w' A) 'const/num/0'))) => (('const/real/real_lte' (('const/binary_ieee/ULP' T A) (('const/pair/,' ('type/fcp/cart' $o A) ('type/bool/itself' T)) e1 ('const/bool/the_value' T))) (('const/binary_ieee/ULP' T A) (('const/pair/,' ('type/fcp/cart' $o A) ('type/bool/itself' T)) e2 ('const/bool/the_value' T)))) = (('const/words/word_ls' A) e1 e2))))).
tt('thm/binary_ieee/ulp_lt_ULP_', ax, ![T : $t, W : $t]: (![e : ('type/fcp/cart' $o W)]: ('const/real/real_lte' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) e ('const/bool/the_value' T)))))).
tt('thm/binary_ieee/ulp_lt_largest_', ax, ![T : $t, W : $t]: ('const/realax/real_lt' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/ulp_lt_threshold_', ax, ![T : $t, W : $t]: ('const/realax/real_lt' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/abs_float_value_0', ax, (![b : ('type/fcp/cart' $o 'type/one/one'), c : 'type/realax/real', d : 'type/realax/real']: (('const/real/abs' ('const/realax/real_mul' ('const/realax/real_mul' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/words/w2n' 'type/one/one') b)) c) d)) = ('const/real/abs' ('const/realax/real_mul' c d))))).
tt('thm/binary_ieee/abs_float_value_e1', ax, (![b : ('type/fcp/cart' $o 'type/one/one'), c : 'type/realax/real']: (('const/real/abs' ('const/realax/real_mul' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/words/w2n' 'type/one/one') b)) c)) = ('const/real/abs' c)))).
tt('thm/binary_ieee/less_than_ulp_', ax, ![T : $t, W : $t]: (![a : ('type/binary_ieee/float' T W)]: (('const/realax/real_lt' ('const/real/abs' (('const/binary_ieee/float_to_real' T W) a)) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (((('const/binary_ieee/float_Exponent' T W) a) = (('const/words/n2w' W) 'const/num/0')) & ((('const/binary_ieee/float_Significand' T W) a) = (('const/words/n2w' T) 'const/num/0')))))).
tt('thm/binary_ieee/float_is_zero_to_real_', ax, ![A : $t, B : $t]: (![x : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/float_is_zero' A B) x) = ((('const/binary_ieee/float_to_real' A B) x) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/binary_ieee/float_is_zero_', ax, ![A : $t, B : $t]: (![x : ('type/binary_ieee/float' A B)]: ((('const/binary_ieee/float_is_zero' A B) x) = (((('const/binary_ieee/float_Exponent' A B) x) = (('const/words/n2w' B) 'const/num/0')) & ((('const/binary_ieee/float_Significand' A B) x) = (('const/words/n2w' A) 'const/num/0')))))).
tt('thm/binary_ieee/float_to_real_eq_', ax, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: (((('const/binary_ieee/float_to_real' T W) x) = (('const/binary_ieee/float_to_real' T W) y)) = ((x = y) | ((('const/binary_ieee/float_is_zero' T W) x) & (('const/binary_ieee/float_is_zero' T W) y)))))).
tt('thm/binary_ieee/diff_float_ULP_', ax, ![T : $t, W : $t]: (![x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: (((~ ((('const/binary_ieee/float_to_real' T W) x) = (('const/binary_ieee/float_to_real' T W) y))) & (~ (('const/binary_ieee/exponent_boundary' T W) y x))) => ('const/real/real_lte' (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) x) ('const/bool/the_value' T))) ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' T W) x) (('const/binary_ieee/float_to_real' T W) y))))))).
tt('thm/binary_ieee/diff_lt_ulp_eq0_', ax, ![T : $t, W : $t]: (![a : ('type/binary_ieee/float' T W), b : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (((~ (('const/binary_ieee/exponent_boundary' T W) b a)) & (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x (('const/binary_ieee/float_to_real' T W) a))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) a) ('const/bool/the_value' T)))) & (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x (('const/binary_ieee/float_to_real' T W) b))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) a) ('const/bool/the_value' T)))) & (('const/real/real_lte' ('const/real/abs' (('const/binary_ieee/float_to_real' T W) a)) ('const/real/abs' x)) & (('const/real/real_lte' ('const/real/abs' (('const/binary_ieee/float_to_real' T W) b)) ('const/real/abs' x)) & (~ (('const/binary_ieee/float_is_zero' T W) a))))))) => (b = a)))).
tt('thm/binary_ieee/diff_lt_ulp_even_', ax, ![T : $t, W : $t]: (![a : ('type/binary_ieee/float' T W), b : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (((~ (('const/binary_ieee/exponent_boundary' T W) b a)) & (('const/realax/real_lt' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' T W) a) x))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) a) ('const/bool/the_value' T)))) & (('const/realax/real_lt' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' T W) b) x))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) a) ('const/bool/the_value' T)))) & (~ (('const/binary_ieee/float_is_zero' T W) a))))) => (b = a)))).
tt('thm/binary_ieee/diff_lt_ulp_even4_', ax, ![T : $t, W : $t]: (![a : ('type/binary_ieee/float' T W), b : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (((~ (('const/binary_ieee/exponent_boundary' T W) b a)) & (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' T W) a) x))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) a) ('const/bool/the_value' T)))) & (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/abs' ('const/real/real_sub' (('const/binary_ieee/float_to_real' T W) b) x))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) a) ('const/bool/the_value' T)))) & (~ (('const/binary_ieee/float_is_zero' T W) a))))) => (b = a)))).
tt('thm/binary_ieee/round_roundTowardZero_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real', r : 'type/realax/real']: ((((('const/binary_ieee/float_value' T W) y) = ('const/binary_ieee/Float' r)) & (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' r x)) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) y) ('const/bool/the_value' T)))) & (('const/real/real_lte' ('const/real/abs' r) ('const/real/abs' x)) & (('const/real/real_lte' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) ('const/real/abs' x)) & ('const/real/real_lte' ('const/real/abs' x) (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardZero' x) = y)))).
tt('thm/binary_ieee/round_roundTiesToEven_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real', r : 'type/realax/real']: ((((('const/binary_ieee/float_value' T W) y) = ('const/binary_ieee/Float' r)) & (((((('const/binary_ieee/float_Significand' T W) y) = (('const/words/n2w' T) 'const/num/0')) & (~ ((('const/binary_ieee/float_Exponent' T W) y) = (('const/words/n2w' W) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) => ('const/real/real_lte' ('const/real/abs' r) ('const/real/abs' x))) & (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' ('const/real/real_sub' r x))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) y) ('const/bool/the_value' T)))) & (((('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' ('const/real/real_sub' r x))) = (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) y) ('const/bool/the_value' T)))) => (~ (('const/words/word_lsb' T) (('const/binary_ieee/float_Significand' T W) y)))) & (('const/realax/real_lt' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' x))) & ('const/realax/real_lt' ('const/real/abs' x) (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTiesToEven' x) = y)))).
tt('thm/binary_ieee/round_roundTiesToEven0_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real', r : 'type/realax/real']: ((((('const/binary_ieee/float_value' T W) y) = ('const/binary_ieee/Float' r)) & ((((('const/binary_ieee/float_Significand' T W) y) = (('const/words/n2w' T) 'const/num/0')) & ((~ ((('const/binary_ieee/float_Exponent' T W) y) = (('const/words/n2w' W) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (~ ('const/real/real_lte' ('const/real/abs' r) ('const/real/abs' x))))) & (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/abs' ('const/real/real_sub' r x))) (('const/binary_ieee/ULP' T W) (('const/pair/,' ('type/fcp/cart' $o W) ('type/bool/itself' T)) (('const/binary_ieee/float_Exponent' T W) y) ('const/bool/the_value' T)))) & (('const/realax/real_lt' (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W))) ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' x))) & ('const/realax/real_lt' ('const/real/abs' x) (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTiesToEven' x) = y)))).
tt('thm/binary_ieee/round_roundTowardZero_is_zero_', ax, ![T : $t, W : $t]: (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' x) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => (((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardZero' x) = (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) | ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardZero' x) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/round_roundTiesToEven_is_zero_', ax, ![T : $t, W : $t]: (![x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' x)) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => (((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTiesToEven' x) = (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) | ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTiesToEven' x) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/round_roundTowardZero_is_minus_zero_', ax, ![T : $t, W : $t]: (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' x) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardZero' $true x) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardZero_is_plus_zero_', ax, ![T : $t, W : $t]: (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' x) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardZero' $false x) = (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTiesToEven_is_minus_zero_', ax, ![T : $t, W : $t]: (![x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' x)) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTiesToEven' $true x) = (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTiesToEven_is_plus_zero_', ax, ![T : $t, W : $t]: (![x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/abs' x)) (('const/binary_ieee/ulp' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTiesToEven' $false x) = (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/largest_is_positive_', ax, ![T : $t, W : $t]: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/threshold_is_positive_', ax, ![T : $t, W : $t]: ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/round_roundTiesToEven_plus_infinity_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/real/real_lte' (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTiesToEven' x) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTiesToEven_minus_infinity_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/real/real_lte' x ('const/realax/real_neg' (('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTiesToEven' x) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardZero_top_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardZero' x) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardZero_bottom_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_neg' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardZero' x) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardPositive_plus_infinity_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardPositive' x) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardPositive_bottom_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_neg' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardPositive' x) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardNegative_top_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardNegative' x) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/round_roundTowardNegative_minus_infinity_', ax, ![T : $t, W : $t]: (![y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_neg' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/round' T W) 'const/binary_ieee/roundTowardNegative' x) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_roundTowardZero_top_', ax, ![T : $t, W : $t]: (![b : $o, y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardZero' b x) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_roundTowardZero_bottom_', ax, ![T : $t, W : $t]: (![b : $o, y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_neg' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardZero' b x) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_roundTowardPositive_plus_infinity_', ax, ![T : $t, W : $t]: (![b : $o, y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardPositive' b x) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_roundTowardPositive_bottom_', ax, ![T : $t, W : $t]: (![b : $o, y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_neg' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardPositive' b x) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_roundTowardNegative_top_', ax, ![T : $t, W : $t]: (![b : $o, y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardNegative' b x) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_roundTowardNegative_minus_infinity_', ax, ![T : $t, W : $t]: (![b : $o, y : ('type/binary_ieee/float' T W), x : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_neg' (('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) => ((('const/binary_ieee/float_round' T W) 'const/binary_ieee/roundTowardNegative' b x) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_minus_zero_', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) (('const/words/n2w' W) 'const/num/0')) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) (('const/words/n2w' T) 'const/num/0')) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))).
tt('thm/binary_ieee/float_minus_infinity_', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) ('const/words/word_T' W)) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) (('const/words/n2w' T) 'const/num/0')) ('const/bool/ARB' ('type/binary_ieee/float' T W))))))).
tt('thm/binary_ieee/float_round_non_zero_', ax, ![B : $t, A : $t]: (![mode : 'type/binary_ieee/rounding', toneg : $o, r : 'type/realax/real', s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o A), f : ('type/fcp/cart' $o B)]: ((((('const/binary_ieee/round' B A) mode r) = (('const/binary_ieee/float_Sign_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o A) ('type/fcp/cart' $o A)) e) (('const/binary_ieee/float_Significand_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o B) ('type/fcp/cart' $o B)) f) ('const/bool/ARB' ('type/binary_ieee/float' B A)))))) & ((~ (e = (('const/words/n2w' A) 'const/num/0'))) | (~ (f = (('const/words/n2w' B) 'const/num/0'))))) => ((('const/binary_ieee/float_round' B A) mode toneg r) = (('const/binary_ieee/float_Sign_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o A) ('type/fcp/cart' $o A)) e) (('const/binary_ieee/float_Significand_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o B) ('type/fcp/cart' $o B)) f) ('const/bool/ARB' ('type/binary_ieee/float' B A))))))))).
tt('thm/binary_ieee/float_round_plus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', toneg : $o, r : 'type/realax/real']: (((('const/binary_ieee/round' T W) mode r) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) mode toneg r) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_minus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', toneg : $o, r : 'type/realax/real']: (((('const/binary_ieee/round' T W) mode r) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) mode toneg r) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_top_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', toneg : $o, r : 'type/realax/real']: (((('const/binary_ieee/round' T W) mode r) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) mode toneg r) = (('const/binary_ieee/float_top' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_round_bottom_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', toneg : $o, r : 'type/realax/real']: (((('const/binary_ieee/round' T W) mode r) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) => ((('const/binary_ieee/float_round' T W) mode toneg r) = (('const/binary_ieee/float_bottom' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_to_real_', ax, ![T : $t, W : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o W), f : ('type/fcp/cart' $o T)]: ((('const/binary_ieee/float_to_real' T W) (('const/binary_ieee/float_Sign_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o W) ('type/fcp/cart' $o W)) e) (('const/binary_ieee/float_Significand_fupd' T W) (('const/combin/K' ('type/fcp/cart' $o T) ('type/fcp/cart' $o T)) f) ('const/bool/ARB' ('type/binary_ieee/float' T W)))))) = (('const/bool/LET' 'type/realax/real' 'type/realax/real') (^[r : 'type/realax/real']: (('const/bool/COND' 'type/realax/real') (s = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/realax/real_neg' r) r)) (('const/bool/COND' 'type/realax/real') (e = (('const/words/n2w' W) 'const/num/0')) ('const/realax/real_mul' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/words/INT_MAX' W) ('const/bool/the_value' W))))) ('const/real/#slash#' ('const/real/real_of_num' (('const/words/w2n' T) f)) ('const/real/real_of_num' (('const/words/dimword' T) ('const/bool/the_value' T))))) ('const/realax/real_mul' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/words/w2n' W) e))) ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/words/INT_MAX' W) ('const/bool/the_value' W))))) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/#slash#' ('const/real/real_of_num' (('const/words/w2n' T) f)) ('const/real/real_of_num' (('const/words/dimword' T) ('const/bool/the_value' T))))))))))).
tt('thm/binary_ieee/largest_', ax, ![W : $t, T : $t]: ((('const/binary_ieee/largest' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = ('const/real/#slash#' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/-' (('const/words/UINT_MAX' W) ('const/bool/the_value' W)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' (('const/words/dimword' T) ('const/bool/the_value' T)))))) ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/words/INT_MAX' W) ('const/bool/the_value' W))))))).
tt('thm/binary_ieee/threshold_', ax, ![W : $t, T : $t]: ((('const/binary_ieee/threshold' T W) ('const/bool/the_value' ('type/pair/prod' T W))) = ('const/real/#slash#' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/-' (('const/words/UINT_MAX' W) ('const/bool/the_value' W)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/words/dimword' T) ('const/bool/the_value' T))))))) ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (('const/words/INT_MAX' W) ('const/bool/the_value' W))))))).
tt('thm/binary_ieee/float_tests_0', ax, ![B : $t, A : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o A), f : ('type/fcp/cart' $o B)]: ((('const/binary_ieee/float_is_nan' B A) (('const/binary_ieee/float_Sign_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o A) ('type/fcp/cart' $o A)) e) (('const/binary_ieee/float_Significand_fupd' B A) (('const/combin/K' ('type/fcp/cart' $o B) ('type/fcp/cart' $o B)) f) ('const/bool/ARB' ('type/binary_ieee/float' B A)))))) = ((e = (('const/words/word_2comp' A) (('const/words/n2w' A) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (~ (f = (('const/words/n2w' B) 'const/num/0'))))))).
tt('thm/binary_ieee/float_tests_1', ax, ![D : $t, C : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o C), f : ('type/fcp/cart' $o D)]: ((('const/binary_ieee/float_is_infinite' D C) (('const/binary_ieee/float_Sign_fupd' D C) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' D C) (('const/combin/K' ('type/fcp/cart' $o C) ('type/fcp/cart' $o C)) e) (('const/binary_ieee/float_Significand_fupd' D C) (('const/combin/K' ('type/fcp/cart' $o D) ('type/fcp/cart' $o D)) f) ('const/bool/ARB' ('type/binary_ieee/float' D C)))))) = ((e = (('const/words/word_2comp' C) (('const/words/n2w' C) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (f = (('const/words/n2w' D) 'const/num/0')))))).
tt('thm/binary_ieee/float_tests_2', ax, ![E : $t, F : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o E), f : ('type/fcp/cart' $o F)]: ((('const/binary_ieee/float_is_normal' F E) (('const/binary_ieee/float_Sign_fupd' F E) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' F E) (('const/combin/K' ('type/fcp/cart' $o E) ('type/fcp/cart' $o E)) e) (('const/binary_ieee/float_Significand_fupd' F E) (('const/combin/K' ('type/fcp/cart' $o F) ('type/fcp/cart' $o F)) f) ('const/bool/ARB' ('type/binary_ieee/float' F E)))))) = ((~ (e = (('const/words/n2w' E) 'const/num/0'))) & (~ (e = (('const/words/word_2comp' E) (('const/words/n2w' E) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))).
tt('thm/binary_ieee/float_tests_3', ax, ![H : $t, G : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o G), f : ('type/fcp/cart' $o H)]: ((('const/binary_ieee/float_is_subnormal' H G) (('const/binary_ieee/float_Sign_fupd' H G) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' H G) (('const/combin/K' ('type/fcp/cart' $o G) ('type/fcp/cart' $o G)) e) (('const/binary_ieee/float_Significand_fupd' H G) (('const/combin/K' ('type/fcp/cart' $o H) ('type/fcp/cart' $o H)) f) ('const/bool/ARB' ('type/binary_ieee/float' H G)))))) = ((e = (('const/words/n2w' G) 'const/num/0')) & (~ (f = (('const/words/n2w' H) 'const/num/0'))))))).
tt('thm/binary_ieee/float_tests_4', ax, ![J : $t, I : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o I), f : ('type/fcp/cart' $o J)]: ((('const/binary_ieee/float_is_zero' J I) (('const/binary_ieee/float_Sign_fupd' J I) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' J I) (('const/combin/K' ('type/fcp/cart' $o I) ('type/fcp/cart' $o I)) e) (('const/binary_ieee/float_Significand_fupd' J I) (('const/combin/K' ('type/fcp/cart' $o J) ('type/fcp/cart' $o J)) f) ('const/bool/ARB' ('type/binary_ieee/float' J I)))))) = ((e = (('const/words/n2w' I) 'const/num/0')) & (f = (('const/words/n2w' J) 'const/num/0')))))).
tt('thm/binary_ieee/float_tests_e5', ax, ![K : $t, L : $t]: (![s : ('type/fcp/cart' $o 'type/one/one'), e : ('type/fcp/cart' $o K), f : ('type/fcp/cart' $o L)]: ((('const/binary_ieee/float_is_finite' L K) (('const/binary_ieee/float_Sign_fupd' L K) (('const/combin/K' ('type/fcp/cart' $o 'type/one/one') ('type/fcp/cart' $o 'type/one/one')) s) (('const/binary_ieee/float_Exponent_fupd' L K) (('const/combin/K' ('type/fcp/cart' $o K) ('type/fcp/cart' $o K)) e) (('const/binary_ieee/float_Significand_fupd' L K) (('const/combin/K' ('type/fcp/cart' $o L) ('type/fcp/cart' $o L)) f) ('const/bool/ARB' ('type/binary_ieee/float' L K)))))) = (~ (e = (('const/words/word_2comp' K) (('const/words/n2w' K) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/binary_ieee/float_infinity_negate_abs_0', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/float_infinity_negate_abs_1', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_negate' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/float_infinity_negate_abs_2', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_abs' T W) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/float_infinity_negate_abs_e3', ax, ![T : $t, W : $t]: ((('const/binary_ieee/float_abs' T W) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))).
tt('thm/binary_ieee/float_add_compute_0', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_add_compute_1', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_add' T W) mode x (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_add_compute_2', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_add_compute_3', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_add_compute_4', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_add_compute_e5', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_add_nan_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((((('const/binary_ieee/float_value' T W) x) = 'const/binary_ieee/NaN') | ((('const/binary_ieee/float_value' T W) y) = 'const/binary_ieee/NaN')) => ((('const/binary_ieee/float_add' T W) mode x y) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_add_finite_', ax, ![A : $t, B : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' A B), y : ('type/binary_ieee/float' A B), r1 : 'type/realax/real', r2 : 'type/realax/real']: ((((('const/binary_ieee/float_value' A B) x) = ('const/binary_ieee/Float' r1)) & ((('const/binary_ieee/float_value' A B) y) = ('const/binary_ieee/Float' r2))) => ((('const/binary_ieee/float_add' A B) mode x y) = (('const/binary_ieee/float_round' A B) mode (('const/bool/COND' $o) ((r1 = ('const/real/real_of_num' 'const/num/0')) & ((r2 = ('const/real/real_of_num' 'const/num/0')) & ((('const/binary_ieee/float_Sign' A B) x) = (('const/binary_ieee/float_Sign' A B) y)))) ((('const/binary_ieee/float_Sign' A B) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (mode = 'const/binary_ieee/roundTowardNegative')) ('const/realax/real_add' r1 r2)))))).
tt('thm/binary_ieee/float_add_finite_plus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_add' T W) mode x (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_add_plus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_add_finite_minus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_add' T W) mode x (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_add_minus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_add' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_sub_compute_0', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_sub_compute_1', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_sub' T W) mode x (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_sub_compute_2', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_sub_compute_3', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_sub_compute_4', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_sub_compute_e5', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_sub_nan_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((((('const/binary_ieee/float_value' T W) x) = 'const/binary_ieee/NaN') | ((('const/binary_ieee/float_value' T W) y) = 'const/binary_ieee/NaN')) => ((('const/binary_ieee/float_sub' T W) mode x y) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_sub_finite_', ax, ![A : $t, B : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' A B), y : ('type/binary_ieee/float' A B), r1 : 'type/realax/real', r2 : 'type/realax/real']: ((((('const/binary_ieee/float_value' A B) x) = ('const/binary_ieee/Float' r1)) & ((('const/binary_ieee/float_value' A B) y) = ('const/binary_ieee/Float' r2))) => ((('const/binary_ieee/float_sub' A B) mode x y) = (('const/binary_ieee/float_round' A B) mode (('const/bool/COND' $o) ((r1 = ('const/real/real_of_num' 'const/num/0')) & ((r2 = ('const/real/real_of_num' 'const/num/0')) & (~ ((('const/binary_ieee/float_Sign' A B) x) = (('const/binary_ieee/float_Sign' A B) y))))) ((('const/binary_ieee/float_Sign' A B) x) = (('const/words/n2w' 'type/one/one') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (mode = 'const/binary_ieee/roundTowardNegative')) ('const/real/real_sub' r1 r2)))))).
tt('thm/binary_ieee/float_sub_finite_plus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_sub' T W) mode x (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_sub_plus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_sub_finite_minus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_sub' T W) mode x (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_sub_minus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_sub' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_mul_compute_0', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_mul_compute_1', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_mul' T W) mode x (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_mul_compute_2', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_mul_compute_3', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_mul_compute_4', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_mul_compute_e5', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_mul_nan_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((((('const/binary_ieee/float_value' T W) x) = 'const/binary_ieee/NaN') | ((('const/binary_ieee/float_value' T W) y) = 'const/binary_ieee/NaN')) => ((('const/binary_ieee/float_mul' T W) mode x y) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_mul_finite_', ax, ![A : $t, B : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' A B), y : ('type/binary_ieee/float' A B), r1 : 'type/realax/real', r2 : 'type/realax/real']: ((((('const/binary_ieee/float_value' A B) x) = ('const/binary_ieee/Float' r1)) & ((('const/binary_ieee/float_value' A B) y) = ('const/binary_ieee/Float' r2))) => ((('const/binary_ieee/float_mul' A B) mode x y) = (('const/binary_ieee/float_round' A B) mode (~ ((('const/binary_ieee/float_Sign' A B) x) = (('const/binary_ieee/float_Sign' A B) y))) ('const/realax/real_mul' r1 r2)))))).
tt('thm/binary_ieee/float_mul_finite_plus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_mul' T W) mode x (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/bool/COND' ('type/binary_ieee/float' T W)) (r = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_mul_plus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/bool/COND' ('type/binary_ieee/float' T W)) (r = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_mul_finite_minus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_mul' T W) mode x (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/bool/COND' ('type/binary_ieee/float' T W)) (r = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_mul_minus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_mul' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/bool/COND' ('type/binary_ieee/float' T W)) (r = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))))).
tt('thm/binary_ieee/float_div_compute_0', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_div_compute_1', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W)]: ((('const/binary_ieee/float_div' T W) mode x (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_div_compute_2', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_div_compute_3', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_div_compute_4', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_div_compute_e5', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding']: ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))).
tt('thm/binary_ieee/float_div_nan_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W)]: ((((('const/binary_ieee/float_value' T W) x) = 'const/binary_ieee/NaN') | ((('const/binary_ieee/float_value' T W) y) = 'const/binary_ieee/NaN')) => ((('const/binary_ieee/float_div' T W) mode x y) = (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))))))).
tt('thm/binary_ieee/float_div_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), y : ('type/binary_ieee/float' T W), r1 : 'type/realax/real', r2 : 'type/realax/real']: ((((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r1)) & ((('const/binary_ieee/float_value' T W) y) = ('const/binary_ieee/Float' r2))) => ((('const/binary_ieee/float_div' T W) mode x y) = (('const/bool/COND' ('type/binary_ieee/float' T W)) (r2 = ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' ('type/binary_ieee/float' T W)) (r1 = ('const/real/real_of_num' 'const/num/0')) (('const/binary_ieee/float_some_nan' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y)) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))))) (('const/binary_ieee/float_round' T W) mode (~ ((('const/binary_ieee/float_Sign' T W) x) = (('const/binary_ieee/float_Sign' T W) y))) ('const/real/#slash#' r1 r2))))))).
tt('thm/binary_ieee/float_div_finite_plus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_div' T W) mode x (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/float_div_plus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/float_div_finite_minus_infinity_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_div' T W) mode x (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))) = (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_minus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_zero' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
tt('thm/binary_ieee/float_div_minus_infinity_finite_', ax, ![T : $t, W : $t]: (![mode : 'type/binary_ieee/rounding', x : ('type/binary_ieee/float' T W), r : 'type/realax/real']: (((('const/binary_ieee/float_value' T W) x) = ('const/binary_ieee/Float' r)) => ((('const/binary_ieee/float_div' T W) mode (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) x) = (('const/bool/COND' ('type/binary_ieee/float' T W)) ((('const/binary_ieee/float_Sign' T W) x) = (('const/words/n2w' 'type/one/one') 'const/num/0')) (('const/binary_ieee/float_minus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W))) (('const/binary_ieee/float_plus_infinity' T W) ('const/bool/the_value' ('type/pair/prod' T W)))))))).
