Theory binary_ieee

⊢ 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 (bias (:χ) + precision (:τ))))

⊢ ∀l. check_for_signalling l =
      clear_flags with InvalidOp := EXISTS float_is_signalling l

⊢ clear_flags =
  <|DivideByZero := F; InvalidOp := F; Overflow := F; Precision := F;
    Underflow_BeforeRounding := F; Underflow_AfterRounding := F|>

⊢ closest = closest_such (K T)

⊢ ∀p s x.
    closest_such p s x =
    @a. is_closest s x a ∧ ∀b. is_closest s x b ∧ p b ⇒ p a

⊢ dividezero_flags = clear_flags with DivideByZero := T

⊢ ∀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

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('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) ⇒
                $var$('flags') a0') ⇒
             $var$('flags') a0') rep

⊢ ∀a0 a1 a2 a3 a4 a5 f.
    flags_CASE (flags a0 a1 a2 a3 a4 a5) f = f a0 a1 a2 a3 a4 a5

⊢ ∀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)))))

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('float').
             (∀a0'.
                (∃a0 a1 a2.
                   a0' =
                   (λa0 a1 a2.
                        ind_type$CONSTR 0 (a0,a1,a2) (λn. ind_type$BOTTOM))
                     a0 a1 a2) ⇒
                $var$('float') a0') ⇒
             $var$('float') a0') rep

⊢ ∀x. float_abs x = x with Sign := 0w

⊢ ∀mode x y.
    float_add mode 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_bottom (:τ # χ) = float_negate FLT_MAX

⊢ ∀a0 a1 a2 f. float_CASE (float a0 a1 a2) f = f a0 a1 a2

⊢ (∀a. num2float_compare (float_compare2num a) = a) ∧
  ∀r. (λn. n < 4) r ⇔ float_compare2num (num2float_compare r) = r

⊢ ∀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)

⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep

⊢ ∀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

⊢ ∀x. float_compare_size x = 0

⊢ ∀mode x y.
    float_div mode 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 POS0 else NEG0)
    | (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))

⊢ ∀x y. float_equal x y ⇔ float_compare x y = EQ

⊢ ∀x y.
    float_greater_equal x y ⇔
    case float_compare x y of LT => F | EQ => T | GT => T | UN => F

⊢ ∀x y. float_greater_than x y ⇔ float_compare x y = GT

⊢ ∀x. float_is_finite x ⇔
      case float_value x of Float v1 => T | Infinity => F | NaN => F

⊢ ∀x. float_is_infinite x ⇔
      case float_value x of Float v1 => F | Infinity => T | NaN => F

⊢ ∀x. float_is_integral x ⇔
      case float_value x of
        Float r => is_integral r
      | Infinity => F
      | NaN => F

⊢ ∀x. float_is_nan x ⇔
      case float_value x of Float v1 => F | Infinity => F | NaN => T

⊢ ∀x. float_is_normal x ⇔ x.Exponent ≠ 0w ∧ x.Exponent ≠ UINT_MAXw

⊢ ∀x. float_is_signalling x ⇔ float_is_nan x ∧ ¬word_msb x.Significand

⊢ ∀x. float_is_subnormal x ⇔ x.Exponent = 0w ∧ x.Significand ≠ 0w

⊢ ∀x. float_is_zero x ⇔
      case float_value x of Float r => r = 0 | Infinity => F | NaN => F

⊢ ∀x y.
    float_less_equal x y ⇔
    case float_compare x y of LT => T | EQ => T | GT => F | UN => F

⊢ ∀x y. float_less_than x y ⇔ float_compare x y = LT

⊢ float_minus_infinity (:τ # χ) =
  float_negate (float_plus_infinity (:τ # χ))

⊢ float_minus_min (:τ # χ) = float_negate (float_plus_min (:τ # χ))

⊢ NEG0 = float_negate POS0

⊢ ∀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 = f2r x * f2r y;
            r2 = f2r z;
            r = r1 + r2
          in
            float_round_with_flags mode
              (r = 0 ∧
               (if r1 = 0 ∧ r2 = 0 ∧ signP = z.Sign then signP = 1w
                else mode = roundTowardNegative) ∨ r < 0) r))

⊢ ∀mode x y.
    float_mul mode 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))

⊢ ∀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 = f2r x * f2r y and r2 = f2r z
          in
            float_round_with_flags mode
              (if r1 = 0 ∧ r2 = 0 ∧ signP ≠ z.Sign then signP = 1w
               else (mode = roundTowardNegative)) (r1 − r2)))

⊢ ∀x. float_negate x = x with Sign := ¬x.Sign

⊢ float_plus_infinity (:τ # χ) =
  <|Sign := 0w; Exponent := UINT_MAXw; Significand := 0w|>

⊢ float_plus_min (:τ # χ) =
  <|Sign := 0w; Exponent := 0w; Significand := 1w|>

⊢ POS0 = <|Sign := 0w; Exponent := 0w; Significand := 0w|>

⊢ ∀mode toneg r.
    float_round mode toneg r =
    (let
       x = round mode r
     in
       if float_is_zero x then if toneg then NEG0 else POS0 else x)

⊢ ∀mode x.
    float_round_to_integral mode x =
    case float_value x of
      Float r => integral_round mode r
    | Infinity => x
    | NaN => x

⊢ ∀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 bias (:χ));
          Underflow_AfterRounding :=
            (inexact ∧
             (float_round mode to_neg r).Exponent ≤₊ n2w (INT_MIN (:χ)));
          Precision := inexact|>,x))

⊢ ∀f f1 a0 a1 a2.
    float_size f f1 (float a0 a1 a2) = 1 + (w2n a0 + (w2n a1 + w2n a2))

⊢ ∀fp_op.
    float_some_qnan fp_op =
    (@f. (let
            qnan = f fp_op
          in
            float_is_nan qnan ∧ ¬float_is_signalling qnan)) fp_op

⊢ ∀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 if x = NEG0 then (clear_flags,NEG0)
    else (invalidop_flags,float_some_qnan (FP_Sqrt mode x))

⊢ ∀mode x y.
    float_sub mode 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))

⊢ ∀mode x.
    float_to_int mode x =
    case float_value x of
      Float r =>
        SOME
          (case mode of
             roundTiesToEven =>
               (let
                  f = ⌊r⌋;
                  df = abs (r − real_of_int f)
                in
                  if df < 1 / 2 ∨ df = 1 / 2 ∧ EVEN (Num (ABS f)) then f
                  else ⌈r⌉)
           | roundTowardPositive => ⌈r⌉
           | roundTowardNegative => ⌊r⌋
           | roundTowardZero => if x.Sign = 1w then ⌈r⌉ else ⌊r⌋)
    | Infinity => NONE
    | NaN => NONE

⊢ ∀x. f2r x =
      if x.Exponent = 0w then
        sign x * (2 / 2 pow bias (:χ)) *
        (&w2n x.Significand / 2 pow precision (:τ))
      else
        sign x * (2 pow w2n x.Exponent / 2 pow bias (:χ)) *
        (1 + &w2n x.Significand / 2 pow precision (:τ))

⊢ FLT_MAX =
  <|Sign := 0w; Exponent := UINT_MAXw − 1w; Significand := UINT_MAXw|>

⊢ ∀f. ulpᶠ f = ULP (f.Exponent,(:α))

⊢ ∀x y. float_unordered x y ⇔ float_compare x y = UN

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0.
           ∀ $var$('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) ⇒
                $var$('float_value') a0) ⇒
             $var$('float_value') a0) rep

⊢ (∀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

⊢ ∀x. float_value x =
      if x.Exponent = UINT_MAXw then
        if x.Significand = 0w then Infinity else NaN
      else Float (f2r x)

⊢ (∀a. float_value_size (Float a) = 1) ∧ float_value_size Infinity = 0 ∧
  float_value_size NaN = 0

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('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) ⇒
                $var$('fp_op') a0') ⇒
             $var$('fp_op') a0') rep

⊢ (∀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

⊢ (∀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)))

⊢ ∀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 (f2r 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 ∧ f2r a ≥ x} x)
    | roundTowardNegative =>
      (let
         t = largest (:τ # χ)
       in
         if x < -t then float_minus_infinity (:τ # χ)
         else if x > t then FLT_MAX
         else closest {a | float_is_integral a ∧ f2r a ≤ x} x)
    | roundTowardZero =>
      (let
         t = largest (:τ # χ)
       in
         if x < -t then float_bottom (:τ # χ)
         else if x > t then FLT_MAX
         else closest {a | float_is_integral a ∧ abs (f2r a) ≤ abs x} x)

⊢ invalidop_flags = clear_flags with InvalidOp := T

⊢ ∀s x a.
    is_closest s x a ⇔
    a ∈ s ∧ ∀b. b ∈ s ⇒ abs (f2r a − x) ≤ abs (f2r b − x)

⊢ ∀r. is_integral r ⇔ ∃n. abs r = &n

⊢ largest (:τ # χ) =
  2 pow (UINT_MAX (:χ) − 1) / 2 pow bias (:χ) *
  (2 − (2 pow precision (:τ))⁻¹)

⊢ ∀x. next_hi x =
      if x.Significand <₊ UINT_MAXw then
        x with Significand := x.Significand + 1w
      else
        <|Sign := x.Sign; Exponent := x.Exponent + 1w; Significand := 0w|>

⊢ ∀x. next_lo x =
      if 0w <₊ x.Significand then x with Significand := x.Significand − 1w
      else
        <|Sign := x.Sign; Exponent := x.Exponent − 1w;
          Significand := UINT_MAXw|>

⊢ ∀m. real_to_float m = float_round m (m = roundTowardNegative)

⊢ ∀m. real_to_float_with_flags m =
      float_round_with_flags m (m = roundTowardNegative)

⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b

⊢ ∀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

⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0

⊢ ∀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

⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1

⊢ ∀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

⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2

⊢ ∀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

⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ 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)

⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3

⊢ ∀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

⊢ ∀c c0 c1. (float c c0 c1).Exponent = c0

⊢ ∀f c c0 c1. float c c0 c1 with Exponent updated_by f = float c (f c0) c1

⊢ ∀c c0 c1. (float c c0 c1).Sign = c

⊢ ∀f c c0 c1. float c c0 c1 with Sign updated_by f = float (f c) c0 c1

⊢ ∀c c0 c1. (float c c0 c1).Significand = c1

⊢ ∀f c c0 c1.
    float c c0 c1 with Significand updated_by f = float c c0 (f c1)

⊢ ∀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 ∧ f2r a ≥ x} x)
    | roundTowardNegative =>
      (let
         t = largest (:τ # χ)
       in
         if x < -t then float_minus_infinity (:τ # χ)
         else if x > t then FLT_MAX
         else closest {a | float_is_finite a ∧ f2r a ≤ x} x)
    | roundTowardZero =>
      (let
         t = largest (:τ # χ)
       in
         if x < -t then float_bottom (:τ # χ)
         else if x > t then FLT_MAX
         else closest {a | float_is_finite a ∧ abs (f2r a) ≤ abs x} x)

⊢ (∀a. num2rounding (rounding2num a) = a) ∧
  ∀r. (λn. n < 4) r ⇔ rounding2num (num2rounding r) = r

⊢ ∀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)

⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep

⊢ ∀x. rounding_size x = 0

⊢ threshold (:τ # χ) =
  2 pow (UINT_MAX (:χ) − 1) / 2 pow bias (:χ) *
  (2 − (2 pow SUC (precision (:τ)))⁻¹)

⊢ ulp (:τ # χ) = ULP (0w,(:τ))

⊢ ∀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|>

⊢ ∀P. (∃f. P f) ⇔
      ∃c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>

⊢ abs (f2r f1) < abs (f2r f2) ⇒ f1.Exponent ≤₊ f2.Exponent

⊢ ∀s. FINITE s

⊢ ∀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|>

⊢ ∀P. (∀f. P f) ⇔
      ∀c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>

⊢ m * n = 2 ⇔ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1

⊢ ULP (e,(:τ)) =
  2 pow (if e = 0w then 1 else w2n e) / 2 pow (bias (:χ) + precision (:τ))

⊢ ∀P. (∀e. P (e,(:τ))) ⇒ ∀v v1. P (v,v1)

⊢ ∀e1 e2. e2 ≠ 0w ⇒ (ULP (e1,(:τ)) ≤ ULP (e2,(:τ)) ⇔ e1 ≤₊ e2)

⊢ ULP (e,(:τ)) ≠ 0

⊢ 0 < ULP (e,i) ∧ 0 ≤ ULP (e,i) ∧ ¬(ULP (e,i) < 0) ∧ ¬(ULP (e,i) ≤ 0)

⊢ abs (ULP (x,y)) = ULP (x,y)

⊢ abs (f2r x) ≤ abs (f2r y) ⇒ ulpᶠ x ≤ ulpᶠ y

⊢ 2 ≤ precision (:β) ∧ float_is_finite f ⇒
  f2r (float_abs f) ≤ largest (:α # β)

⊢ abs (ulpᶠ f) = ulpᶠ f

⊢ (∀b c d. abs (-1 pow w2n b * c * d) = abs (c * d)) ∧
  ∀b c. abs (-1 pow w2n b * c) = abs c

⊢ abs (ulp (:α # β)) = ulp (:α # β)

⊢ ¬float_is_zero (float_bottom (:τ # χ)) ∧
  float_is_finite (float_bottom (:τ # χ)) ∧
  ¬float_is_nan (float_bottom (:τ # χ)) ∧
  (float_is_normal (float_bottom (:τ # χ)) ⇔ precision (:χ) ≠ 1) ∧
  (float_is_subnormal (float_bottom (:τ # χ)) ⇔ precision (:χ) = 1) ∧
  ¬float_is_infinite (float_bottom (:τ # χ))

⊢ DATATYPE
    (record flags DivideByZero InvalidOp Overflow Precision
       Underflow_BeforeRounding Underflow_AfterRounding)

⊢ DATATYPE (record float Sign Exponent Significand)

⊢ DATATYPE (float_compare LT EQ GT UN)

⊢ DATATYPE (float_value Float Infinity NaN)

⊢ DATATYPE (fp_op FP_Sqrt FP_Add FP_Sub FP_Mul FP_Div FP_MulAdd FP_MulSub)

⊢ DATATYPE
    (rounding roundTiesToEven roundTowardPositive roundTowardNegative
       roundTowardZero)

⊢ ∀x y.
    f2r x ≠ f2r y ∧ ¬exponent_boundary y x ⇒
    ULP (x.Exponent,(:τ)) ≤ abs (f2r x − f2r y)

⊢ ∀a b x.
    ¬exponent_boundary b a ∧ abs (x − f2r a) < ULP (a.Exponent,(:τ)) ∧
    abs (x − f2r b) < ULP (a.Exponent,(:τ)) ∧ abs (f2r a) ≤ abs x ∧
    abs (f2r b) ≤ abs x ∧ ¬float_is_zero a ⇒
    b = a

⊢ ∀a b x.
    ¬exponent_boundary b a ∧ 2 * abs (f2r a − x) < ULP (a.Exponent,(:τ)) ∧
    2 * abs (f2r b − x) < ULP (a.Exponent,(:τ)) ∧ ¬float_is_zero a ⇒
    b = a

⊢ ∀a b x.
    ¬exponent_boundary b a ∧ 4 * abs (f2r a − x) ≤ ULP (a.Exponent,(:τ)) ∧
    4 * abs (f2r b − x) ≤ ULP (a.Exponent,(:τ)) ∧ ¬float_is_zero a ⇒
    b = a

⊢ ∀a b. 0 < b ⇒ (a / b = 0 ⇔ a = 0)

⊢ ∀b. 2 ≤ 2 ** b ⇔ 1 ≤ b

⊢ ∀b. 2 < 2 ** b ⇔ 1 < b

⊢ ∀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')

⊢ ∀f. ∃fn. ∀a0 a1 a2 a3 a4 a5.
    fn (flags a0 a1 a2 a3 a4 a5) = f a0 a1 a2 a3 a4 a5

⊢ (∀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

⊢ (∀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

⊢ ∀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 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

⊢ ∀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)

⊢ (∀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)

⊢ (∀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|>

⊢ ((∀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

⊢ (∀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

⊢ ((∀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

⊢ ∀P. (∀b b0 b1 b2 b3 b4. P (flags b b0 b1 b2 b3 b4)) ⇒ ∀f. P f

⊢ ∀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)

⊢ ∀f. ∃b4 b3 b2 b1 b0 b.
    f =
    <|DivideByZero := b4; InvalidOp := b3; Overflow := b2; Precision := b1;
      Underflow_BeforeRounding := b0; Underflow_AfterRounding := b|>

⊢ ∀ff. ∃b b0 b1 b2 b3 b4. ff = flags b b0 b1 b2 b3 b4

⊢ ∀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|>

⊢ ∀a0 a1 a2 a0' a1' a2'.
    float a0 a1 a2 = float a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (float a0 a1 a2) = f a0 a1 a2

⊢ (float_abs f).Exponent = f.Exponent

⊢ (float_abs f).Significand = f.Significand

⊢ (∀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

⊢ (∀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

⊢ (∀mode x fp_op.
     float_add mode (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.
     float_add mode x (float_some_qnan fp_op) =
     (check_for_signalling [x],
      float_some_qnan (FP_Add mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
     float_add mode (float_minus_infinity (:τ # χ))
       (float_minus_infinity (:τ # χ)) =
     (clear_flags,float_minus_infinity (:τ # χ))) ∧
  (∀mode.
     float_add mode (float_minus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (invalidop_flags,
      float_some_qnan
        (FP_Add mode (float_minus_infinity (:τ # χ))
           (float_plus_infinity (:τ # χ))))) ∧
  (∀mode.
     float_add mode (float_plus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (clear_flags,float_plus_infinity (:τ # χ))) ∧
  ∀mode.
    float_add mode (float_plus_infinity (:τ # χ))
      (float_minus_infinity (:τ # χ)) =
    (invalidop_flags,
     float_some_qnan
       (FP_Add mode (float_plus_infinity (:τ # χ))
          (float_minus_infinity (:τ # χ))))

⊢ ∀mode x y r1 r2.
    float_value x = Float r1 ∧ float_value y = Float r2 ⇒
    float_add mode 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)

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_add mode x (float_minus_infinity (:τ # χ)) =
    (clear_flags,float_minus_infinity (:τ # χ))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_add mode x (float_plus_infinity (:τ # χ)) =
    (clear_flags,float_plus_infinity (:τ # χ))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_add mode (float_minus_infinity (:τ # χ)) x =
    (clear_flags,float_minus_infinity (:τ # χ))

⊢ ∀mode x y.
    float_value x = NaN ∨ float_value y = NaN ⇒
    float_add mode x y =
    (check_for_signalling [x; y],float_some_qnan (FP_Add mode x y))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_add mode (float_plus_infinity (:τ # χ)) x =
    (clear_flags,float_plus_infinity (:τ # χ))

⊢ 2 ≤ precision (:β) ∧ float_value a = Float r ⇒
  -largest (:α # β) ≤ r ∧ r ≤ largest (:α # β)

⊢ ∀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 x f = v ⇔ ∃c c0 c1. x = float c c0 c1 ∧ f c c0 c1 = v

⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_normal x ∨
      float_is_subnormal x ∨ float_is_zero x

⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_finite x

⊢ ∀a a'. float_compare2num a = float_compare2num a' ⇔ a = a'

⊢ ∀r. r < 4 ⇔ ∃a. r = float_compare2num a

⊢ ∀r. r < 4 ⇔ float_compare2num (num2float_compare r) = r

⊢ float_compare2num LT = 0 ∧ float_compare2num EQ = 1 ∧
  float_compare2num GT = 2 ∧ float_compare2num UN = 3

⊢ ∀x0 x1 x2 x3. ∃f. f LT = x0 ∧ f EQ = x1 ∧ f GT = x2 ∧ f UN = x3

⊢ ∀a a'. a = a' ⇔ float_compare2num a = float_compare2num a'

⊢ ∀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'

⊢ (∀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

⊢ (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

⊢ LT ≠ EQ ∧ LT ≠ GT ∧ LT ≠ UN ∧ EQ ≠ GT ∧ EQ ≠ UN ∧ GT ≠ UN

⊢ ∀P. P EQ ∧ P GT ∧ P LT ∧ P UN ⇒ ∀a. P a

⊢ ∀a. a = LT ∨ a = EQ ∨ a = GT ∨ a = UN

⊢ ∀f1 f2.
    f1 = f2 ⇔
    f1.Sign = f2.Sign ∧ f1.Exponent = f2.Exponent ∧
    f1.Significand = f2.Significand

⊢ (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 ∧ POS0.Sign = 0w ∧
  POS0.Exponent = 0w ∧ POS0.Significand = 0w ∧ NEG0.Sign = 1w ∧
  NEG0.Exponent = 0w ∧ NEG0.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 ∧ FLT_MAX.Sign = 0w ∧
  FLT_MAX.Exponent = UINT_MAXw − 1w ∧ FLT_MAX.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_plus_infinity (:τ # χ) ≠ float_minus_infinity (:τ # χ) ∧
  float_plus_infinity (:τ # χ) ≠ POS0 ∧
  float_plus_infinity (:τ # χ) ≠ NEG0 ∧
  float_plus_infinity (:τ # χ) ≠ FLT_MAX ∧
  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 (:τ # χ) ≠ POS0 ∧
  float_minus_infinity (:τ # χ) ≠ NEG0 ∧
  float_minus_infinity (:τ # χ) ≠ FLT_MAX ∧
  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) ∧
  POS0 ≠ NEG0 ∧ POS0 ≠ FLT_MAX ∧ POS0 ≠ float_bottom (:τ # χ) ∧
  POS0 ≠ float_plus_min (:τ # χ) ∧ POS0 ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. POS0 ≠ float_some_qnan fp_op) ∧ NEG0 ≠ FLT_MAX ∧
  NEG0 ≠ float_bottom (:τ # χ) ∧ NEG0 ≠ float_plus_min (:τ # χ) ∧
  NEG0 ≠ float_minus_min (:τ # χ) ∧
  (∀fp_op. NEG0 ≠ float_some_qnan fp_op) ∧
  FLT_MAX ≠ float_minus_min (:τ # χ) ∧ FLT_MAX ≠ float_bottom (:τ # χ) ∧
  (∀fp_op. FLT_MAX ≠ 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

⊢ ∀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)

⊢ (∀mode x fp_op.
     float_div mode (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.
     float_div mode x (float_some_qnan fp_op) =
     (check_for_signalling [x],
      float_some_qnan (FP_Div mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
     float_div mode (float_minus_infinity (:τ # χ))
       (float_minus_infinity (:τ # χ)) =
     (invalidop_flags,
      float_some_qnan
        (FP_Div mode (float_minus_infinity (:τ # χ))
           (float_minus_infinity (:τ # χ))))) ∧
  (∀mode.
     float_div mode (float_minus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (invalidop_flags,
      float_some_qnan
        (FP_Div mode (float_minus_infinity (:τ # χ))
           (float_plus_infinity (:τ # χ))))) ∧
  (∀mode.
     float_div mode (float_plus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (invalidop_flags,
      float_some_qnan
        (FP_Div mode (float_plus_infinity (:τ # χ))
           (float_plus_infinity (:τ # χ))))) ∧
  ∀mode.
    float_div mode (float_plus_infinity (:τ # χ))
      (float_minus_infinity (:τ # χ)) =
    (invalidop_flags,
     float_some_qnan
       (FP_Div mode (float_plus_infinity (:τ # χ))
          (float_minus_infinity (:τ # χ))))

⊢ ∀mode x y r1 r2.
    float_value x = Float r1 ∧ float_value y = Float r2 ⇒
    float_div mode 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)

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_div mode x (float_minus_infinity (:τ # χ)) =
    (clear_flags,if x.Sign = 0w then NEG0 else POS0)

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_div mode x (float_plus_infinity (:τ # χ)) =
    (clear_flags,if x.Sign = 0w then POS0 else NEG0)

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_div mode (float_minus_infinity (:τ # χ)) x =
    (clear_flags,
     if x.Sign = 0w then float_minus_infinity (:τ # χ)
     else float_plus_infinity (:τ # χ))

⊢ ∀mode x y.
    float_value x = NaN ∨ float_value y = NaN ⇒
    float_div mode x y =
    (check_for_signalling [x; y],float_some_qnan (FP_Div mode x y))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_div mode (float_plus_infinity (:τ # χ)) x =
    (clear_flags,
     if x.Sign = 0w then float_plus_infinity (:τ # χ)
     else float_minus_infinity (:τ # χ))

⊢ (∀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)

⊢ (∀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|>

⊢ ((∀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

⊢ (∀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

⊢ ((∀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

⊢ ∀P. (∀c c0 c1. P (float c c0 c1)) ⇒ ∀f. P f

⊢ ∀x. float_is_infinite x ⇔
      x = float_plus_infinity (:τ # χ) ∨ x = float_minus_infinity (:τ # χ)

⊢ ∀x. ¬(x = float_plus_infinity (:τ # χ) ∧
       x = float_minus_infinity (:τ # χ))

⊢ 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 (:τ # χ)

⊢ ∀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)

⊢ ∀x. float_is_finite x ⇔
      float_is_normal x ∨ float_is_subnormal x ∨ float_is_zero x

⊢ float_is_finite f ⇔ f.Exponent ≠ UINT_MAXw

⊢ float_is_finite (float_abs f) ⇔ float_is_finite f

⊢ float_is_finite (float_negate f) ⇔ float_is_finite f

⊢ float_is_finite f ⇒ float_value f = Float (f2r f)

⊢ 2 ≤ precision (:β) ∧ float_is_finite f ∧ abs (f2r f) < largest (:α # β) ⇒
  float_is_finite (next_hi f)

⊢ float_is_finite f ∧ ¬float_is_zero f ⇒ float_is_finite (next_lo f)

⊢ float_is_finite f ⇔ ∃r. float_value f = Float r

⊢ ∀x. float_is_nan x ⇔ ¬float_equal x x

⊢ ∀x. float_is_zero x ⇔ x.Exponent = 0w ∧ x.Significand = 0w

⊢ float_is_zero f ⇒ float_is_finite f

⊢ float_is_zero (float_negate f) ⇔ float_is_zero f

⊢ float_is_zero f ⇔ float_value f = Float 0

⊢ ∀x. float_is_zero x ⇔ float_equal POS0 x

⊢ float_is_finite a ⇒ ¬float_is_zero (next_hi a)

⊢ ∀x. float_is_zero x ⇔ f2r x = 0

⊢ ∀c11 c01 c1 c12 c02 c2.
    <|Sign := c11; Exponent := c01; Significand := c1|> =
    <|Sign := c12; Exponent := c02; Significand := c2|> ⇔
    c11 = c12 ∧ c01 = c02 ∧ c1 = c2

⊢ ∀f. ∃c1 c0 c. f = <|Sign := c1; Exponent := c0; Significand := c|>

⊢ float_minus_infinity (:τ # χ) =
  <|Sign := 1w; Exponent := UINT_MAXw; Significand := 0w|>

⊢ NEG0 = <|Sign := 1w; Exponent := 0w; Significand := 0w|>

⊢ (∀mode x fp_op.
     float_mul mode (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.
     float_mul mode x (float_some_qnan fp_op) =
     (check_for_signalling [x],
      float_some_qnan (FP_Mul mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
     float_mul mode (float_minus_infinity (:τ # χ))
       (float_minus_infinity (:τ # χ)) =
     (clear_flags,float_plus_infinity (:τ # χ))) ∧
  (∀mode.
     float_mul mode (float_minus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (clear_flags,float_minus_infinity (:τ # χ))) ∧
  (∀mode.
     float_mul mode (float_plus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (clear_flags,float_plus_infinity (:τ # χ))) ∧
  ∀mode.
    float_mul mode (float_plus_infinity (:τ # χ))
      (float_minus_infinity (:τ # χ)) =
    (clear_flags,float_minus_infinity (:τ # χ))

⊢ ∀mode x y r1 r2.
    float_value x = Float r1 ∧ float_value y = Float r2 ⇒
    float_mul mode x y =
    float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 * r2)

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_mul mode 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 (:τ # χ))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_mul mode 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 (:τ # χ))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_mul mode (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 (:τ # χ))

⊢ ∀mode x y.
    float_value x = NaN ∨ float_value y = NaN ⇒
    float_mul mode x y =
    (check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_mul mode (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 (:τ # χ))

⊢ ∀ff. ∃c c0 c1. ff = float c c0 c1

⊢ float_value (float_negate a) = Float r ⇔ float_value a = Float (-r)

⊢ float_negate f1 = float_negate f2 ⇔ f1 = f2

⊢ ∀x. float_negate (float_negate x) = x

⊢ ∀mode toneg r.
    round mode r = float_bottom (:τ # χ) ⇒
    float_round mode toneg r = float_bottom (:τ # χ)

⊢ ∀mode toneg r.
    round mode r = float_minus_infinity (:τ # χ) ⇒
    float_round mode toneg r = float_minus_infinity (:τ # χ)

⊢ ∀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|>

⊢ ∀mode toneg r.
    round mode r = float_plus_infinity (:τ # χ) ⇒
    float_round mode toneg r = float_plus_infinity (:τ # χ)

⊢ ∀b y x.
    x < -largest (:τ # χ) ⇒
    float_round roundTowardNegative b x = float_minus_infinity (:τ # χ)

⊢ ∀b y x.
    largest (:τ # χ) < x ⇒ float_round roundTowardNegative b x = FLT_MAX

⊢ ∀b y x.
    x < -largest (:τ # χ) ⇒
    float_round roundTowardPositive b x = float_bottom (:τ # χ)

⊢ ∀b y x.
    largest (:τ # χ) < x ⇒
    float_round roundTowardPositive b x = float_plus_infinity (:τ # χ)

⊢ ∀b y x.
    x < -largest (:τ # χ) ⇒
    float_round roundTowardZero b x = float_bottom (:τ # χ)

⊢ ∀b y x. largest (:τ # χ) < x ⇒ float_round roundTowardZero b x = FLT_MAX

⊢ (∀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

⊢ ∀mode toneg r.
    round mode r = FLT_MAX ⇒ float_round mode toneg r = FLT_MAX

⊢ float_is_zero = {NEG0; POS0} ∧
  float_is_infinite =
  {float_minus_infinity (:τ # χ); float_plus_infinity (:τ # χ)}

⊢ (∀mode x fp_op.
     float_sub mode (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.
     float_sub mode x (float_some_qnan fp_op) =
     (check_for_signalling [x],
      float_some_qnan (FP_Sub mode x (float_some_qnan fp_op)))) ∧
  (∀mode.
     float_sub mode (float_minus_infinity (:τ # χ))
       (float_minus_infinity (:τ # χ)) =
     (invalidop_flags,
      float_some_qnan
        (FP_Sub mode (float_minus_infinity (:τ # χ))
           (float_minus_infinity (:τ # χ))))) ∧
  (∀mode.
     float_sub mode (float_minus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (clear_flags,float_minus_infinity (:τ # χ))) ∧
  (∀mode.
     float_sub mode (float_plus_infinity (:τ # χ))
       (float_plus_infinity (:τ # χ)) =
     (invalidop_flags,
      float_some_qnan
        (FP_Sub mode (float_plus_infinity (:τ # χ))
           (float_plus_infinity (:τ # χ))))) ∧
  ∀mode.
    float_sub mode (float_plus_infinity (:τ # χ))
      (float_minus_infinity (:τ # χ)) =
    (clear_flags,float_plus_infinity (:τ # χ))

⊢ ∀mode x y r1 r2.
    float_value x = Float r1 ∧ float_value y = Float r2 ⇒
    float_sub mode 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)

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_sub mode x (float_minus_infinity (:τ # χ)) =
    (clear_flags,float_plus_infinity (:τ # χ))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_sub mode x (float_plus_infinity (:τ # χ)) =
    (clear_flags,float_minus_infinity (:τ # χ))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_sub mode (float_minus_infinity (:τ # χ)) x =
    (clear_flags,float_minus_infinity (:τ # χ))

⊢ ∀mode x y.
    float_value x = NaN ∨ float_value y = NaN ⇒
    float_sub mode x y =
    (check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y))

⊢ ∀mode x r.
    float_value x = Float r ⇒
    float_sub mode (float_plus_infinity (:τ # χ)) x =
    (clear_flags,float_plus_infinity (:τ # χ))

⊢ (∀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

⊢ ∀s e f.
    f2r <|Sign := s; Exponent := e; Significand := f|> =
    (let
       r =
         if e = 0w then 2 / &(2 ** bias (:χ)) * (&w2n f / &dimword (:τ))
         else
           &(2 ** w2n e) / &(2 ** bias (:χ)) * (1 + &w2n f / &dimword (:τ))
     in
       if s = 1w then -r else r)

⊢ f2r f = 0 ⇔ f = POS0 ∨ f = NEG0

⊢ ∀x y. f2r x = f2r y ⇔ x = y ∨ float_is_zero x ∧ float_is_zero y

⊢ f2r (float_abs f) = abs (f2r f)

⊢ ∀x. f2r (float_negate x) = -f2r x

⊢ f2r (round m 0) = 0

⊢ f2r POS0 = 0 ∧ f2r NEG0 = 0

⊢ ulpᶠ f ≠ 0

⊢ 0 < ulpᶠ f

⊢ ulpᶠ (float_abs a) = ulpᶠ a

⊢ ulpᶠ (float_negate f) = ulpᶠ f

⊢ ulpᶠ (f with Sign := s) = ulpᶠ f

⊢ ulpᶠ (f with Significand := s) = ulpᶠ f

⊢ ∀f c1 c0 c.
    f with <|Sign := c1; Exponent := c0; Significand := c|> =
    <|Sign := c1; Exponent := c0; Significand := c|>

⊢ ∀a a'. Float a = Float a' ⇔ a = a'

⊢ ∀f0 f1 f2. ∃fn.
    (∀a. fn (Float a) = f0 a) ∧ fn Infinity = f1 ∧ fn NaN = f2

⊢ ∀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 x f v v1 = v' ⇔
  (∃r. x = Float r ∧ f r = v') ∨ x = Infinity ∧ v = v' ∨ x = NaN ∧ v1 = v'

⊢ (∀a. Float a ≠ Infinity) ∧ (∀a. Float a ≠ NaN) ∧ Infinity ≠ NaN

⊢ ∀P. (∀r. P (Float r)) ∧ P Infinity ∧ P NaN ⇒ ∀f. P f

⊢ ∀ff. (∃r. ff = Float r) ∨ ff = Infinity ∨ ff = NaN

⊢ float_value (float_plus_infinity (:τ # χ)) = Infinity ∧
  float_value (float_minus_infinity (:τ # χ)) = Infinity ∧
  (∀fp_op. float_value (float_some_qnan fp_op) = NaN) ∧
  float_value POS0 = Float 0 ∧ float_value NEG0 = Float 0 ∧
  float_value (float_plus_min (:τ # χ)) =
  Float (2 / 2 pow (bias (:χ) + precision (:τ))) ∧
  float_value (float_minus_min (:τ # χ)) =
  Float (-2 / 2 pow (bias (:χ) + precision (:τ)))

⊢ (∀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'

⊢ ∀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

⊢ ∀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 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

⊢ (∀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'

⊢ ∀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

⊢ ∀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

⊢ ¬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 (:τ # χ))

⊢ ∃a. is_closest float_is_finite r a ∧
      ∀b. is_closest float_is_finite r b ∧ P b ⇒ P a

⊢ s ≠ ∅ ⇒ ∃a. is_closest s r a

⊢ is_closest float_is_finite r f ∧ Q f ⇒
  is_closest {a | float_is_finite a ∧ Q a} r f

⊢ is_closest float_is_finite 0 f ⇔ f = POS0 ∨ f = NEG0

⊢ largest (:τ # χ) =
  &(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &dimword (:τ)) / &(2 ** bias (:χ))

⊢ 0 ≤ largest (:τ # χ)

⊢ 1 < precision (:χ) ⇒ largest (:τ # χ) = f2r FLT_MAX

⊢ largest (:τ # χ) < threshold (:τ # χ)

⊢ ∀n m. 2 ≤ n ∧ 2 ≤ m ⇒ 2 ≤ n * m

⊢ ∀a. abs (f2r a) < ulp (:τ # χ) ⇔ a.Exponent = 0w ∧ a.Significand = 0w

⊢ ¬float_is_zero (float_plus_min (:τ # χ)) ∧
  float_is_finite (float_plus_min (:τ # χ)) ∧
  (float_is_integral (float_plus_min (:τ # χ)) ⇔
   precision (:χ) = 1 ∧ precision (:τ) = 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 (:τ # χ)) ⇔
   precision (:χ) = 1 ∧ precision (:τ) = 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 (:τ # χ))

⊢ -ulp (:τ # χ) = f2r (float_negate (float_plus_min (:τ # χ)))

⊢ next_hi f = next_hi g ⇔ f = g

⊢ (next_hi f).Sign = f.Sign

⊢ float_is_finite f ⇒ abs (f2r (next_hi f) − f2r f) = ulpᶠ f

⊢ abs (f2r f0) < abs (f2r f) ∧ float_is_finite f ⇒
  abs (f2r (next_hi f0)) ≤ abs (f2r f)

⊢ next_hi (float_abs f) = float_abs (next_hi f)

⊢ next_hi (float_negate f) = float_negate (next_hi f)

⊢ next_hi f ≠ f

⊢ float_is_finite f ⇒ abs (f2r f) < abs (f2r (next_hi f))

⊢ next_hi (next_lo f) = f

⊢ next_lo f = next_lo g ⇔ f = g

⊢ (next_lo f).Sign = f.Sign

⊢ ¬float_is_zero f ∧ float_is_finite f ⇒
  abs (f2r f − f2r (next_lo f)) = ulpᶠ (next_lo f)

⊢ next_lo f ≠ f

⊢ ¬float_is_zero f ⇒ abs (f2r (next_lo f)) < abs (f2r f)

⊢ next_lo (next_hi f) = f

⊢ ∀r r'.
    r < 4 ⇒ r' < 4 ⇒ (num2float_compare r = num2float_compare r' ⇔ r = r')

⊢ ∀a. ∃r. a = num2float_compare r ∧ r < 4

⊢ ∀a. num2float_compare (float_compare2num a) = a

⊢ num2float_compare 0 = LT ∧ num2float_compare 1 = EQ ∧
  num2float_compare 2 = GT ∧ num2float_compare 3 = UN

⊢ ∀r r'. r < 4 ⇒ r' < 4 ⇒ (num2rounding r = num2rounding r' ⇔ r = r')

⊢ ∀a. ∃r. a = num2rounding r ∧ r < 4

⊢ ∀a. num2rounding (rounding2num a) = a

⊢ num2rounding 0 = roundTiesToEven ∧ num2rounding 1 = roundTowardPositive ∧
  num2rounding 2 = roundTowardNegative ∧ num2rounding 3 = roundTowardZero

⊢ ∀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

⊢ ∀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

⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒ float_round roundTiesToEven T x = NEG0

⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒ float_round roundTiesToEven F x = POS0

⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
      round roundTiesToEven x = POS0 ∨ round roundTiesToEven x = NEG0

⊢ ∀y x.
    x ≤ -threshold (:τ # χ) ⇒
    round roundTiesToEven x = float_minus_infinity (:τ # χ)

⊢ ∀y x.
    threshold (:τ # χ) ≤ x ⇒
    round roundTiesToEven x = float_plus_infinity (:τ # χ)

⊢ ∀y x.
    x < -largest (:τ # χ) ⇒
    round roundTowardNegative x = float_minus_infinity (:τ # χ)

⊢ ∀y x. largest (:τ # χ) < x ⇒ round roundTowardNegative x = FLT_MAX

⊢ ∀y x.
    x < -largest (:τ # χ) ⇒
    round roundTowardPositive x = float_bottom (:τ # χ)

⊢ ∀y x.
    largest (:τ # χ) < x ⇒
    round roundTowardPositive x = float_plus_infinity (:τ # χ)

⊢ ∀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

⊢ ∀y x.
    x < -largest (:τ # χ) ⇒ round roundTowardZero x = float_bottom (:τ # χ)

⊢ ∀x. abs x < ulp (:τ # χ) ⇒ float_round roundTowardZero T x = NEG0

⊢ ∀x. abs x < ulp (:τ # χ) ⇒ float_round roundTowardZero F x = POS0

⊢ ∀x. abs x < ulp (:τ # χ) ⇒
      round roundTowardZero x = POS0 ∨ round roundTowardZero x = NEG0

⊢ ∀y x. largest (:τ # χ) < x ⇒ round roundTowardZero x = FLT_MAX

⊢ ∀a a'. rounding2num a = rounding2num a' ⇔ a = a'

⊢ ∀r. r < 4 ⇔ ∃a. r = rounding2num a

⊢ ∀r. r < 4 ⇔ rounding2num (num2rounding r) = r

⊢ rounding2num roundTiesToEven = 0 ∧ rounding2num roundTowardPositive = 1 ∧
  rounding2num roundTowardNegative = 2 ∧ rounding2num roundTowardZero = 3

⊢ ∀x0 x1 x2 x3. ∃f.
    f roundTiesToEven = x0 ∧ f roundTowardPositive = x1 ∧
    f roundTowardNegative = x2 ∧ f roundTowardZero = x3

⊢ ∀a a'. a = a' ⇔ rounding2num a = rounding2num a'

⊢ ∀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'

⊢ (∀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

⊢ (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

⊢ roundTiesToEven ≠ roundTowardPositive ∧
  roundTiesToEven ≠ roundTowardNegative ∧
  roundTiesToEven ≠ roundTowardZero ∧
  roundTowardPositive ≠ roundTowardNegative ∧
  roundTowardPositive ≠ roundTowardZero ∧
  roundTowardNegative ≠ roundTowardZero

⊢ ∀P. P roundTiesToEven ∧ P roundTowardNegative ∧ P roundTowardPositive ∧
      P roundTowardZero ⇒
      ∀a. P a

⊢ ∀a. a = roundTiesToEven ∨ a = roundTowardPositive ∨
      a = roundTowardNegative ∨ a = roundTowardZero

⊢ sign (float_abs f) = 1

⊢ ∀s. -1 pow w2n s ≠ 0

⊢ ∀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)

⊢ threshold (:τ # χ) =
  &(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &(2 * dimword (:τ))) /
  &(2 ** bias (:χ))

⊢ 0 < threshold (:τ # χ)

⊢ ¬float_is_zero FLT_MAX ∧ float_is_finite FLT_MAX ∧
  ¬float_is_nan FLT_MAX ∧ (float_is_normal FLT_MAX ⇔ precision (:χ) ≠ 1) ∧
  (float_is_subnormal FLT_MAX ⇔ precision (:χ) = 1) ∧
  ¬float_is_infinite FLT_MAX

⊢ ulp (:τ # χ) = f2r (float_plus_min (:τ # χ))

⊢ ∀e. ulp (:τ # χ) ≤ ULP (e,(:τ))

⊢ ulp (:τ # χ) < largest (:τ # χ)

⊢ ulp (:τ # χ) < threshold (:τ # χ)

⊢ ulp (:τ # χ) ≠ 0

⊢ 0 < ulp (:τ # χ) ∧ 0 ≤ ulp (:τ # χ) ∧ ¬(ulp (:τ # χ) < 0) ∧
  ¬(ulp (:τ # χ) ≤ 0)

⊢ ¬w1 = ¬w2 ⇔ w1 = w2

⊢ float_is_finite f ⇒ (0 ≤ f2r (next_hi f) ⇔ 0 ≤ f2r f ∧ f ≠ NEG0)

⊢ ∀m n. 0 ≤ &m / 2 pow n

⊢ 0 ≤ (2 pow n)⁻¹

⊢ ∀n. 0 ≤ 2 pow n

⊢ ∀n. 0 < 2 pow n

⊢ ∀n. 2 pow n ≠ 0

⊢ float_is_zero POS0 ∧ float_is_zero NEG0 ∧ float_is_finite POS0 ∧
  float_is_finite NEG0 ∧ float_is_integral POS0 ∧ float_is_integral NEG0 ∧
  ¬float_is_nan POS0 ∧ ¬float_is_nan NEG0 ∧ ¬float_is_normal POS0 ∧
  ¬float_is_normal NEG0 ∧ ¬float_is_subnormal POS0 ∧
  ¬float_is_subnormal NEG0 ∧ ¬float_is_infinite POS0 ∧
  ¬float_is_infinite NEG0

⊢ f2r POS0 = 0 ∧ f2r NEG0 = 0

⊢ float_is_finite POS0 ∧ float_is_finite NEG0