Theory "binary_ieee"

Parents     words   transc   intreal

Signature

Type Arity
flags 0
float 2
float_compare 0
float_value 0
fp_op 2
rounding 0
Constant Type
EQ :float_compare
FP_Add :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) fp_op
FP_Div :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) fp_op
FP_Mul :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) fp_op
FP_MulAdd :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) float -> (τ, χ) fp_op
FP_MulSub :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) float -> (τ, χ) fp_op
FP_Sqrt :rounding -> (τ, χ) float -> (τ, χ) fp_op
FP_Sub :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) fp_op
Float :real -> float_value
GT :float_compare
Infinity :float_value
LT :float_compare
NaN :float_value
ULP :χ word # τ itself -> real
UN :float_compare
check_for_signalling :(α, β) float list -> flags
clear_flags :flags
closest :((α, β) float -> bool) -> real -> (α, β) float
closest_such :((α, β) float -> bool) -> ((α, β) float -> bool) -> real -> (α, β) float
dividezero_flags :flags
exponent_boundary :(τ, χ) float reln
flags_CASE :flags -> (bool -> bool -> bool -> bool -> bool -> bool -> α) -> α
flags_DivideByZero :flags -> bool
flags_DivideByZero_fupd :(bool -> bool) -> flags -> flags
flags_InvalidOp :flags -> bool
flags_InvalidOp_fupd :(bool -> bool) -> flags -> flags
flags_Overflow :flags -> bool
flags_Overflow_fupd :(bool -> bool) -> flags -> flags
flags_Precision :flags -> bool
flags_Precision_fupd :(bool -> bool) -> flags -> flags
flags_Underflow_AfterRounding :flags -> bool
flags_Underflow_AfterRounding_fupd :(bool -> bool) -> flags -> flags
flags_Underflow_BeforeRounding :flags -> bool
flags_Underflow_BeforeRounding_fupd :(bool -> bool) -> flags -> flags
flags_size :flags -> num
float_CASE :(τ, χ) float -> (word1 -> χ word -> τ word -> α) -> α
float_Exponent :(τ, χ) float -> χ word
float_Exponent_fupd :(χ word -> ψ word) -> (τ, χ) float -> (τ, ψ) float
float_Sign :(τ, χ) float -> word1
float_Sign_fupd :(word1 -> word1) -> (τ, χ) float -> (τ, χ) float
float_Significand :(τ, χ) float -> τ word
float_Significand_fupd :(τ word -> υ word) -> (τ, χ) float -> (υ, χ) float
float_abs :(τ, χ) float -> (τ, χ) float
float_add :rounding -> (τ, χ) float -> (τ, χ) float -> flags # (τ, χ) float
float_bottom :(τ # χ) itself -> (τ, χ) float
float_compare :(τ, χ) float -> (τ, χ) float -> float_compare
float_compare2num :float_compare -> num
float_compare_CASE :float_compare -> α -> α -> α -> α -> α
float_compare_size :float_compare -> num
float_div :rounding -> (τ, χ) float -> (τ, χ) float -> flags # (τ, χ) float
float_equal :(τ, χ) float reln
float_greater_equal :(τ, χ) float reln
float_greater_than :(τ, χ) float reln
float_is_finite :(τ, χ) float -> bool
float_is_infinite :(τ, χ) float -> bool
float_is_integral :(τ, χ) float -> bool
float_is_nan :(τ, χ) float -> bool
float_is_normal :(τ, χ) float -> bool
float_is_signalling :(τ, χ) float -> bool
float_is_subnormal :(τ, χ) float -> bool
float_is_zero :(τ, χ) float -> bool
float_less_equal :(τ, χ) float reln
float_less_than :(τ, χ) float reln
float_minus_infinity :(τ # χ) itself -> (τ, χ) float
float_minus_min :(τ # χ) itself -> (τ, χ) float
float_minus_zero :(τ # χ) itself -> (τ, χ) float
float_mul :rounding -> (τ, χ) float -> (τ, χ) float -> flags # (τ, χ) float
float_mul_add :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) float -> flags # (τ, χ) float
float_mul_sub :rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) float -> flags # (τ, χ) float
float_negate :(τ, χ) float -> (τ, χ) float
float_plus_infinity :(τ # χ) itself -> (τ, χ) float
float_plus_min :(τ # χ) itself -> (τ, χ) float
float_plus_zero :(τ # χ) itself -> (τ, χ) float
float_round :rounding -> bool -> real -> (τ, χ) float
float_round_to_integral :rounding -> (τ, χ) float -> (τ, χ) float
float_round_with_flags :rounding -> bool -> real -> flags # (τ, χ) float
float_size :(τ -> num) -> (χ -> num) -> (τ, χ) float -> num
float_some_qnan :(τ, χ) fp_op -> (τ, χ) float
float_sqrt :rounding -> (τ, χ) float -> flags # (τ, χ) float
float_sub :rounding -> (τ, χ) float -> (τ, χ) float -> flags # (τ, χ) float
float_to_int :rounding -> (τ, χ) float -> int option
float_to_real :(τ, χ) float -> real
float_top :(τ # χ) itself -> (τ, χ) float
float_value :(τ, χ) float -> float_value
float_value_CASE :float_value -> (real -> α) -> α -> α -> α
float_value_size :float_value -> num
fp_op_CASE :(τ, χ) fp_op -> (rounding -> (τ, χ) float -> α) -> (rounding -> (τ, χ) float -> (τ, χ) float -> α) -> (rounding -> (τ, χ) float -> (τ, χ) float -> α) -> (rounding -> (τ, χ) float -> (τ, χ) float -> α) -> (rounding -> (τ, χ) float -> (τ, χ) float -> α) -> (rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) float -> α) -> (rounding -> (τ, χ) float -> (τ, χ) float -> (τ, χ) float -> α) -> α
fp_op_size :(τ -> num) -> (χ -> num) -> (τ, χ) fp_op -> num
integral_round :rounding -> real -> (τ, χ) float
invalidop_flags :flags
is_closest :((α, β) float -> bool) -> real -> (α, β) float -> bool
is_integral :real -> bool
largest :(τ # χ) itself -> real
num2float_compare :num -> float_compare
num2rounding :num -> rounding
real_to_float :rounding -> real -> (α, β) float
real_to_float_with_flags :rounding -> real -> flags # (α, β) float
recordtype.flags :bool -> bool -> bool -> bool -> bool -> bool -> flags
recordtype.float :word1 -> χ word -> τ word -> (τ, χ) float
round :rounding -> real -> (τ, χ) float
roundTiesToEven :rounding
roundTowardNegative :rounding
roundTowardPositive :rounding
roundTowardZero :rounding
rounding2num :rounding -> num
rounding_CASE :rounding -> α -> α -> α -> α -> α
rounding_size :rounding -> num
threshold :(τ # χ) itself -> real
ulp :(τ # χ) itself -> real

Definitions

float_TY_DEF 
⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀'float' .
                 (∀a0'.
                      (∃a0 a1 a2.
                           a0' =
                           (λa0 a1 a2.
                                ind_type$CONSTR 0 (a0,a1,a2)
                                  (λn. ind_type$BOTTOM)) a0 a1 a2) ⇒
                      'float' a0') ⇒
                 'float' a0') rep
float_case_def 
⊢ ∀a0 a1 a2 f. float_CASE (float a0 a1 a2) f = f a0 a1 a2
float_size_def 
⊢ ∀f f1 a0 a1 a2. float_size f f1 (float a0 a1 a2) = 1
float_Sign 
⊢ ∀c c0 c1. (float c c0 c1).Sign = c
float_Exponent 
⊢ ∀c c0 c1. (float c c0 c1).Exponent = c0
float_Significand 
⊢ ∀c c0 c1. (float c c0 c1).Significand = c1
float_Sign_fupd 
⊢ ∀f c c0 c1. float c c0 c1 with Sign updated_by f = float (f c) c0 c1
float_Exponent_fupd 
⊢ ∀f c c0 c1. float c c0 c1 with Exponent updated_by f = float c (f c0) c1
float_Significand_fupd 
⊢ ∀f c c0 c1. float c c0 c1 with Significand updated_by f = float c c0 (f c1)
float_value_TY_DEF 
⊢ ∃rep.
      TYPE_DEFINITION
        (λa0.
             ∀'float_value' .
                 (∀a0.
                      (∃a.
                           a0 =
                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) a) ∨
                      a0 = ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ∨
                      a0 =
                      ind_type$CONSTR (SUC (SUC 0)) ARB (λn. ind_type$BOTTOM) ⇒
                      'float_value' a0) ⇒
                 'float_value' a0) rep
float_value_case_def 
⊢ (∀a f v v1. float_value_CASE (Float a) f v v1 = f a) ∧
  (∀f v v1. float_value_CASE Infinity f v v1 = v) ∧
  ∀f v v1. float_value_CASE NaN f v v1 = v1
float_value_size_def 
⊢ (∀a. float_value_size (Float a) = 1) ∧ float_value_size Infinity = 0 ∧
  float_value_size NaN = 0
float_to_real_def 
⊢ ∀x.
      float_to_real x =
      if x.Exponent = 0w then
        -1 pow w2n x.Sign * (2 / 2 pow INT_MAX (:χ)) *
        (&w2n x.Significand / 2 pow dimindex (:τ))
      else
        -1 pow w2n x.Sign * (2 pow w2n x.Exponent / 2 pow INT_MAX (:χ)) *
        (1 + &w2n x.Significand / 2 pow dimindex (:τ))
float_value_def 
⊢ ∀x.
      float_value x =
      if x.Exponent = UINT_MAXw then
        if x.Significand = 0w then Infinity else NaN
      else Float (float_to_real x)
float_is_nan_def 
⊢ ∀x.
      float_is_nan x ⇔
      case float_value x of Float v1 => F | Infinity => F | NaN => T
float_is_signalling_def 
⊢ ∀x. float_is_signalling x ⇔ float_is_nan x ∧ ¬word_msb x.Significand
float_is_infinite_def 
⊢ ∀x.
      float_is_infinite x ⇔
      case float_value x of Float v1 => F | Infinity => T | NaN => F
float_is_normal_def 
⊢ ∀x. float_is_normal x ⇔ x.Exponent ≠ 0w ∧ x.Exponent ≠ UINT_MAXw
float_is_subnormal_def 
⊢ ∀x. float_is_subnormal x ⇔ x.Exponent = 0w ∧ x.Significand ≠ 0w
float_is_zero_def 
⊢ ∀x.
      float_is_zero x ⇔
      case float_value x of Float r => r = 0 | Infinity => F | NaN => F
float_is_finite_def 
⊢ ∀x.
      float_is_finite x ⇔
      case float_value x of Float v1 => T | Infinity => F | NaN => F
is_integral_def 
⊢ ∀r. is_integral r ⇔ ∃n. abs r = &n
float_is_integral_def 
⊢ ∀x.
      float_is_integral x ⇔
      case float_value x of
        Float r => is_integral r
      | Infinity => F
      | NaN => F
float_negate_def 
⊢ ∀x. float_negate x = x with Sign := ¬x.Sign
float_abs_def 
⊢ ∀x. float_abs x = x with Sign := 0w
float_plus_infinity_def 
⊢ float_plus_infinity (:τ # χ) =
  <|Sign := 0w; Exponent := UINT_MAXw; Significand := 0w|>
float_plus_zero_def 
⊢ float_plus_zero (:τ # χ) = <|Sign := 0w; Exponent := 0w; Significand := 0w|>
float_top_def 
⊢ float_top (:τ # χ) =
  <|Sign := 0w; Exponent := UINT_MAXw − 1w; Significand := UINT_MAXw|>
float_plus_min_def 
⊢ float_plus_min (:τ # χ) = <|Sign := 0w; Exponent := 0w; Significand := 1w|>
float_minus_infinity_def 
⊢ float_minus_infinity (:τ # χ) = float_negate (float_plus_infinity (:τ # χ))
float_minus_zero_def 
⊢ float_minus_zero (:τ # χ) = float_negate (float_plus_zero (:τ # χ))
float_bottom_def 
⊢ float_bottom (:τ # χ) = float_negate (float_top (:τ # χ))
float_minus_min_def 
⊢ float_minus_min (:τ # χ) = float_negate (float_plus_min (:τ # χ))
flags_TY_DEF 
⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀'flags' .
                 (∀a0'.
                      (∃a0 a1 a2 a3 a4 a5.
                           a0' =
                           (λa0 a1 a2 a3 a4 a5.
                                ind_type$CONSTR 0 (a0,a1,a2,a3,a4,a5)
                                  (λn. ind_type$BOTTOM)) a0 a1 a2 a3 a4 a5) ⇒
                      'flags' a0') ⇒
                 'flags' a0') rep
flags_case_def 
⊢ ∀a0 a1 a2 a3 a4 a5 f.
      flags_CASE (flags a0 a1 a2 a3 a4 a5) f = f a0 a1 a2 a3 a4 a5
flags_size_def 
⊢ ∀a0 a1 a2 a3 a4 a5.
      flags_size (flags a0 a1 a2 a3 a4 a5) =
      1 +
      (bool_size a0 +
       (bool_size a1 +
        (bool_size a2 + (bool_size a3 + (bool_size a4 + bool_size a5)))))
flags_DivideByZero 
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b
flags_InvalidOp 
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0
flags_Overflow 
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1
flags_Precision 
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2
flags_Underflow_BeforeRounding 
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3
flags_Underflow_AfterRounding 
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ b4
flags_DivideByZero_fupd 
⊢ ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with DivideByZero updated_by f =
      flags (f b) b0 b1 b2 b3 b4
flags_InvalidOp_fupd 
⊢ ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with InvalidOp updated_by f =
      flags b (f b0) b1 b2 b3 b4
flags_Overflow_fupd 
⊢ ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with Overflow updated_by f =
      flags b b0 (f b1) b2 b3 b4
flags_Precision_fupd 
⊢ ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with Precision updated_by f =
      flags b b0 b1 (f b2) b3 b4
flags_Underflow_BeforeRounding_fupd 
⊢ ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with Underflow_BeforeRounding updated_by f =
      flags b b0 b1 b2 (f b3) b4
flags_Underflow_AfterRounding_fupd 
⊢ ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with Underflow_AfterRounding updated_by f =
      flags b b0 b1 b2 b3 (f b4)
clear_flags_def 
⊢ clear_flags =
  <|DivideByZero := F; InvalidOp := F; Overflow := F; Precision := F;
    Underflow_BeforeRounding := F; Underflow_AfterRounding := F|>
invalidop_flags_def 
⊢ invalidop_flags = clear_flags with InvalidOp := T
dividezero_flags_def 
⊢ dividezero_flags = clear_flags with DivideByZero := T
rounding_TY_DEF 
⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep
rounding_BIJ 
⊢ (∀a. num2rounding (rounding2num a) = a) ∧
  ∀r. (λn. n < 4) r ⇔ rounding2num (num2rounding r) = r
rounding_size_def 
⊢ ∀x. rounding_size x = 0
rounding_CASE 
⊢ ∀x v0 v1 v2 v3.
      (case x of
         roundTiesToEven => v0
       | roundTowardPositive => v1
       | roundTowardNegative => v2
       | roundTowardZero => v3) =
      (λm.
           if m < 1 then v0
           else if m < 2 then v1
           else if m = 2 then v2
           else v3) (rounding2num x)
is_closest_def 
⊢ ∀s x a.
      is_closest s x a ⇔
      a ∈ s ∧
      ∀b. b ∈ s ⇒ abs (float_to_real a − x) ≤ abs (float_to_real b − x)
closest_such_def 
⊢ ∀p s x.
      closest_such p s x =
      @a. is_closest s x a ∧ ∀b. is_closest s x b ∧ p b ⇒ p a
closest_def 
⊢ closest = closest_such (K T)
largest_def 
⊢ largest (:τ # χ) =
  2 pow (UINT_MAX (:χ) − 1) / 2 pow INT_MAX (:χ) *
  (2 − (2 pow dimindex (:τ))⁻¹)
threshold_def 
⊢ threshold (:τ # χ) =
  2 pow (UINT_MAX (:χ) − 1) / 2 pow INT_MAX (:χ) *
  (2 − (2 pow SUC (dimindex (:τ)))⁻¹)
ULP_primitive_def 
⊢ ULP =
  WFREC (@R. WF R)
    (λULP a.
         case a of
           (v,v1) =>
             I
               (2 pow (if v = 0w then 1 else w2n v) /
                2 pow (INT_MAX (:χ) + dimindex (:τ))))
ulp_def 
⊢ ulp (:τ # χ) = ULP (0w,(:τ))
round_def 
⊢ ∀mode x.
      round mode x =
      case mode of
        roundTiesToEven =>
          (let
             t = threshold (:τ # χ)
           in
             if x ≤ -t then float_minus_infinity (:τ # χ)
             else if x ≥ t then float_plus_infinity (:τ # χ)
             else closest_such (λa. ¬word_lsb a.Significand) float_is_finite x)
      | roundTowardPositive =>
        (let
           t = largest (:τ # χ)
         in
           if x < -t then float_bottom (:τ # χ)
           else if x > t then float_plus_infinity (:τ # χ)
           else closest {a | float_is_finite a ∧ float_to_real a ≥ x} x)
      | roundTowardNegative =>
        (let
           t = largest (:τ # χ)
         in
           if x < -t then float_minus_infinity (:τ # χ)
           else if x > t then float_top (:τ # χ)
           else closest {a | float_is_finite a ∧ float_to_real a ≤ x} x)
      | roundTowardZero =>
        (let
           t = largest (:τ # χ)
         in
           if x < -t then float_bottom (:τ # χ)
           else if x > t then float_top (:τ # χ)
           else
             closest {a | float_is_finite a ∧ abs (float_to_real a) ≤ abs x} x)
integral_round_def 
⊢ ∀mode x.
      integral_round mode x =
      case mode of
        roundTiesToEven =>
          (let
             t = threshold (:τ # χ)
           in
             if x ≤ -t then float_minus_infinity (:τ # χ)
             else if x ≥ t then float_plus_infinity (:τ # χ)
             else
               closest_such (λa. ∃n. EVEN n ∧ abs (float_to_real a) = &n)
                 float_is_integral x)
      | roundTowardPositive =>
        (let
           t = largest (:τ # χ)
         in
           if x < -t then float_bottom (:τ # χ)
           else if x > t then float_plus_infinity (:τ # χ)
           else closest {a | float_is_integral a ∧ float_to_real a ≥ x} x)
      | roundTowardNegative =>
        (let
           t = largest (:τ # χ)
         in
           if x < -t then float_minus_infinity (:τ # χ)
           else if x > t then float_top (:τ # χ)
           else closest {a | float_is_integral a ∧ float_to_real a ≤ x} x)
      | roundTowardZero =>
        (let
           t = largest (:τ # χ)
         in
           if x < -t then float_bottom (:τ # χ)
           else if x > t then float_top (:τ # χ)
           else
             closest {a | float_is_integral a ∧ abs (float_to_real a) ≤ abs x}
               x)
fp_op_TY_DEF 
⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀'fp_op' .
                 (∀a0'.
                      (∃a0 a1.
                           a0' =
                           (λa0 a1.
                                ind_type$CONSTR 0 (a0,a1,ARB,ARB)
                                  (λn. ind_type$BOTTOM)) a0 a1) ∨
                      (∃a0 a1 a2.
                           a0' =
                           (λa0 a1 a2.
                                ind_type$CONSTR (SUC 0) (a0,a1,a2,ARB)
                                  (λn. ind_type$BOTTOM)) a0 a1 a2) ∨
                      (∃a0 a1 a2.
                           a0' =
                           (λa0 a1 a2.
                                ind_type$CONSTR (SUC (SUC 0)) (a0,a1,a2,ARB)
                                  (λn. ind_type$BOTTOM)) a0 a1 a2) ∨
                      (∃a0 a1 a2.
                           a0' =
                           (λa0 a1 a2.
                                ind_type$CONSTR (SUC (SUC (SUC 0)))
                                  (a0,a1,a2,ARB) (λn. ind_type$BOTTOM)) a0 a1
                             a2) ∨
                      (∃a0 a1 a2.
                           a0' =
                           (λa0 a1 a2.
                                ind_type$CONSTR (SUC (SUC (SUC (SUC 0))))
                                  (a0,a1,a2,ARB) (λn. ind_type$BOTTOM)) a0 a1
                             a2) ∨
                      (∃a0 a1 a2 a3.
                           a0' =
                           (λa0 a1 a2 a3.
                                ind_type$CONSTR
                                  (SUC (SUC (SUC (SUC (SUC 0)))))
                                  (a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0 a1
                             a2 a3) ∨
                      (∃a0 a1 a2 a3.
                           a0' =
                           (λa0 a1 a2 a3.
                                ind_type$CONSTR
                                  (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                                  (a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0 a1
                             a2 a3) ⇒
                      'fp_op' a0') ⇒
                 'fp_op' a0') rep
fp_op_case_def 
⊢ (∀a0 a1 f f1 f2 f3 f4 f5 f6.
       fp_op_CASE (FP_Sqrt a0 a1) f f1 f2 f3 f4 f5 f6 = f a0 a1) ∧
  (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
       fp_op_CASE (FP_Add a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f1 a0 a1 a2) ∧
  (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
       fp_op_CASE (FP_Sub a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f2 a0 a1 a2) ∧
  (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
       fp_op_CASE (FP_Mul a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f3 a0 a1 a2) ∧
  (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
       fp_op_CASE (FP_Div a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f4 a0 a1 a2) ∧
  (∀a0 a1 a2 a3 f f1 f2 f3 f4 f5 f6.
       fp_op_CASE (FP_MulAdd a0 a1 a2 a3) f f1 f2 f3 f4 f5 f6 = f5 a0 a1 a2 a3) ∧
  ∀a0 a1 a2 a3 f f1 f2 f3 f4 f5 f6.
      fp_op_CASE (FP_MulSub a0 a1 a2 a3) f f1 f2 f3 f4 f5 f6 = f6 a0 a1 a2 a3
fp_op_size_def 
⊢ (∀f f1 a0 a1.
       fp_op_size f f1 (FP_Sqrt a0 a1) =
       1 + (rounding_size a0 + float_size f f1 a1)) ∧
  (∀f f1 a0 a1 a2.
       fp_op_size f f1 (FP_Add a0 a1 a2) =
       1 + (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
  (∀f f1 a0 a1 a2.
       fp_op_size f f1 (FP_Sub a0 a1 a2) =
       1 + (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
  (∀f f1 a0 a1 a2.
       fp_op_size f f1 (FP_Mul a0 a1 a2) =
       1 + (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
  (∀f f1 a0 a1 a2.
       fp_op_size f f1 (FP_Div a0 a1 a2) =
       1 + (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
  (∀f f1 a0 a1 a2 a3.
       fp_op_size f f1 (FP_MulAdd a0 a1 a2 a3) =
       1 +
       (rounding_size a0 +
        (float_size f f1 a1 + (float_size f f1 a2 + float_size f f1 a3)))) ∧
  ∀f f1 a0 a1 a2 a3.
      fp_op_size f f1 (FP_MulSub a0 a1 a2 a3) =
      1 +
      (rounding_size a0 +
       (float_size f f1 a1 + (float_size f f1 a2 + float_size f f1 a3)))
float_some_qnan_def 
⊢ ∀fp_op.
      float_some_qnan fp_op =
      (@f.
           (let
              qnan = f fp_op
            in
              float_is_nan qnan ∧ ¬float_is_signalling qnan)) fp_op
float_round_def 
⊢ ∀mode toneg r.
      float_round mode toneg r =
      (let
         x = round mode r
       in
         if float_is_zero x then
           if toneg then float_minus_zero (:τ # χ)
           else float_plus_zero (:τ # χ) else x)
float_round_with_flags_def 
⊢ ∀mode to_neg r.
      float_round_with_flags mode to_neg r =
      (let
         x = float_round mode to_neg r and a = abs r ;
         inexact = float_value x ≠ Float r
       in
         (clear_flags with
          <|Overflow := (float_is_infinite x ∨ 2 pow INT_MIN (:χ) ≤ a);
            Underflow_BeforeRounding := (inexact ∧ a < 2 / 2 pow INT_MAX (:χ));
            Underflow_AfterRounding :=
              (inexact ∧
               (float_round mode to_neg r).Exponent ≤₊ n2w (INT_MIN (:χ)));
            Precision := inexact|>,x))
check_for_signalling_def 
⊢ ∀l.
      check_for_signalling l =
      clear_flags with InvalidOp := EXISTS float_is_signalling l
real_to_float_def 
⊢ ∀m. real_to_float m = float_round m (m = roundTowardNegative)
real_to_float_with_flags_def 
⊢ ∀m.
      real_to_float_with_flags m =
      float_round_with_flags m (m = roundTowardNegative)
float_round_to_integral_def 
⊢ ∀mode x.
      float_round_to_integral mode x =
      case float_value x of
        Float r => integral_round mode r
      | Infinity => x
      | NaN => x
float_to_int_def 
⊢ ∀mode x.
      float_to_int mode x =
      case float_value x of
        Float r =>
          SOME
            (case mode of
             roundTiesToEven =>
               (let
                  f = flr r ;
                  df = abs (r − real_of_int f)
                in
                  if df < 1 / 2 ∨ df = 1 / 2 ∧ EVEN (Num (ABS f)) then f
                  else clg r)
           | roundTowardPositive => clg r
           | roundTowardNegative => flr r
           | roundTowardZero => if x.Sign = 1w then clg r else flr r)
      | Infinity => NONE
      | NaN => NONE
float_sqrt_def 
⊢ ∀mode x.
      float_sqrt mode x =
      if x.Sign = 0w then
        case float_value x of
          Float r => float_round_with_flags mode F (sqrt r)
        | Infinity => (clear_flags,float_plus_infinity (:τ # χ))
        | NaN => (check_for_signalling [x],float_some_qnan (FP_Sqrt mode x))
      else (invalidop_flags,float_some_qnan (FP_Sqrt mode x))
float_add_def 
⊢ ∀mode x y.
      (mode float_add x) y =
      case (float_value x,float_value y) of
        (Float r1,Float r2) =>
          float_round_with_flags mode
            (if r1 = 0 ∧ r2 = 0 ∧ x.Sign = y.Sign then x.Sign = 1w
             else (mode = roundTowardNegative)) (r1 + r2)
      | (Float r1,Infinity) => (clear_flags,y)
      | (Float r1,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Add mode x y))
      | (Infinity,Float v7) => (clear_flags,x)
      | (Infinity,Infinity) =>
        if x.Sign = y.Sign then (clear_flags,x)
        else (invalidop_flags,float_some_qnan (FP_Add mode x y))
      | (Infinity,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Add mode x y))
      | (NaN,v1) =>
        (check_for_signalling [x; y],float_some_qnan (FP_Add mode x y))
float_sub_def 
⊢ ∀mode x y.
      (mode float_sub x) y =
      case (float_value x,float_value y) of
        (Float r1,Float r2) =>
          float_round_with_flags mode
            (if r1 = 0 ∧ r2 = 0 ∧ x.Sign ≠ y.Sign then x.Sign = 1w
             else (mode = roundTowardNegative)) (r1 − r2)
      | (Float r1,Infinity) => (clear_flags,float_negate y)
      | (Float r1,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Sub mode x y))
      | (Infinity,Float v7) => (clear_flags,x)
      | (Infinity,Infinity) =>
        if x.Sign = y.Sign then
          (invalidop_flags,float_some_qnan (FP_Sub mode x y))
        else (clear_flags,x)
      | (Infinity,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Sub mode x y))
      | (NaN,v1) =>
        (check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y))
float_mul_def 
⊢ ∀mode x y.
      (mode float_mul x) y =
      case (float_value x,float_value y) of
        (Float r',Float r2) =>
          float_round_with_flags mode (x.Sign ≠ y.Sign) (r' * r2)
      | (Float 0,Infinity) =>
        (invalidop_flags,float_some_qnan (FP_Mul mode x y))
      | (Float r',Infinity) =>
        (clear_flags,if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
      | (Float r',NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Mul mode x y))
      | (Infinity,Float 0) =>
        (invalidop_flags,float_some_qnan (FP_Mul mode x y))
      | (Infinity,Float r) =>
        (clear_flags,if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
      | (Infinity,Infinity) =>
        (clear_flags,if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
      | (Infinity,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Mul mode x y))
      | (NaN,v1) =>
        (check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y))
float_div_def 
⊢ ∀mode x y.
      (mode float_div x) y =
      case (float_value x,float_value y) of
        (Float 0,Float 0) =>
          (invalidop_flags,float_some_qnan (FP_Div mode x y))
      | (Float r1,Float 0) =>
        (dividezero_flags,if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
      | (Float r1,Float r2) =>
        float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 / r2)
      | (Float r1,Infinity) =>
        (clear_flags,if x.Sign = y.Sign then float_plus_zero (:τ # χ)
         else float_minus_zero (:τ # χ))
      | (Float r1,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Div mode x y))
      | (Infinity,Float v7) =>
        (clear_flags,if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
      | (Infinity,Infinity) =>
        (invalidop_flags,float_some_qnan (FP_Div mode x y))
      | (Infinity,NaN) =>
        (check_for_signalling [y],float_some_qnan (FP_Div mode x y))
      | (NaN,v1) =>
        (check_for_signalling [x; y],float_some_qnan (FP_Div mode x y))
float_mul_add_def 
⊢ ∀mode x y z.
      float_mul_add mode x y z =
      (let
         signP = x.Sign ⊕ y.Sign ;
         infP = float_is_infinite x ∨ float_is_infinite y
       in
         if float_is_nan x ∨ float_is_nan y ∨ float_is_nan z then
           (check_for_signalling [x; y; z],
            float_some_qnan (FP_MulAdd mode x y z))
         else if
           float_is_infinite x ∧ float_is_zero y ∨
           float_is_zero x ∧ float_is_infinite y ∨
           float_is_infinite z ∧ infP ∧ signP ≠ z.Sign
         then
           (invalidop_flags,float_some_qnan (FP_MulAdd mode x y z))
         else if float_is_infinite z ∧ z.Sign = 0w ∨ infP ∧ signP = 0w then
           (clear_flags,float_plus_infinity (:τ # χ))
         else if float_is_infinite z ∧ z.Sign = 1w ∨ infP ∧ signP = 1w then
           (clear_flags,float_minus_infinity (:τ # χ))
         else
           (let
              r1 = float_to_real x * float_to_real y and r2 = float_to_real z
            in
              float_round_with_flags mode
                (if r1 = 0 ∧ r2 = 0 ∧ signP = z.Sign then signP = 1w
                 else (mode = roundTowardNegative)) (r1 + r2)))
float_mul_sub_def 
⊢ ∀mode x y z.
      float_mul_sub mode x y z =
      (let
         signP = x.Sign ⊕ y.Sign ;
         infP = float_is_infinite x ∨ float_is_infinite y
       in
         if float_is_nan x ∨ float_is_nan y ∨ float_is_nan z then
           (check_for_signalling [x; y; z],
            float_some_qnan (FP_MulSub mode x y z))
         else if
           float_is_infinite x ∧ float_is_zero y ∨
           float_is_zero x ∧ float_is_infinite y ∨
           float_is_infinite z ∧ infP ∧ signP = z.Sign
         then
           (invalidop_flags,float_some_qnan (FP_MulAdd mode x y z))
         else if float_is_infinite z ∧ z.Sign = 1w ∨ infP ∧ signP = 0w then
           (clear_flags,float_plus_infinity (:τ # χ))
         else if float_is_infinite z ∧ z.Sign = 0w ∨ infP ∧ signP = 1w then
           (clear_flags,float_minus_infinity (:τ # χ))
         else
           (let
              r1 = float_to_real x * float_to_real y and r2 = float_to_real z
            in
              float_round_with_flags mode
                (if r1 = 0 ∧ r2 = 0 ∧ signP ≠ z.Sign then signP = 1w
                 else (mode = roundTowardNegative)) (r1 − r2)))
float_compare_TY_DEF 
⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep
float_compare_BIJ 
⊢ (∀a. num2float_compare (float_compare2num a) = a) ∧
  ∀r. (λn. n < 4) r ⇔ float_compare2num (num2float_compare r) = r
float_compare_size_def 
⊢ ∀x. float_compare_size x = 0
float_compare_CASE 
⊢ ∀x v0 v1 v2 v3.
      (case x of LT => v0 | EQ => v1 | GT => v2 | UN => v3) =
      (λm.
           if m < 1 then v0
           else if m < 2 then v1
           else if m = 2 then v2
           else v3) (float_compare2num x)
float_compare_def 
⊢ ∀x y.
      float_compare x y =
      case (float_value x,float_value y) of
        (Float r1,Float r2) =>
          if r1 < r2 then LT else if r1 = r2 then EQ else GT
      | (Float r1,Infinity) => if y.Sign = 1w then GT else LT
      | (Float r1,NaN) => UN
      | (Infinity,Float v7) => if x.Sign = 1w then LT else GT
      | (Infinity,Infinity) =>
        if x.Sign = y.Sign then EQ else if x.Sign = 1w then LT else GT
      | (Infinity,NaN) => UN
      | (NaN,v1) => UN
float_less_than_def 
⊢ ∀x y. float_less_than x y ⇔ float_compare x y = LT
float_less_equal_def 
⊢ ∀x y.
      float_less_equal x y ⇔
      case float_compare x y of LT => T | EQ => T | GT => F | UN => F
float_greater_than_def 
⊢ ∀x y. float_greater_than x y ⇔ float_compare x y = GT
float_greater_equal_def 
⊢ ∀x y.
      float_greater_equal x y ⇔
      case float_compare x y of LT => F | EQ => T | GT => T | UN => F
float_equal_def 
⊢ ∀x y. float_equal x y ⇔ float_compare x y = EQ
exponent_boundary_def 
⊢ ∀y x.
      exponent_boundary y x ⇔
      x.Sign = y.Sign ∧ w2n x.Exponent = w2n y.Exponent + 1 ∧
      x.Exponent ≠ 1w ∧ y.Significand = -1w ∧ x.Significand = 0w

Theorems

float_accessors 
⊢ (∀c c0 c1. (float c c0 c1).Sign = c) ∧
  (∀c c0 c1. (float c c0 c1).Exponent = c0) ∧
  ∀c c0 c1. (float c c0 c1).Significand = c1
float_fn_updates 
⊢ (∀f c c0 c1. float c c0 c1 with Sign updated_by f = float (f c) c0 c1) ∧
  (∀f c c0 c1. float c c0 c1 with Exponent updated_by f = float c (f c0) c1) ∧
  ∀f c c0 c1. float c c0 c1 with Significand updated_by f = float c c0 (f c1)
float_accfupds 
⊢ (∀f0 f. (f with Exponent updated_by f0).Sign = f.Sign) ∧
  (∀f0 f. (f with Significand updated_by f0).Sign = f.Sign) ∧
  (∀f0 f. (f with Sign updated_by f0).Exponent = f.Exponent) ∧
  (∀f0 f. (f with Significand updated_by f0).Exponent = f.Exponent) ∧
  (∀f0 f. (f with Sign updated_by f0).Significand = f.Significand) ∧
  (∀f0 f. (f with Exponent updated_by f0).Significand = f.Significand) ∧
  (∀f0 f. (f with Sign updated_by f0).Sign = f0 f.Sign) ∧
  (∀f0 f. (f with Exponent updated_by f0).Exponent = f0 f.Exponent) ∧
  ∀f0 f. (f with Significand updated_by f0).Significand = f0 f.Significand
float_fupdfupds 
⊢ (∀g f0 f.
       f with <|Sign updated_by f0; Sign updated_by g|> =
       f with Sign updated_by f0 ∘ g) ∧
  (∀g f0 f.
       f with <|Exponent updated_by f0; Exponent updated_by g|> =
       f with Exponent updated_by f0 ∘ g) ∧
  ∀g f0 f.
      f with <|Significand updated_by f0; Significand updated_by g|> =
      f with Significand updated_by f0 ∘ g
float_fupdfupds_comp 
⊢ ((∀g f0. Sign_fupd f0 ∘ Sign_fupd g = Sign_fupd (f0 ∘ g)) ∧
   ∀h g f0. Sign_fupd f0 ∘ Sign_fupd g ∘ h = Sign_fupd (f0 ∘ g) ∘ h) ∧
  ((∀g f0. Exponent_fupd f0 ∘ Exponent_fupd g = Exponent_fupd (f0 ∘ g)) ∧
   ∀h g f0.
       Exponent_fupd f0 ∘ Exponent_fupd g ∘ h = Exponent_fupd (f0 ∘ g) ∘ h) ∧
  (∀g f0. Significand_fupd f0 ∘ Significand_fupd g = Significand_fupd (f0 ∘ g)) ∧
  ∀h g f0.
      Significand_fupd f0 ∘ Significand_fupd g ∘ h =
      Significand_fupd (f0 ∘ g) ∘ h
float_fupdcanon 
⊢ (∀g f0 f.
       f with <|Exponent updated_by f0; Sign updated_by g|> =
       f with <|Sign updated_by g; Exponent updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Significand updated_by f0; Sign updated_by g|> =
       f with <|Sign updated_by g; Significand updated_by f0|>) ∧
  ∀g f0 f.
      f with <|Significand updated_by f0; Exponent updated_by g|> =
      f with <|Exponent updated_by g; Significand updated_by f0|>
float_fupdcanon_comp 
⊢ ((∀g f0. Exponent_fupd f0 ∘ Sign_fupd g = Sign_fupd g ∘ Exponent_fupd f0) ∧
   ∀h g f0.
       Exponent_fupd f0 ∘ Sign_fupd g ∘ h = Sign_fupd g ∘ Exponent_fupd f0 ∘ h) ∧
  ((∀g f0.
        Significand_fupd f0 ∘ Sign_fupd g = Sign_fupd g ∘ Significand_fupd f0) ∧
   ∀h g f0.
       Significand_fupd f0 ∘ Sign_fupd g ∘ h =
       Sign_fupd g ∘ Significand_fupd f0 ∘ h) ∧
  (∀g f0.
       Significand_fupd f0 ∘ Exponent_fupd g =
       Exponent_fupd g ∘ Significand_fupd f0) ∧
  ∀h g f0.
      Significand_fupd f0 ∘ Exponent_fupd g ∘ h =
      Exponent_fupd g ∘ Significand_fupd f0 ∘ h
float_component_equality 
⊢ ∀f1 f2.
      f1 = f2 ⇔
      f1.Sign = f2.Sign ∧ f1.Exponent = f2.Exponent ∧
      f1.Significand = f2.Significand
float_updates_eq_literal 
⊢ ∀f c1 c0 c.
      f with <|Sign := c1; Exponent := c0; Significand := c|> =
      <|Sign := c1; Exponent := c0; Significand := c|>
float_literal_nchotomy 
⊢ ∀f. ∃c1 c0 c. f = <|Sign := c1; Exponent := c0; Significand := c|>
FORALL_float 
⊢ ∀P. (∀f. P f) ⇔ ∀c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>
EXISTS_float 
⊢ ∀P. (∃f. P f) ⇔ ∃c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>
float_literal_11 
⊢ ∀c11 c01 c1 c12 c02 c2.
      <|Sign := c11; Exponent := c01; Significand := c1|> =
      <|Sign := c12; Exponent := c02; Significand := c2|> ⇔
      c11 = c12 ∧ c01 = c02 ∧ c1 = c2
datatype_float 
⊢ DATATYPE (record float Sign Exponent Significand)
float_11 
⊢ ∀a0 a1 a2 a0' a1' a2'.
      float a0 a1 a2 = float a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
float_nchotomy 
⊢ ∀ff. ∃c c0 c1. ff = float c c0 c1
float_Axiom 
⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (float a0 a1 a2) = f a0 a1 a2
float_induction 
⊢ ∀P. (∀c c0 c1. P (float c c0 c1)) ⇒ ∀f. P f
float_case_cong 
⊢ ∀M M' f.
      M = M' ∧ (∀a0 a1 a2. M' = float a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
      float_CASE M f = float_CASE M' f'
float_case_eq 
⊢ float_CASE x f = v ⇔ ∃c c0 c1. x = float c c0 c1 ∧ f c c0 c1 = v
datatype_float_value 
⊢ DATATYPE (float_value Float Infinity NaN)
float_value_11 
⊢ ∀a a'. Float a = Float a' ⇔ a = a'
float_value_distinct 
⊢ (∀a. Float a ≠ Infinity) ∧ (∀a. Float a ≠ NaN) ∧ Infinity ≠ NaN
float_value_nchotomy 
⊢ ∀ff. (∃r. ff = Float r) ∨ ff = Infinity ∨ ff = NaN
float_value_Axiom 
⊢ ∀f0 f1 f2. ∃fn. (∀a. fn (Float a) = f0 a) ∧ fn Infinity = f1 ∧ fn NaN = f2
float_value_induction 
⊢ ∀P. (∀r. P (Float r)) ∧ P Infinity ∧ P NaN ⇒ ∀f. P f
float_value_case_cong 
⊢ ∀M M' f v v1.
      M = M' ∧ (∀a. M' = Float a ⇒ f a = f' a) ∧ (M' = Infinity ⇒ v = v') ∧
      (M' = NaN ⇒ v1 = v1') ⇒
      float_value_CASE M f v v1 = float_value_CASE M' f' v' v1'
float_value_case_eq 
⊢ float_value_CASE x f v v1 = v' ⇔
  (∃r. x = Float r ∧ f r = v') ∨ x = Infinity ∧ v = v' ∨ x = NaN ∧ v1 = v'
flags_accessors 
⊢ (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b) ∧
  (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0) ∧
  (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1) ∧
  (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2) ∧
  (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3) ∧
  ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ b4
flags_fn_updates 
⊢ (∀f b b0 b1 b2 b3 b4.
       flags b b0 b1 b2 b3 b4 with DivideByZero updated_by f =
       flags (f b) b0 b1 b2 b3 b4) ∧
  (∀f b b0 b1 b2 b3 b4.
       flags b b0 b1 b2 b3 b4 with InvalidOp updated_by f =
       flags b (f b0) b1 b2 b3 b4) ∧
  (∀f b b0 b1 b2 b3 b4.
       flags b b0 b1 b2 b3 b4 with Overflow updated_by f =
       flags b b0 (f b1) b2 b3 b4) ∧
  (∀f b b0 b1 b2 b3 b4.
       flags b b0 b1 b2 b3 b4 with Precision updated_by f =
       flags b b0 b1 (f b2) b3 b4) ∧
  (∀f b b0 b1 b2 b3 b4.
       flags b b0 b1 b2 b3 b4 with Underflow_BeforeRounding updated_by f =
       flags b b0 b1 b2 (f b3) b4) ∧
  ∀f b b0 b1 b2 b3 b4.
      flags b b0 b1 b2 b3 b4 with Underflow_AfterRounding updated_by f =
      flags b b0 b1 b2 b3 (f b4)
flags_accfupds 
⊢ (∀f0 f. (f with InvalidOp updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
  (∀f0 f. (f with Overflow updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
  (∀f0 f. (f with Precision updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
  (∀f0 f.
       (f with Underflow_BeforeRounding updated_by f0).DivideByZero ⇔
       f.DivideByZero) ∧
  (∀f0 f.
       (f with Underflow_AfterRounding updated_by f0).DivideByZero ⇔
       f.DivideByZero) ∧
  (∀f0 f. (f with DivideByZero updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
  (∀f0 f. (f with Overflow updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
  (∀f0 f. (f with Precision updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
  (∀f0 f.
       (f with Underflow_BeforeRounding updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
  (∀f0 f.
       (f with Underflow_AfterRounding updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
  (∀f0 f. (f with DivideByZero updated_by f0).Overflow ⇔ f.Overflow) ∧
  (∀f0 f. (f with InvalidOp updated_by f0).Overflow ⇔ f.Overflow) ∧
  (∀f0 f. (f with Precision updated_by f0).Overflow ⇔ f.Overflow) ∧
  (∀f0 f.
       (f with Underflow_BeforeRounding updated_by f0).Overflow ⇔ f.Overflow) ∧
  (∀f0 f. (f with Underflow_AfterRounding updated_by f0).Overflow ⇔ f.Overflow) ∧
  (∀f0 f. (f with DivideByZero updated_by f0).Precision ⇔ f.Precision) ∧
  (∀f0 f. (f with InvalidOp updated_by f0).Precision ⇔ f.Precision) ∧
  (∀f0 f. (f with Overflow updated_by f0).Precision ⇔ f.Precision) ∧
  (∀f0 f.
       (f with Underflow_BeforeRounding updated_by f0).Precision ⇔ f.Precision) ∧
  (∀f0 f.
       (f with Underflow_AfterRounding updated_by f0).Precision ⇔ f.Precision) ∧
  (∀f0 f.
       (f with DivideByZero updated_by f0).Underflow_BeforeRounding ⇔
       f.Underflow_BeforeRounding) ∧
  (∀f0 f.
       (f with InvalidOp updated_by f0).Underflow_BeforeRounding ⇔
       f.Underflow_BeforeRounding) ∧
  (∀f0 f.
       (f with Overflow updated_by f0).Underflow_BeforeRounding ⇔
       f.Underflow_BeforeRounding) ∧
  (∀f0 f.
       (f with Precision updated_by f0).Underflow_BeforeRounding ⇔
       f.Underflow_BeforeRounding) ∧
  (∀f0 f.
       (f with Underflow_AfterRounding updated_by f0).Underflow_BeforeRounding ⇔
       f.Underflow_BeforeRounding) ∧
  (∀f0 f.
       (f with DivideByZero updated_by f0).Underflow_AfterRounding ⇔
       f.Underflow_AfterRounding) ∧
  (∀f0 f.
       (f with InvalidOp updated_by f0).Underflow_AfterRounding ⇔
       f.Underflow_AfterRounding) ∧
  (∀f0 f.
       (f with Overflow updated_by f0).Underflow_AfterRounding ⇔
       f.Underflow_AfterRounding) ∧
  (∀f0 f.
       (f with Precision updated_by f0).Underflow_AfterRounding ⇔
       f.Underflow_AfterRounding) ∧
  (∀f0 f.
       (f with Underflow_BeforeRounding updated_by f0).Underflow_AfterRounding ⇔
       f.Underflow_AfterRounding) ∧
  (∀f0 f. (f with DivideByZero updated_by f0).DivideByZero ⇔ f0 f.DivideByZero) ∧
  (∀f0 f. (f with InvalidOp updated_by f0).InvalidOp ⇔ f0 f.InvalidOp) ∧
  (∀f0 f. (f with Overflow updated_by f0).Overflow ⇔ f0 f.Overflow) ∧
  (∀f0 f. (f with Precision updated_by f0).Precision ⇔ f0 f.Precision) ∧
  (∀f0 f.
       (f with Underflow_BeforeRounding updated_by f0).
       Underflow_BeforeRounding ⇔ f0 f.Underflow_BeforeRounding) ∧
  ∀f0 f.
      (f with Underflow_AfterRounding updated_by f0).Underflow_AfterRounding ⇔
      f0 f.Underflow_AfterRounding
flags_fupdfupds 
⊢ (∀g f0 f.
       f with <|DivideByZero updated_by f0; DivideByZero updated_by g|> =
       f with DivideByZero updated_by f0 ∘ g) ∧
  (∀g f0 f.
       f with <|InvalidOp updated_by f0; InvalidOp updated_by g|> =
       f with InvalidOp updated_by f0 ∘ g) ∧
  (∀g f0 f.
       f with <|Overflow updated_by f0; Overflow updated_by g|> =
       f with Overflow updated_by f0 ∘ g) ∧
  (∀g f0 f.
       f with <|Precision updated_by f0; Precision updated_by g|> =
       f with Precision updated_by f0 ∘ g) ∧
  (∀g f0 f.
       f with
       <|Underflow_BeforeRounding updated_by f0;
         Underflow_BeforeRounding updated_by g|> =
       f with Underflow_BeforeRounding updated_by f0 ∘ g) ∧
  ∀g f0 f.
      f with
      <|Underflow_AfterRounding updated_by f0;
        Underflow_AfterRounding updated_by g|> =
      f with Underflow_AfterRounding updated_by f0 ∘ g
flags_fupdfupds_comp 
⊢ ((∀g f0.
        DivideByZero_fupd f0 ∘ DivideByZero_fupd g =
        DivideByZero_fupd (f0 ∘ g)) ∧
   ∀h g f0.
       DivideByZero_fupd f0 ∘ DivideByZero_fupd g ∘ h =
       DivideByZero_fupd (f0 ∘ g) ∘ h) ∧
  ((∀g f0. InvalidOp_fupd f0 ∘ InvalidOp_fupd g = InvalidOp_fupd (f0 ∘ g)) ∧
   ∀h g f0.
       InvalidOp_fupd f0 ∘ InvalidOp_fupd g ∘ h = InvalidOp_fupd (f0 ∘ g) ∘ h) ∧
  ((∀g f0. Overflow_fupd f0 ∘ Overflow_fupd g = Overflow_fupd (f0 ∘ g)) ∧
   ∀h g f0.
       Overflow_fupd f0 ∘ Overflow_fupd g ∘ h = Overflow_fupd (f0 ∘ g) ∘ h) ∧
  ((∀g f0. Precision_fupd f0 ∘ Precision_fupd g = Precision_fupd (f0 ∘ g)) ∧
   ∀h g f0.
       Precision_fupd f0 ∘ Precision_fupd g ∘ h = Precision_fupd (f0 ∘ g) ∘ h) ∧
  ((∀g f0.
        Underflow_BeforeRounding_fupd f0 ∘ Underflow_BeforeRounding_fupd g =
        Underflow_BeforeRounding_fupd (f0 ∘ g)) ∧
   ∀h g f0.
       Underflow_BeforeRounding_fupd f0 ∘ Underflow_BeforeRounding_fupd g ∘ h =
       Underflow_BeforeRounding_fupd (f0 ∘ g) ∘ h) ∧
  (∀g f0.
       Underflow_AfterRounding_fupd f0 ∘ Underflow_AfterRounding_fupd g =
       Underflow_AfterRounding_fupd (f0 ∘ g)) ∧
  ∀h g f0.
      Underflow_AfterRounding_fupd f0 ∘ Underflow_AfterRounding_fupd g ∘ h =
      Underflow_AfterRounding_fupd (f0 ∘ g) ∘ h
flags_fupdcanon 
⊢ (∀g f0 f.
       f with <|InvalidOp updated_by f0; DivideByZero updated_by g|> =
       f with <|DivideByZero updated_by g; InvalidOp updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Overflow updated_by f0; DivideByZero updated_by g|> =
       f with <|DivideByZero updated_by g; Overflow updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Overflow updated_by f0; InvalidOp updated_by g|> =
       f with <|InvalidOp updated_by g; Overflow updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Precision updated_by f0; DivideByZero updated_by g|> =
       f with <|DivideByZero updated_by g; Precision updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Precision updated_by f0; InvalidOp updated_by g|> =
       f with <|InvalidOp updated_by g; Precision updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Precision updated_by f0; Overflow updated_by g|> =
       f with <|Overflow updated_by g; Precision updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_BeforeRounding updated_by f0; DivideByZero updated_by g|> =
       f with
       <|DivideByZero updated_by g; Underflow_BeforeRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_BeforeRounding updated_by f0; InvalidOp updated_by g|> =
       f with
       <|InvalidOp updated_by g; Underflow_BeforeRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_BeforeRounding updated_by f0; Overflow updated_by g|> =
       f with
       <|Overflow updated_by g; Underflow_BeforeRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_BeforeRounding updated_by f0; Precision updated_by g|> =
       f with
       <|Precision updated_by g; Underflow_BeforeRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_AfterRounding updated_by f0; DivideByZero updated_by g|> =
       f with
       <|DivideByZero updated_by g; Underflow_AfterRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_AfterRounding updated_by f0; InvalidOp updated_by g|> =
       f with
       <|InvalidOp updated_by g; Underflow_AfterRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with <|Underflow_AfterRounding updated_by f0; Overflow updated_by g|> =
       f with <|Overflow updated_by g; Underflow_AfterRounding updated_by f0|>) ∧
  (∀g f0 f.
       f with
       <|Underflow_AfterRounding updated_by f0; Precision updated_by g|> =
       f with
       <|Precision updated_by g; Underflow_AfterRounding updated_by f0|>) ∧
  ∀g f0 f.
      f with
      <|Underflow_AfterRounding updated_by f0;
        Underflow_BeforeRounding updated_by g|> =
      f with
      <|Underflow_BeforeRounding updated_by g;
        Underflow_AfterRounding updated_by f0|>
flags_fupdcanon_comp 
⊢ ((∀g f0.
        InvalidOp_fupd f0 ∘ DivideByZero_fupd g =
        DivideByZero_fupd g ∘ InvalidOp_fupd f0) ∧
   ∀h g f0.
       InvalidOp_fupd f0 ∘ DivideByZero_fupd g ∘ h =
       DivideByZero_fupd g ∘ InvalidOp_fupd f0 ∘ h) ∧
  ((∀g f0.
        Overflow_fupd f0 ∘ DivideByZero_fupd g =
        DivideByZero_fupd g ∘ Overflow_fupd f0) ∧
   ∀h g f0.
       Overflow_fupd f0 ∘ DivideByZero_fupd g ∘ h =
       DivideByZero_fupd g ∘ Overflow_fupd f0 ∘ h) ∧
  ((∀g f0.
        Overflow_fupd f0 ∘ InvalidOp_fupd g =
        InvalidOp_fupd g ∘ Overflow_fupd f0) ∧
   ∀h g f0.
       Overflow_fupd f0 ∘ InvalidOp_fupd g ∘ h =
       InvalidOp_fupd g ∘ Overflow_fupd f0 ∘ h) ∧
  ((∀g f0.
        Precision_fupd f0 ∘ DivideByZero_fupd g =
        DivideByZero_fupd g ∘ Precision_fupd f0) ∧
   ∀h g f0.
       Precision_fupd f0 ∘ DivideByZero_fupd g ∘ h =
       DivideByZero_fupd g ∘ Precision_fupd f0 ∘ h) ∧
  ((∀g f0.
        Precision_fupd f0 ∘ InvalidOp_fupd g =
        InvalidOp_fupd g ∘ Precision_fupd f0) ∧
   ∀h g f0.
       Precision_fupd f0 ∘ InvalidOp_fupd g ∘ h =
       InvalidOp_fupd g ∘ Precision_fupd f0 ∘ h) ∧
  ((∀g f0.
        Precision_fupd f0 ∘ Overflow_fupd g =
        Overflow_fupd g ∘ Precision_fupd f0) ∧
   ∀h g f0.
       Precision_fupd f0 ∘ Overflow_fupd g ∘ h =
       Overflow_fupd g ∘ Precision_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_BeforeRounding_fupd f0 ∘ DivideByZero_fupd g =
        DivideByZero_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_BeforeRounding_fupd f0 ∘ DivideByZero_fupd g ∘ h =
       DivideByZero_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_BeforeRounding_fupd f0 ∘ InvalidOp_fupd g =
        InvalidOp_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_BeforeRounding_fupd f0 ∘ InvalidOp_fupd g ∘ h =
       InvalidOp_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_BeforeRounding_fupd f0 ∘ Overflow_fupd g =
        Overflow_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_BeforeRounding_fupd f0 ∘ Overflow_fupd g ∘ h =
       Overflow_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_BeforeRounding_fupd f0 ∘ Precision_fupd g =
        Precision_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_BeforeRounding_fupd f0 ∘ Precision_fupd g ∘ h =
       Precision_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_AfterRounding_fupd f0 ∘ DivideByZero_fupd g =
        DivideByZero_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_AfterRounding_fupd f0 ∘ DivideByZero_fupd g ∘ h =
       DivideByZero_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_AfterRounding_fupd f0 ∘ InvalidOp_fupd g =
        InvalidOp_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_AfterRounding_fupd f0 ∘ InvalidOp_fupd g ∘ h =
       InvalidOp_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_AfterRounding_fupd f0 ∘ Overflow_fupd g =
        Overflow_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_AfterRounding_fupd f0 ∘ Overflow_fupd g ∘ h =
       Overflow_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
  ((∀g f0.
        Underflow_AfterRounding_fupd f0 ∘ Precision_fupd g =
        Precision_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
   ∀h g f0.
       Underflow_AfterRounding_fupd f0 ∘ Precision_fupd g ∘ h =
       Precision_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
  (∀g f0.
       Underflow_AfterRounding_fupd f0 ∘ Underflow_BeforeRounding_fupd g =
       Underflow_BeforeRounding_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
  ∀h g f0.
      Underflow_AfterRounding_fupd f0 ∘ Underflow_BeforeRounding_fupd g ∘ h =
      Underflow_BeforeRounding_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h
flags_component_equality 
⊢ ∀f1 f2.
      f1 = f2 ⇔
      (f1.DivideByZero ⇔ f2.DivideByZero) ∧ (f1.InvalidOp ⇔ f2.InvalidOp) ∧
      (f1.Overflow ⇔ f2.Overflow) ∧ (f1.Precision ⇔ f2.Precision) ∧
      (f1.Underflow_BeforeRounding ⇔ f2.Underflow_BeforeRounding) ∧
      (f1.Underflow_AfterRounding ⇔ f2.Underflow_AfterRounding)
flags_updates_eq_literal 
⊢ ∀f b4 b3 b2 b1 b0 b.
      f with
      <|DivideByZero := b4; InvalidOp := b3; Overflow := b2; Precision := b1;
        Underflow_BeforeRounding := b0; Underflow_AfterRounding := b|> =
      <|DivideByZero := b4; InvalidOp := b3; Overflow := b2; Precision := b1;
        Underflow_BeforeRounding := b0; Underflow_AfterRounding := b|>
flags_literal_nchotomy 
⊢ ∀f.
      ∃b4 b3 b2 b1 b0 b.
          f =
          <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
            Precision := b1; Underflow_BeforeRounding := b0;
            Underflow_AfterRounding := b|>
FORALL_flags 
⊢ ∀P.
      (∀f. P f) ⇔
      ∀b4 b3 b2 b1 b0 b.
          P
            <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
            Precision := b1; Underflow_BeforeRounding := b0;
            Underflow_AfterRounding := b|>
EXISTS_flags 
⊢ ∀P.
      (∃f. P f) ⇔
      ∃b4 b3 b2 b1 b0 b.
          P
            <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
            Precision := b1; Underflow_BeforeRounding := b0;
            Underflow_AfterRounding := b|>
flags_literal_11 
⊢ ∀b41 b31 b21 b11 b01 b1 b42 b32 b22 b12 b02 b2.
      <|DivideByZero := b41; InvalidOp := b31; Overflow := b21;
        Precision := b11; Underflow_BeforeRounding := b01;
        Underflow_AfterRounding := b1|> =
      <|DivideByZero := b42; InvalidOp := b32; Overflow := b22;
        Precision := b12; Underflow_BeforeRounding := b02;
        Underflow_AfterRounding := b2|> ⇔
      (b41 ⇔ b42) ∧ (b31 ⇔ b32) ∧ (b21 ⇔ b22) ∧ (b11 ⇔ b12) ∧ (b01 ⇔ b02) ∧
      (b1 ⇔ b2)
datatype_flags 
⊢ DATATYPE
    (record flags DivideByZero InvalidOp Overflow Precision
       Underflow_BeforeRounding Underflow_AfterRounding)
flags_11 
⊢ ∀a0 a1 a2 a3 a4 a5 a0' a1' a2' a3' a4' a5'.
      flags a0 a1 a2 a3 a4 a5 = flags a0' a1' a2' a3' a4' a5' ⇔
      (a0 ⇔ a0') ∧ (a1 ⇔ a1') ∧ (a2 ⇔ a2') ∧ (a3 ⇔ a3') ∧ (a4 ⇔ a4') ∧
      (a5 ⇔ a5')
flags_nchotomy 
⊢ ∀ff. ∃b b0 b1 b2 b3 b4. ff = flags b b0 b1 b2 b3 b4
flags_Axiom 
⊢ ∀f.
      ∃fn.
          ∀a0 a1 a2 a3 a4 a5.
              fn (flags a0 a1 a2 a3 a4 a5) = f a0 a1 a2 a3 a4 a5
flags_induction 
⊢ ∀P. (∀b b0 b1 b2 b3 b4. P (flags b b0 b1 b2 b3 b4)) ⇒ ∀f. P f
flags_case_cong 
⊢ ∀M M' f.
      M = M' ∧
      (∀a0 a1 a2 a3 a4 a5.
           M' = flags a0 a1 a2 a3 a4 a5 ⇒
           f a0 a1 a2 a3 a4 a5 = f' a0 a1 a2 a3 a4 a5) ⇒
      flags_CASE M f = flags_CASE M' f'
flags_case_eq 
⊢ flags_CASE x f = v ⇔
  ∃b b0 b1 b2 b3 b4. x = flags b b0 b1 b2 b3 b4 ∧ f b b0 b1 b2 b3 b4 = v
num2rounding_rounding2num 
⊢ ∀a. num2rounding (rounding2num a) = a
rounding2num_num2rounding 
⊢ ∀r. r < 4 ⇔ rounding2num (num2rounding r) = r
num2rounding_11 
⊢ ∀r r'. r < 4 ⇒ r' < 4 ⇒ (num2rounding r = num2rounding r' ⇔ r = r')
rounding2num_11 
⊢ ∀a a'. rounding2num a = rounding2num a' ⇔ a = a'
num2rounding_ONTO 
⊢ ∀a. ∃r. a = num2rounding r ∧ r < 4
rounding2num_ONTO 
⊢ ∀r. r < 4 ⇔ ∃a. r = rounding2num a
num2rounding_thm 
⊢ num2rounding 0 = roundTiesToEven ∧ num2rounding 1 = roundTowardPositive ∧
  num2rounding 2 = roundTowardNegative ∧ num2rounding 3 = roundTowardZero
rounding2num_thm 
⊢ rounding2num roundTiesToEven = 0 ∧ rounding2num roundTowardPositive = 1 ∧
  rounding2num roundTowardNegative = 2 ∧ rounding2num roundTowardZero = 3
rounding_EQ_rounding 
⊢ ∀a a'. a = a' ⇔ rounding2num a = rounding2num a'
rounding_case_def 
⊢ (∀v0 v1 v2 v3.
       (case roundTiesToEven of
          roundTiesToEven => v0
        | roundTowardPositive => v1
        | roundTowardNegative => v2
        | roundTowardZero => v3) = v0) ∧
  (∀v0 v1 v2 v3.
       (case roundTowardPositive of
          roundTiesToEven => v0
        | roundTowardPositive => v1
        | roundTowardNegative => v2
        | roundTowardZero => v3) = v1) ∧
  (∀v0 v1 v2 v3.
       (case roundTowardNegative of
          roundTiesToEven => v0
        | roundTowardPositive => v1
        | roundTowardNegative => v2
        | roundTowardZero => v3) = v2) ∧
  ∀v0 v1 v2 v3.
      (case roundTowardZero of
         roundTiesToEven => v0
       | roundTowardPositive => v1
       | roundTowardNegative => v2
       | roundTowardZero => v3) = v3
datatype_rounding 
⊢ DATATYPE
    (rounding roundTiesToEven roundTowardPositive roundTowardNegative
       roundTowardZero)
rounding_distinct 
⊢ roundTiesToEven ≠ roundTowardPositive ∧
  roundTiesToEven ≠ roundTowardNegative ∧ roundTiesToEven ≠ roundTowardZero ∧
  roundTowardPositive ≠ roundTowardNegative ∧
  roundTowardPositive ≠ roundTowardZero ∧
  roundTowardNegative ≠ roundTowardZero
rounding_nchotomy 
⊢ ∀a.
      a = roundTiesToEven ∨ a = roundTowardPositive ∨
      a = roundTowardNegative ∨ a = roundTowardZero
rounding_Axiom 
⊢ ∀x0 x1 x2 x3.
      ∃f.
          f roundTiesToEven = x0 ∧ f roundTowardPositive = x1 ∧
          f roundTowardNegative = x2 ∧ f roundTowardZero = x3
rounding_induction 
⊢ ∀P.
      P roundTiesToEven ∧ P roundTowardNegative ∧ P roundTowardPositive ∧
      P roundTowardZero ⇒
      ∀a. P a
rounding_case_cong 
⊢ ∀M M' v0 v1 v2 v3.
      M = M' ∧ (M' = roundTiesToEven ⇒ v0 = v0') ∧
      (M' = roundTowardPositive ⇒ v1 = v1') ∧
      (M' = roundTowardNegative ⇒ v2 = v2') ∧
      (M' = roundTowardZero ⇒ v3 = v3') ⇒
      (case M of
         roundTiesToEven => v0
       | roundTowardPositive => v1
       | roundTowardNegative => v2
       | roundTowardZero => v3) =
      case M' of
        roundTiesToEven => v0'
      | roundTowardPositive => v1'
      | roundTowardNegative => v2'
      | roundTowardZero => v3'
rounding_case_eq 
⊢ (case x of
     roundTiesToEven => v0
   | roundTowardPositive => v1
   | roundTowardNegative => v2
   | roundTowardZero => v3) = v ⇔
  x = roundTiesToEven ∧ v0 = v ∨ x = roundTowardPositive ∧ v1 = v ∨
  x = roundTowardNegative ∧ v2 = v ∨ x = roundTowardZero ∧ v3 = v
ULP_ind 
⊢ ∀P. (∀e. P (e,(:τ))) ⇒ ∀v v1. P (v,v1)
ULP_def 
⊢ ULP (e,(:τ)) =
  2 pow (if e = 0w then 1 else w2n e) / 2 pow (INT_MAX (:χ) + dimindex (:τ))
datatype_fp_op 
⊢ DATATYPE (fp_op FP_Sqrt FP_Add FP_Sub FP_Mul FP_Div FP_MulAdd FP_MulSub)
fp_op_11 
⊢ (∀a0 a1 a0' a1'. FP_Sqrt a0 a1 = FP_Sqrt a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
  (∀a0 a1 a2 a0' a1' a2'.
       FP_Add a0 a1 a2 = FP_Add a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
  (∀a0 a1 a2 a0' a1' a2'.
       FP_Sub a0 a1 a2 = FP_Sub a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
  (∀a0 a1 a2 a0' a1' a2'.
       FP_Mul a0 a1 a2 = FP_Mul a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
  (∀a0 a1 a2 a0' a1' a2'.
       FP_Div a0 a1 a2 = FP_Div a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
  (∀a0 a1 a2 a3 a0' a1' a2' a3'.
       FP_MulAdd a0 a1 a2 a3 = FP_MulAdd a0' a1' a2' a3' ⇔
       a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3') ∧
  ∀a0 a1 a2 a3 a0' a1' a2' a3'.
      FP_MulSub a0 a1 a2 a3 = FP_MulSub a0' a1' a2' a3' ⇔
      a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3'
fp_op_distinct 
⊢ (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Add a0' a1' a2) ∧
  (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Sub a0' a1' a2) ∧
  (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Mul a0' a1' a2) ∧
  (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Div a0' a1' a2) ∧
  (∀a3 a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_MulAdd a0' a1' a2 a3) ∧
  (∀a3 a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_MulSub a0' a1' a2 a3) ∧
  (∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Sub a0' a1' a2') ∧
  (∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Mul a0' a1' a2') ∧
  (∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
  (∀a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_Mul a0' a1' a2') ∧
  (∀a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
  (∀a2' a2 a1' a1 a0' a0. FP_Mul a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Mul a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Mul a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Div a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
  (∀a3 a2' a2 a1' a1 a0' a0. FP_Div a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
  ∀a3' a3 a2' a2 a1' a1 a0' a0.
      FP_MulAdd a0 a1 a2 a3 ≠ FP_MulSub a0' a1' a2' a3'
fp_op_nchotomy 
⊢ ∀ff.
      (∃r f. ff = FP_Sqrt r f) ∨ (∃r f f0. ff = FP_Add r f f0) ∨
      (∃r f f0. ff = FP_Sub r f f0) ∨ (∃r f f0. ff = FP_Mul r f f0) ∨
      (∃r f f0. ff = FP_Div r f f0) ∨ (∃r f f0 f1. ff = FP_MulAdd r f f0 f1) ∨
      ∃r f f0 f1. ff = FP_MulSub r f f0 f1
fp_op_Axiom 
⊢ ∀f0 f1 f2 f3 f4 f5 f6.
      ∃fn.
          (∀a0 a1. fn (FP_Sqrt a0 a1) = f0 a0 a1) ∧
          (∀a0 a1 a2. fn (FP_Add a0 a1 a2) = f1 a0 a1 a2) ∧
          (∀a0 a1 a2. fn (FP_Sub a0 a1 a2) = f2 a0 a1 a2) ∧
          (∀a0 a1 a2. fn (FP_Mul a0 a1 a2) = f3 a0 a1 a2) ∧
          (∀a0 a1 a2. fn (FP_Div a0 a1 a2) = f4 a0 a1 a2) ∧
          (∀a0 a1 a2 a3. fn (FP_MulAdd a0 a1 a2 a3) = f5 a0 a1 a2 a3) ∧
          ∀a0 a1 a2 a3. fn (FP_MulSub a0 a1 a2 a3) = f6 a0 a1 a2 a3
fp_op_induction 
⊢ ∀P.
      (∀r f. P (FP_Sqrt r f)) ∧ (∀r f f0. P (FP_Add r f f0)) ∧
      (∀r f f0. P (FP_Sub r f f0)) ∧ (∀r f f0. P (FP_Mul r f f0)) ∧
      (∀r f f0. P (FP_Div r f f0)) ∧ (∀r f f0 f1. P (FP_MulAdd r f f0 f1)) ∧
      (∀r f f0 f1. P (FP_MulSub r f f0 f1)) ⇒
      ∀f. P f
fp_op_case_cong 
⊢ ∀M M' f f1 f2 f3 f4 f5 f6.
      M = M' ∧ (∀a0 a1. M' = FP_Sqrt a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
      (∀a0 a1 a2. M' = FP_Add a0 a1 a2 ⇒ f1 a0 a1 a2 = f1' a0 a1 a2) ∧
      (∀a0 a1 a2. M' = FP_Sub a0 a1 a2 ⇒ f2 a0 a1 a2 = f2' a0 a1 a2) ∧
      (∀a0 a1 a2. M' = FP_Mul a0 a1 a2 ⇒ f3 a0 a1 a2 = f3' a0 a1 a2) ∧
      (∀a0 a1 a2. M' = FP_Div a0 a1 a2 ⇒ f4 a0 a1 a2 = f4' a0 a1 a2) ∧
      (∀a0 a1 a2 a3.
           M' = FP_MulAdd a0 a1 a2 a3 ⇒ f5 a0 a1 a2 a3 = f5' a0 a1 a2 a3) ∧
      (∀a0 a1 a2 a3.
           M' = FP_MulSub a0 a1 a2 a3 ⇒ f6 a0 a1 a2 a3 = f6' a0 a1 a2 a3) ⇒
      fp_op_CASE M f f1 f2 f3 f4 f5 f6 =
      fp_op_CASE M' f' f1' f2' f3' f4' f5' f6'
fp_op_case_eq 
⊢ fp_op_CASE x f f1 f2 f3 f4 f5 f6 = v ⇔
  (∃r f'. x = FP_Sqrt r f' ∧ f r f' = v) ∨
  (∃r f' f0. x = FP_Add r f' f0 ∧ f1 r f' f0 = v) ∨
  (∃r f' f0. x = FP_Sub r f' f0 ∧ f2 r f' f0 = v) ∨
  (∃r f' f0. x = FP_Mul r f' f0 ∧ f3 r f' f0 = v) ∨
  (∃r f' f0. x = FP_Div r f' f0 ∧ f4 r f' f0 = v) ∨
  (∃r f' f0 f1'. x = FP_MulAdd r f' f0 f1' ∧ f5 r f' f0 f1' = v) ∨
  ∃r f' f0 f1'. x = FP_MulSub r f' f0 f1' ∧ f6 r f' f0 f1' = v
num2float_compare_float_compare2num 
⊢ ∀a. num2float_compare (float_compare2num a) = a
float_compare2num_num2float_compare 
⊢ ∀r. r < 4 ⇔ float_compare2num (num2float_compare r) = r
num2float_compare_11 
⊢ ∀r r'.
      r < 4 ⇒ r' < 4 ⇒ (num2float_compare r = num2float_compare r' ⇔ r = r')
float_compare2num_11 
⊢ ∀a a'. float_compare2num a = float_compare2num a' ⇔ a = a'
num2float_compare_ONTO 
⊢ ∀a. ∃r. a = num2float_compare r ∧ r < 4
float_compare2num_ONTO 
⊢ ∀r. r < 4 ⇔ ∃a. r = float_compare2num a
num2float_compare_thm 
⊢ num2float_compare 0 = LT ∧ num2float_compare 1 = EQ ∧
  num2float_compare 2 = GT ∧ num2float_compare 3 = UN
float_compare2num_thm 
⊢ float_compare2num LT = 0 ∧ float_compare2num EQ = 1 ∧
  float_compare2num GT = 2 ∧ float_compare2num UN = 3
float_compare_EQ_float_compare 
⊢ ∀a a'. a = a' ⇔ float_compare2num a = float_compare2num a'
float_compare_case_def 
⊢ (∀v0 v1 v2 v3. (case LT of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v0) ∧
  (∀v0 v1 v2 v3. (case EQ of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v1) ∧
  (∀v0 v1 v2 v3. (case GT of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v2) ∧
  ∀v0 v1 v2 v3. (case UN of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v3
datatype_float_compare 
⊢ DATATYPE (float_compare LT EQ GT UN)
float_compare_distinct 
⊢ LT ≠ EQ ∧ LT ≠ GT ∧ LT ≠ UN ∧ EQ ≠ GT ∧ EQ ≠ UN ∧ GT ≠ UN
float_compare_nchotomy 
⊢ ∀a. a = LT ∨ a = EQ ∨ a = GT ∨ a = UN
float_compare_Axiom 
⊢ ∀x0 x1 x2 x3. ∃f. f LT = x0 ∧ f EQ = x1 ∧ f GT = x2 ∧ f UN = x3
float_compare_induction 
⊢ ∀P. P EQ ∧ P GT ∧ P LT ∧ P UN ⇒ ∀a. P a
float_compare_case_cong 
⊢ ∀M M' v0 v1 v2 v3.
      M = M' ∧ (M' = LT ⇒ v0 = v0') ∧ (M' = EQ ⇒ v1 = v1') ∧
      (M' = GT ⇒ v2 = v2') ∧ (M' = UN ⇒ v3 = v3') ⇒
      (case M of LT => v0 | EQ => v1 | GT => v2 | UN => v3) =
      case M' of LT => v0' | EQ => v1' | GT => v2' | UN => v3'
float_compare_case_eq 
⊢ (case x of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v ⇔
  x = LT ∧ v0 = v ∨ x = EQ ∧ v1 = v ∨ x = GT ∧ v2 = v ∨ x = UN ∧ v3 = v
zero_lt_twopow 
⊢ ∀n. 0 < 2 pow n
zero_le_twopow 
⊢ ∀n. 0 ≤ 2 pow n
zero_neq_twopow 
⊢ ∀n. 2 pow n ≠ 0
zero_le_pos_div_twopow 
⊢ ∀m n. 0 ≤ &m / 2 pow n
div_eq0 
⊢ ∀a b. 0 < b ⇒ (a / b = 0 ⇔ a = 0)
exp_ge2 
⊢ ∀b. 2 ≤ 2 ** b ⇔ 1 ≤ b
exp_gt2 
⊢ ∀b. 2 < 2 ** b ⇔ 1 < b
le2 
⊢ ∀n m. 2 ≤ n ∧ 2 ≤ m ⇒ 2 ≤ n * m
float_components 
⊢ (float_plus_infinity (:τ # χ)).Sign = 0w ∧
  (float_plus_infinity (:τ # χ)).Exponent = UINT_MAXw ∧
  (float_plus_infinity (:τ # χ)).Significand = 0w ∧
  (float_minus_infinity (:τ # χ)).Sign = 1w ∧
  (float_minus_infinity (:τ # χ)).Exponent = UINT_MAXw ∧
  (float_minus_infinity (:τ # χ)).Significand = 0w ∧
  (float_plus_zero (:τ # χ)).Sign = 0w ∧
  (float_plus_zero (:τ # χ)).Exponent = 0w ∧
  (float_plus_zero (:τ # χ)).Significand = 0w ∧
  (float_minus_zero (:τ # χ)).Sign = 1w ∧
  (float_minus_zero (:τ # χ)).Exponent = 0w ∧
  (float_minus_zero (:τ # χ)).Significand = 0w ∧
  (float_plus_min (:τ # χ)).Sign = 0w ∧
  (float_plus_min (:τ # χ)).Exponent = 0w ∧
  (float_plus_min (:τ # χ)).Significand = 1w ∧
  (float_minus_min (:τ # χ)).Sign = 1w ∧
  (float_minus_min (:τ # χ)).Exponent = 0w ∧
  (float_minus_min (:τ # χ)).Significand = 1w ∧
  (float_top (:τ # χ)).Sign = 0w ∧
  (float_top (:τ # χ)).Exponent = UINT_MAXw − 1w ∧
  (float_top (:τ # χ)).Significand = UINT_MAXw ∧
  (float_bottom (:τ # χ)).Sign = 1w ∧
  (float_bottom (:τ # χ)).Exponent = UINT_MAXw − 1w ∧
  (float_bottom (:τ # χ)).Significand = UINT_MAXw ∧
  (∀fp_op. (float_some_qnan fp_op).Exponent = UINT_MAXw) ∧
  (∀fp_op. (float_some_qnan fp_op).Significand ≠ 0w) ∧
  (∀x. (float_negate x).Sign = ¬x.Sign) ∧
  (∀x. (float_negate x).Exponent = x.Exponent) ∧
  ∀x. (float_negate x).Significand = x.Significand
float_distinct 
⊢ float_plus_infinity (:τ # χ) ≠ float_minus_infinity (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ float_plus_zero (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ float_minus_zero (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ float_top (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ float_bottom (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. float_plus_infinity (:τ # χ) ≠ float_some_qnan fp_op) ∧
  float_minus_infinity (:τ # χ) ≠ float_plus_zero (:τ # χ) ∧
  float_minus_infinity (:τ # χ) ≠ float_minus_zero (:τ # χ) ∧
  float_minus_infinity (:τ # χ) ≠ float_top (:τ # χ) ∧
  float_minus_infinity (:τ # χ) ≠ float_bottom (:τ # χ) ∧
  float_minus_infinity (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
  float_minus_infinity (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. float_minus_infinity (:τ # χ) ≠ float_some_qnan fp_op) ∧
  float_plus_zero (:τ # χ) ≠ float_minus_zero (:τ # χ) ∧
  float_plus_zero (:τ # χ) ≠ float_top (:τ # χ) ∧
  float_plus_zero (:τ # χ) ≠ float_bottom (:τ # χ) ∧
  float_plus_zero (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
  float_plus_zero (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. float_plus_zero (:τ # χ) ≠ float_some_qnan fp_op) ∧
  float_minus_zero (:τ # χ) ≠ float_top (:τ # χ) ∧
  float_minus_zero (:τ # χ) ≠ float_bottom (:τ # χ) ∧
  float_minus_zero (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
  float_minus_zero (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. float_minus_zero (:τ # χ) ≠ float_some_qnan fp_op) ∧
  float_top (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
  float_top (:τ # χ) ≠ float_bottom (:τ # χ) ∧
  (∀fp_op. float_top (:τ # χ) ≠ float_some_qnan fp_op) ∧
  float_bottom (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
  (∀fp_op. float_bottom (:τ # χ) ≠ float_some_qnan fp_op) ∧
  (∀fp_op. float_plus_min (:τ # χ) ≠ float_some_qnan fp_op) ∧
  float_plus_min (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. float_minus_min (:τ # χ) ≠ float_some_qnan fp_op) ∧
  ∀x. float_negate x ≠ x
float_values 
⊢ float_value (float_plus_infinity (:τ # χ)) = Infinity ∧
  float_value (float_minus_infinity (:τ # χ)) = Infinity ∧
  (∀fp_op. float_value (float_some_qnan fp_op) = NaN) ∧
  float_value (float_plus_zero (:τ # χ)) = Float 0 ∧
  float_value (float_minus_zero (:τ # χ)) = Float 0 ∧
  float_value (float_plus_min (:τ # χ)) =
  Float (2 / 2 pow (INT_MAX (:χ) + dimindex (:τ))) ∧
  float_value (float_minus_min (:τ # χ)) =
  Float (-2 / 2 pow (INT_MAX (:χ) + dimindex (:τ)))
zero_to_real 
⊢ float_to_real (float_plus_zero (:τ # χ)) = 0 ∧
  float_to_real (float_minus_zero (:τ # χ)) = 0
sign_not_zero 
⊢ ∀s. -1 pow w2n s ≠ 0
float_sets 
⊢ float_is_zero = {float_minus_zero (:τ # χ); float_plus_zero (:τ # χ)} ∧
  float_is_infinite =
  {float_minus_infinity (:τ # χ); float_plus_infinity (:τ # χ)}
infinity_properties 
⊢ ¬float_is_zero (float_plus_infinity (:τ # χ)) ∧
  ¬float_is_zero (float_minus_infinity (:τ # χ)) ∧
  ¬float_is_finite (float_plus_infinity (:τ # χ)) ∧
  ¬float_is_finite (float_minus_infinity (:τ # χ)) ∧
  ¬float_is_integral (float_plus_infinity (:τ # χ)) ∧
  ¬float_is_integral (float_minus_infinity (:τ # χ)) ∧
  ¬float_is_nan (float_plus_infinity (:τ # χ)) ∧
  ¬float_is_nan (float_minus_infinity (:τ # χ)) ∧
  ¬float_is_normal (float_plus_infinity (:τ # χ)) ∧
  ¬float_is_normal (float_minus_infinity (:τ # χ)) ∧
  ¬float_is_subnormal (float_plus_infinity (:τ # χ)) ∧
  ¬float_is_subnormal (float_minus_infinity (:τ # χ)) ∧
  float_is_infinite (float_plus_infinity (:τ # χ)) ∧
  float_is_infinite (float_minus_infinity (:τ # χ))
zero_properties 
⊢ float_is_zero (float_plus_zero (:τ # χ)) ∧
  float_is_zero (float_minus_zero (:τ # χ)) ∧
  float_is_finite (float_plus_zero (:τ # χ)) ∧
  float_is_finite (float_minus_zero (:τ # χ)) ∧
  float_is_integral (float_plus_zero (:τ # χ)) ∧
  float_is_integral (float_minus_zero (:τ # χ)) ∧
  ¬float_is_nan (float_plus_zero (:τ # χ)) ∧
  ¬float_is_nan (float_minus_zero (:τ # χ)) ∧
  ¬float_is_normal (float_plus_zero (:τ # χ)) ∧
  ¬float_is_normal (float_minus_zero (:τ # χ)) ∧
  ¬float_is_subnormal (float_plus_zero (:τ # χ)) ∧
  ¬float_is_subnormal (float_minus_zero (:τ # χ)) ∧
  ¬float_is_infinite (float_plus_zero (:τ # χ)) ∧
  ¬float_is_infinite (float_minus_zero (:τ # χ))
some_nan_properties 
⊢ ∀fp_op.
      ¬float_is_zero (float_some_qnan fp_op) ∧
      ¬float_is_finite (float_some_qnan fp_op) ∧
      ¬float_is_integral (float_some_qnan fp_op) ∧
      float_is_nan (float_some_qnan fp_op) ∧
      ¬float_is_signalling (float_some_qnan fp_op) ∧
      ¬float_is_normal (float_some_qnan fp_op) ∧
      ¬float_is_subnormal (float_some_qnan fp_op) ∧
      ¬float_is_infinite (float_some_qnan fp_op)
min_properties 
⊢ ¬float_is_zero (float_plus_min (:τ # χ)) ∧
  float_is_finite (float_plus_min (:τ # χ)) ∧
  (float_is_integral (float_plus_min (:τ # χ)) ⇔
   dimindex (:χ) = 1 ∧ dimindex (:τ) = 1) ∧
  ¬float_is_nan (float_plus_min (:τ # χ)) ∧
  ¬float_is_normal (float_plus_min (:τ # χ)) ∧
  float_is_subnormal (float_plus_min (:τ # χ)) ∧
  ¬float_is_infinite (float_plus_min (:τ # χ)) ∧
  ¬float_is_zero (float_minus_min (:τ # χ)) ∧
  float_is_finite (float_minus_min (:τ # χ)) ∧
  (float_is_integral (float_minus_min (:τ # χ)) ⇔
   dimindex (:χ) = 1 ∧ dimindex (:τ) = 1) ∧
  ¬float_is_nan (float_minus_min (:τ # χ)) ∧
  ¬float_is_normal (float_minus_min (:τ # χ)) ∧
  float_is_subnormal (float_minus_min (:τ # χ)) ∧
  ¬float_is_infinite (float_minus_min (:τ # χ))
top_properties 
⊢ ¬float_is_zero (float_top (:τ # χ)) ∧ float_is_finite (float_top (:τ # χ)) ∧
  ¬float_is_nan (float_top (:τ # χ)) ∧
  (float_is_normal (float_top (:τ # χ)) ⇔ dimindex (:χ) ≠ 1) ∧
  (float_is_subnormal (float_top (:τ # χ)) ⇔ dimindex (:χ) = 1) ∧
  ¬float_is_infinite (float_top (:τ # χ))
bottom_properties 
⊢ ¬float_is_zero (float_bottom (:τ # χ)) ∧
  float_is_finite (float_bottom (:τ # χ)) ∧
  ¬float_is_nan (float_bottom (:τ # χ)) ∧
  (float_is_normal (float_bottom (:τ # χ)) ⇔ dimindex (:χ) ≠ 1) ∧
  (float_is_subnormal (float_bottom (:τ # χ)) ⇔ dimindex (:χ) = 1) ∧
  ¬float_is_infinite (float_bottom (:τ # χ))
float_is_zero 
⊢ ∀x. float_is_zero x ⇔ x.Exponent = 0w ∧ x.Significand = 0w
float_is_finite 
⊢ ∀x.
      float_is_finite x ⇔
      float_is_normal x ∨ float_is_subnormal x ∨ float_is_zero x
float_cases_finite 
⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_finite x
float_distinct_finite 
⊢ ∀x.
      ¬(float_is_nan x ∧ float_is_infinite x) ∧
      ¬(float_is_nan x ∧ float_is_finite x) ∧
      ¬(float_is_infinite x ∧ float_is_finite x)
float_cases 
⊢ ∀x.
      float_is_nan x ∨ float_is_infinite x ∨ float_is_normal x ∨
      float_is_subnormal x ∨ float_is_zero x
float_is_distinct 
⊢ ∀x.
      ¬(float_is_nan x ∧ float_is_infinite x) ∧
      ¬(float_is_nan x ∧ float_is_normal x) ∧
      ¬(float_is_nan x ∧ float_is_subnormal x) ∧
      ¬(float_is_nan x ∧ float_is_zero x) ∧
      ¬(float_is_infinite x ∧ float_is_normal x) ∧
      ¬(float_is_infinite x ∧ float_is_subnormal x) ∧
      ¬(float_is_infinite x ∧ float_is_zero x) ∧
      ¬(float_is_normal x ∧ float_is_subnormal x) ∧
      ¬(float_is_normal x ∧ float_is_zero x) ∧
      ¬(float_is_subnormal x ∧ float_is_zero x)
float_infinities 
⊢ ∀x.
      float_is_infinite x ⇔
      x = float_plus_infinity (:τ # χ) ∨ x = float_minus_infinity (:τ # χ)
float_infinities_distinct 
⊢ ∀x. ¬(x = float_plus_infinity (:τ # χ) ∧ x = float_minus_infinity (:τ # χ))
float_to_real_negate 
⊢ ∀x. float_to_real (float_negate x) = -float_to_real x
float_negate_negate 
⊢ ∀x. float_negate (float_negate x) = x
ulp 
⊢ ulp (:τ # χ) = float_to_real (float_plus_min (:τ # χ))
neg_ulp 
⊢ -ulp (:τ # χ) = float_to_real (float_negate (float_plus_min (:τ # χ)))
ULP_le_mono 
⊢ ∀e1 e2. e2 ≠ 0w ⇒ (ULP (e1,(:τ)) ≤ ULP (e2,(:τ)) ⇔ e1 ≤₊ e2)
ulp_lt_ULP 
⊢ ∀e. ulp (:τ # χ) ≤ ULP (e,(:τ))
ulp_lt_largest 
⊢ ulp (:τ # χ) < largest (:τ # χ)
ulp_lt_threshold 
⊢ ulp (:τ # χ) < threshold (:τ # χ)
abs_float_value 
⊢ (∀b c d. abs (-1 pow w2n b * c * d) = abs (c * d)) ∧
  ∀b c. abs (-1 pow w2n b * c) = abs c
less_than_ulp 
⊢ ∀a.
      abs (float_to_real a) < ulp (:τ # χ) ⇔
      a.Exponent = 0w ∧ a.Significand = 0w
float_is_zero_to_real 
⊢ ∀x. float_is_zero x ⇔ float_to_real x = 0
float_to_real_eq 
⊢ ∀x y.
      float_to_real x = float_to_real y ⇔
      x = y ∨ float_is_zero x ∧ float_is_zero y
diff_float_ULP 
⊢ ∀x y.
      float_to_real x ≠ float_to_real y ∧ ¬exponent_boundary y x ⇒
      ULP (x.Exponent,(:τ)) ≤ abs (float_to_real x − float_to_real y)
diff_lt_ulp_eq0 
⊢ ∀a b x.
      ¬exponent_boundary b a ∧
      abs (x − float_to_real a) < ULP (a.Exponent,(:τ)) ∧
      abs (x − float_to_real b) < ULP (a.Exponent,(:τ)) ∧
      abs (float_to_real a) ≤ abs x ∧ abs (float_to_real b) ≤ abs x ∧
      ¬float_is_zero a ⇒
      b = a
diff_lt_ulp_even 
⊢ ∀a b x.
      ¬exponent_boundary b a ∧
      2 * abs (float_to_real a − x) < ULP (a.Exponent,(:τ)) ∧
      2 * abs (float_to_real b − x) < ULP (a.Exponent,(:τ)) ∧ ¬float_is_zero a ⇒
      b = a
diff_lt_ulp_even4 
⊢ ∀a b x.
      ¬exponent_boundary b a ∧
      4 * abs (float_to_real a − x) ≤ ULP (a.Exponent,(:τ)) ∧
      4 * abs (float_to_real b − x) ≤ ULP (a.Exponent,(:τ)) ∧ ¬float_is_zero a ⇒
      b = a
round_roundTowardZero 
⊢ ∀y x r.
      float_value y = Float r ∧ abs (r − x) < ULP (y.Exponent,(:τ)) ∧
      abs r ≤ abs x ∧ ulp (:τ # χ) ≤ abs x ∧ abs x ≤ largest (:τ # χ) ⇒
      round roundTowardZero x = y
round_roundTiesToEven 
⊢ ∀y x r.
      float_value y = Float r ∧
      (y.Significand = 0w ∧ y.Exponent ≠ 1w ⇒ abs r ≤ abs x) ∧
      2 * abs (r − x) ≤ ULP (y.Exponent,(:τ)) ∧
      (2 * abs (r − x) = ULP (y.Exponent,(:τ)) ⇒ ¬word_lsb y.Significand) ∧
      ulp (:τ # χ) < 2 * abs x ∧ abs x < threshold (:τ # χ) ⇒
      round roundTiesToEven x = y
round_roundTiesToEven0 
⊢ ∀y x r.
      float_value y = Float r ∧
      (y.Significand = 0w ∧ y.Exponent ≠ 1w ∧ ¬(abs r ≤ abs x)) ∧
      4 * abs (r − x) ≤ ULP (y.Exponent,(:τ)) ∧ ulp (:τ # χ) < 2 * abs x ∧
      abs x < threshold (:τ # χ) ⇒
      round roundTiesToEven x = y
round_roundTowardZero_is_zero 
⊢ ∀x.
      abs x < ulp (:τ # χ) ⇒
      round roundTowardZero x = float_plus_zero (:τ # χ) ∨
      round roundTowardZero x = float_minus_zero (:τ # χ)
round_roundTiesToEven_is_zero 
⊢ ∀x.
      2 * abs x ≤ ulp (:τ # χ) ⇒
      round roundTiesToEven x = float_plus_zero (:τ # χ) ∨
      round roundTiesToEven x = float_minus_zero (:τ # χ)
round_roundTowardZero_is_minus_zero 
⊢ ∀x.
      abs x < ulp (:τ # χ) ⇒
      float_round roundTowardZero T x = float_minus_zero (:τ # χ)
round_roundTowardZero_is_plus_zero 
⊢ ∀x.
      abs x < ulp (:τ # χ) ⇒
      float_round roundTowardZero F x = float_plus_zero (:τ # χ)
round_roundTiesToEven_is_minus_zero 
⊢ ∀x.
      2 * abs x ≤ ulp (:τ # χ) ⇒
      float_round roundTiesToEven T x = float_minus_zero (:τ # χ)
round_roundTiesToEven_is_plus_zero 
⊢ ∀x.
      2 * abs x ≤ ulp (:τ # χ) ⇒
      float_round roundTiesToEven F x = float_plus_zero (:τ # χ)
largest_is_positive 
⊢ 0 ≤ largest (:τ # χ)
threshold_is_positive 
⊢ 0 < threshold (:τ # χ)
round_roundTiesToEven_plus_infinity 
⊢ ∀y x.
      threshold (:τ # χ) ≤ x ⇒
      round roundTiesToEven x = float_plus_infinity (:τ # χ)
round_roundTiesToEven_minus_infinity 
⊢ ∀y x.
      x ≤ -threshold (:τ # χ) ⇒
      round roundTiesToEven x = float_minus_infinity (:τ # χ)
round_roundTowardZero_top 
⊢ ∀y x. largest (:τ # χ) < x ⇒ round roundTowardZero x = float_top (:τ # χ)
round_roundTowardZero_bottom 
⊢ ∀y x.
      x < -largest (:τ # χ) ⇒ round roundTowardZero x = float_bottom (:τ # χ)
round_roundTowardPositive_plus_infinity 
⊢ ∀y x.
      largest (:τ # χ) < x ⇒
      round roundTowardPositive x = float_plus_infinity (:τ # χ)
round_roundTowardPositive_bottom 
⊢ ∀y x.
      x < -largest (:τ # χ) ⇒
      round roundTowardPositive x = float_bottom (:τ # χ)
round_roundTowardNegative_top 
⊢ ∀y x.
      largest (:τ # χ) < x ⇒ round roundTowardNegative x = float_top (:τ # χ)
round_roundTowardNegative_minus_infinity 
⊢ ∀y x.
      x < -largest (:τ # χ) ⇒
      round roundTowardNegative x = float_minus_infinity (:τ # χ)
float_round_roundTowardZero_top 
⊢ ∀b y x.
      largest (:τ # χ) < x ⇒
      float_round roundTowardZero b x = float_top (:τ # χ)
float_round_roundTowardZero_bottom 
⊢ ∀b y x.
      x < -largest (:τ # χ) ⇒
      float_round roundTowardZero b x = float_bottom (:τ # χ)
float_round_roundTowardPositive_plus_infinity 
⊢ ∀b y x.
      largest (:τ # χ) < x ⇒
      float_round roundTowardPositive b x = float_plus_infinity (:τ # χ)
float_round_roundTowardPositive_bottom 
⊢ ∀b y x.
      x < -largest (:τ # χ) ⇒
      float_round roundTowardPositive b x = float_bottom (:τ # χ)
float_round_roundTowardNegative_top 
⊢ ∀b y x.
      largest (:τ # χ) < x ⇒
      float_round roundTowardNegative b x = float_top (:τ # χ)
float_round_roundTowardNegative_minus_infinity 
⊢ ∀b y x.
      x < -largest (:τ # χ) ⇒
      float_round roundTowardNegative b x = float_minus_infinity (:τ # χ)
float_minus_zero 
⊢ float_minus_zero (:τ # χ) =
  <|Sign := 1w; Exponent := 0w; Significand := 0w|>
float_minus_infinity 
⊢ float_minus_infinity (:τ # χ) =
  <|Sign := 1w; Exponent := UINT_MAXw; Significand := 0w|>
float_round_non_zero 
⊢ ∀mode toneg r s e f.
      round mode r = <|Sign := s; Exponent := e; Significand := f|> ∧
      (e ≠ 0w ∨ f ≠ 0w) ⇒
      float_round mode toneg r =
      <|Sign := s; Exponent := e; Significand := f|>
float_round_plus_infinity 
⊢ ∀mode toneg r.
      round mode r = float_plus_infinity (:τ # χ) ⇒
      float_round mode toneg r = float_plus_infinity (:τ # χ)
float_round_minus_infinity 
⊢ ∀mode toneg r.
      round mode r = float_minus_infinity (:τ # χ) ⇒
      float_round mode toneg r = float_minus_infinity (:τ # χ)
float_round_top 
⊢ ∀mode toneg r.
      round mode r = float_top (:τ # χ) ⇒
      float_round mode toneg r = float_top (:τ # χ)
float_round_bottom 
⊢ ∀mode toneg r.
      round mode r = float_bottom (:τ # χ) ⇒
      float_round mode toneg r = float_bottom (:τ # χ)
float_to_real 
⊢ ∀s e f.
      float_to_real <|Sign := s; Exponent := e; Significand := f|> =
      (let
         r =
           if e = 0w then 2 / &(2 ** INT_MAX (:χ)) * (&w2n f / &dimword (:τ))
           else
             &(2 ** w2n e) / &(2 ** INT_MAX (:χ)) *
             (1 + &w2n f / &dimword (:τ))
       in
         if s = 1w then -r else r)
largest 
⊢ largest (:τ # χ) =
  &(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &dimword (:τ)) / &(2 ** INT_MAX (:χ))
threshold 
⊢ threshold (:τ # χ) =
  &(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &(2 * dimword (:τ))) /
  &(2 ** INT_MAX (:χ))
largest_is_top 
⊢ 1 < dimindex (:χ) ⇒ largest (:τ # χ) = float_to_real (float_top (:τ # χ))
largest_lt_threshold 
⊢ largest (:τ # χ) < threshold (:τ # χ)
float_tests 
⊢ (∀s e f.
       float_is_nan <|Sign := s; Exponent := e; Significand := f|> ⇔
       e = -1w ∧ f ≠ 0w) ∧
  (∀s e f.
       float_is_signalling <|Sign := s; Exponent := e; Significand := f|> ⇔
       e = -1w ∧ ¬word_msb f ∧ f ≠ 0w) ∧
  (∀s e f.
       float_is_infinite <|Sign := s; Exponent := e; Significand := f|> ⇔
       e = -1w ∧ f = 0w) ∧
  (∀s e f.
       float_is_normal <|Sign := s; Exponent := e; Significand := f|> ⇔
       e ≠ 0w ∧ e ≠ -1w) ∧
  (∀s e f.
       float_is_subnormal <|Sign := s; Exponent := e; Significand := f|> ⇔
       e = 0w ∧ f ≠ 0w) ∧
  (∀s e f.
       float_is_zero <|Sign := s; Exponent := e; Significand := f|> ⇔
       e = 0w ∧ f = 0w) ∧
  ∀s e f.
      float_is_finite <|Sign := s; Exponent := e; Significand := f|> ⇔ e ≠ -1w
float_infinity_negate_abs 
⊢ float_negate (float_plus_infinity (:τ # χ)) = float_minus_infinity (:τ # χ) ∧
  float_negate (float_minus_infinity (:τ # χ)) = float_plus_infinity (:τ # χ) ∧
  float_abs (float_plus_infinity (:τ # χ)) = float_plus_infinity (:τ # χ) ∧
  float_abs (float_minus_infinity (:τ # χ)) = float_plus_infinity (:τ # χ)
float_round_to_integral_compute 
⊢ (∀m.
       float_round_to_integral m (float_minus_infinity (:τ # χ)) =
       float_minus_infinity (:τ # χ)) ∧
  (∀m.
       float_round_to_integral m (float_plus_infinity (:τ # χ)) =
       float_plus_infinity (:τ # χ)) ∧
  ∀m fp_op.
      float_round_to_integral m (float_some_qnan fp_op) =
      float_some_qnan fp_op
float_add_compute 
⊢ (∀mode x fp_op.
       (mode float_add float_some_qnan fp_op) x =
       (check_for_signalling [x],
        float_some_qnan (FP_Add mode (float_some_qnan fp_op) x))) ∧
  (∀mode x fp_op.
       (mode float_add x) (float_some_qnan fp_op) =
       (check_for_signalling [x],
        float_some_qnan (FP_Add mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
       (mode float_add float_minus_infinity (:τ # χ))
         (float_minus_infinity (:τ # χ)) =
       (clear_flags,float_minus_infinity (:τ # χ))) ∧
  (∀mode.
       (mode float_add float_minus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (invalidop_flags,
        float_some_qnan
          (FP_Add mode (float_minus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ))))) ∧
  (∀mode.
       (mode float_add float_plus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (clear_flags,float_plus_infinity (:τ # χ))) ∧
  ∀mode.
      (mode float_add float_plus_infinity (:τ # χ))
        (float_minus_infinity (:τ # χ)) =
      (invalidop_flags,
       float_some_qnan
         (FP_Add mode (float_plus_infinity (:τ # χ))
            (float_minus_infinity (:τ # χ))))
float_add_nan 
⊢ ∀mode x y.
      float_value x = NaN ∨ float_value y = NaN ⇒
      (mode float_add x) y =
      (check_for_signalling [x; y],float_some_qnan (FP_Add mode x y))
float_add_finite 
⊢ ∀mode x y r1 r2.
      float_value x = Float r1 ∧ float_value y = Float r2 ⇒
      (mode float_add x) y =
      float_round_with_flags mode
        (if r1 = 0 ∧ r2 = 0 ∧ x.Sign = y.Sign then x.Sign = 1w
         else (mode = roundTowardNegative)) (r1 + r2)
float_add_finite_plus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_add x) (float_plus_infinity (:τ # χ)) =
      (clear_flags,float_plus_infinity (:τ # χ))
float_add_plus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_add float_plus_infinity (:τ # χ)) x =
      (clear_flags,float_plus_infinity (:τ # χ))
float_add_finite_minus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_add x) (float_minus_infinity (:τ # χ)) =
      (clear_flags,float_minus_infinity (:τ # χ))
float_add_minus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_add float_minus_infinity (:τ # χ)) x =
      (clear_flags,float_minus_infinity (:τ # χ))
float_sub_compute 
⊢ (∀mode x fp_op.
       (mode float_sub float_some_qnan fp_op) x =
       (check_for_signalling [x],
        float_some_qnan (FP_Sub mode (float_some_qnan fp_op) x))) ∧
  (∀mode x fp_op.
       (mode float_sub x) (float_some_qnan fp_op) =
       (check_for_signalling [x],
        float_some_qnan (FP_Sub mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
       (mode float_sub float_minus_infinity (:τ # χ))
         (float_minus_infinity (:τ # χ)) =
       (invalidop_flags,
        float_some_qnan
          (FP_Sub mode (float_minus_infinity (:τ # χ))
             (float_minus_infinity (:τ # χ))))) ∧
  (∀mode.
       (mode float_sub float_minus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (clear_flags,float_minus_infinity (:τ # χ))) ∧
  (∀mode.
       (mode float_sub float_plus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (invalidop_flags,
        float_some_qnan
          (FP_Sub mode (float_plus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ))))) ∧
  ∀mode.
      (mode float_sub float_plus_infinity (:τ # χ))
        (float_minus_infinity (:τ # χ)) =
      (clear_flags,float_plus_infinity (:τ # χ))
float_sub_nan 
⊢ ∀mode x y.
      float_value x = NaN ∨ float_value y = NaN ⇒
      (mode float_sub x) y =
      (check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y))
float_sub_finite 
⊢ ∀mode x y r1 r2.
      float_value x = Float r1 ∧ float_value y = Float r2 ⇒
      (mode float_sub x) y =
      float_round_with_flags mode
        (if r1 = 0 ∧ r2 = 0 ∧ x.Sign ≠ y.Sign then x.Sign = 1w
         else (mode = roundTowardNegative)) (r1 − r2)
float_sub_finite_plus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_sub x) (float_plus_infinity (:τ # χ)) =
      (clear_flags,float_minus_infinity (:τ # χ))
float_sub_plus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_sub float_plus_infinity (:τ # χ)) x =
      (clear_flags,float_plus_infinity (:τ # χ))
float_sub_finite_minus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_sub x) (float_minus_infinity (:τ # χ)) =
      (clear_flags,float_plus_infinity (:τ # χ))
float_sub_minus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_sub float_minus_infinity (:τ # χ)) x =
      (clear_flags,float_minus_infinity (:τ # χ))
float_mul_compute 
⊢ (∀mode x fp_op.
       (mode float_mul float_some_qnan fp_op) x =
       (check_for_signalling [x],
        float_some_qnan (FP_Mul mode (float_some_qnan fp_op) x))) ∧
  (∀mode x fp_op.
       (mode float_mul x) (float_some_qnan fp_op) =
       (check_for_signalling [x],
        float_some_qnan (FP_Mul mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
       (mode float_mul float_minus_infinity (:τ # χ))
         (float_minus_infinity (:τ # χ)) =
       (clear_flags,float_plus_infinity (:τ # χ))) ∧
  (∀mode.
       (mode float_mul float_minus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (clear_flags,float_minus_infinity (:τ # χ))) ∧
  (∀mode.
       (mode float_mul float_plus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (clear_flags,float_plus_infinity (:τ # χ))) ∧
  ∀mode.
      (mode float_mul float_plus_infinity (:τ # χ))
        (float_minus_infinity (:τ # χ)) =
      (clear_flags,float_minus_infinity (:τ # χ))
float_mul_nan 
⊢ ∀mode x y.
      float_value x = NaN ∨ float_value y = NaN ⇒
      (mode float_mul x) y =
      (check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y))
float_mul_finite 
⊢ ∀mode x y r1 r2.
      float_value x = Float r1 ∧ float_value y = Float r2 ⇒
      (mode float_mul x) y =
      float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 * r2)
float_mul_finite_plus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_mul x) (float_plus_infinity (:τ # χ)) =
      if r = 0 then
        (invalidop_flags,
         float_some_qnan (FP_Mul mode x (float_plus_infinity (:τ # χ))))
      else
        (clear_flags,if x.Sign = 0w then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
float_mul_plus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_mul float_plus_infinity (:τ # χ)) x =
      if r = 0 then
        (invalidop_flags,
         float_some_qnan (FP_Mul mode (float_plus_infinity (:τ # χ)) x))
      else
        (clear_flags,if x.Sign = 0w then float_plus_infinity (:τ # χ)
         else float_minus_infinity (:τ # χ))
float_mul_finite_minus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_mul x) (float_minus_infinity (:τ # χ)) =
      if r = 0 then
        (invalidop_flags,
         float_some_qnan (FP_Mul mode x (float_minus_infinity (:τ # χ))))
      else
        (clear_flags,if x.Sign = 0w then float_minus_infinity (:τ # χ)
         else float_plus_infinity (:τ # χ))
float_mul_minus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_mul float_minus_infinity (:τ # χ)) x =
      if r = 0 then
        (invalidop_flags,
         float_some_qnan (FP_Mul mode (float_minus_infinity (:τ # χ)) x))
      else
        (clear_flags,if x.Sign = 0w then float_minus_infinity (:τ # χ)
         else float_plus_infinity (:τ # χ))
float_div_compute 
⊢ (∀mode x fp_op.
       (mode float_div float_some_qnan fp_op) x =
       (check_for_signalling [x],
        float_some_qnan (FP_Div mode (float_some_qnan fp_op) x))) ∧
  (∀mode x fp_op.
       (mode float_div x) (float_some_qnan fp_op) =
       (check_for_signalling [x],
        float_some_qnan (FP_Div mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
       (mode float_div float_minus_infinity (:τ # χ))
         (float_minus_infinity (:τ # χ)) =
       (invalidop_flags,
        float_some_qnan
          (FP_Div mode (float_minus_infinity (:τ # χ))
             (float_minus_infinity (:τ # χ))))) ∧
  (∀mode.
       (mode float_div float_minus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (invalidop_flags,
        float_some_qnan
          (FP_Div mode (float_minus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ))))) ∧
  (∀mode.
       (mode float_div float_plus_infinity (:τ # χ))
         (float_plus_infinity (:τ # χ)) =
       (invalidop_flags,
        float_some_qnan
          (FP_Div mode (float_plus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ))))) ∧
  ∀mode.
      (mode float_div float_plus_infinity (:τ # χ))
        (float_minus_infinity (:τ # χ)) =
      (invalidop_flags,
       float_some_qnan
         (FP_Div mode (float_plus_infinity (:τ # χ))
            (float_minus_infinity (:τ # χ))))
float_div_nan 
⊢ ∀mode x y.
      float_value x = NaN ∨ float_value y = NaN ⇒
      (mode float_div x) y =
      (check_for_signalling [x; y],float_some_qnan (FP_Div mode x y))
float_div_finite 
⊢ ∀mode x y r1 r2.
      float_value x = Float r1 ∧ float_value y = Float r2 ⇒
      (mode float_div x) y =
      if r2 = 0 then
        if r1 = 0 then (invalidop_flags,float_some_qnan (FP_Div mode x y))
        else
          (dividezero_flags,
           if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
           else float_minus_infinity (:τ # χ))
      else float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 / r2)
float_div_finite_plus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_div x) (float_plus_infinity (:τ # χ)) =
      (clear_flags,if x.Sign = 0w then float_plus_zero (:τ # χ)
       else float_minus_zero (:τ # χ))
float_div_plus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_div float_plus_infinity (:τ # χ)) x =
      (clear_flags,if x.Sign = 0w then float_plus_infinity (:τ # χ)
       else float_minus_infinity (:τ # χ))
float_div_finite_minus_infinity 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_div x) (float_minus_infinity (:τ # χ)) =
      (clear_flags,if x.Sign = 0w then float_minus_zero (:τ # χ)
       else float_plus_zero (:τ # χ))
float_div_minus_infinity_finite 
⊢ ∀mode x r.
      float_value x = Float r ⇒
      (mode float_div float_minus_infinity (:τ # χ)) x =
      (clear_flags,if x.Sign = 0w then float_minus_infinity (:τ # χ)
       else float_plus_infinity (:τ # χ))