Theory "machine_ieee"

Parents binary_ieee

Signature

Constant	Type
convert	:(α word -> (β, γ) float) -> ((δ, ε) float -> ζ word) -> (rounding -> real -> flags # ζ word) -> rounding -> α word -> flags # ζ word
float_to_fp16	:half -> word16
float_to_fp32	:single -> word32
float_to_fp64	:double -> word64
fp16_abs	:word16 -> word16
fp16_add	:rounding -> word16 -> word16 -> word16
fp16_add_with_flags	:rounding -> word16 -> word16 -> flags # word16
fp16_bottom	:word16
fp16_compare	:word16 -> word16 -> float_compare
fp16_div	:rounding -> word16 -> word16 -> word16
fp16_div_with_flags	:rounding -> word16 -> word16 -> flags # word16
fp16_equal	:word16 reln
fp16_greaterEqual	:word16 reln
fp16_greaterThan	:word16 reln
fp16_isFinite	:word16 -> bool
fp16_isInfinite	:word16 -> bool
fp16_isIntegral	:word16 -> bool
fp16_isNan	:word16 -> bool
fp16_isNormal	:word16 -> bool
fp16_isSignallingNan	:word16 -> bool
fp16_isSubnormal	:word16 -> bool
fp16_isZero	:word16 -> bool
fp16_lessEqual	:word16 reln
fp16_lessThan	:word16 reln
fp16_mul	:rounding -> word16 -> word16 -> word16
fp16_mul_add	:rounding -> word16 -> word16 -> word16 -> word16
fp16_mul_add_with_flags	:rounding -> word16 -> word16 -> word16 -> flags # word16
fp16_mul_sub	:rounding -> word16 -> word16 -> word16 -> word16
fp16_mul_sub_with_flags	:rounding -> word16 -> word16 -> word16 -> flags # word16
fp16_mul_with_flags	:rounding -> word16 -> word16 -> flags # word16
fp16_negInf	:word16
fp16_negMin	:word16
fp16_negZero	:word16
fp16_negate	:word16 -> word16
fp16_posInf	:word16
fp16_posMin	:word16
fp16_posZero	:word16
fp16_roundToIntegral	:rounding -> word16 -> word16
fp16_sqrt	:rounding -> word16 -> word16
fp16_sqrt_with_flags	:rounding -> word16 -> flags # word16
fp16_sub	:rounding -> word16 -> word16 -> word16
fp16_sub_with_flags	:rounding -> word16 -> word16 -> flags # word16
fp16_to_float	:word16 -> half
fp16_to_fp32	:word16 -> word32
fp16_to_fp32_with_flags	:word16 -> flags # word32
fp16_to_fp64	:word16 -> word64
fp16_to_fp64_with_flags	:word16 -> flags # word64
fp16_to_int	:rounding -> word16 -> int option
fp16_to_real	:word16 -> float_value
fp16_top	:word16
fp32_abs	:word32 -> word32
fp32_add	:rounding -> word32 -> word32 -> word32
fp32_add_with_flags	:rounding -> word32 -> word32 -> flags # word32
fp32_bottom	:word32
fp32_compare	:word32 -> word32 -> float_compare
fp32_div	:rounding -> word32 -> word32 -> word32
fp32_div_with_flags	:rounding -> word32 -> word32 -> flags # word32
fp32_equal	:word32 reln
fp32_greaterEqual	:word32 reln
fp32_greaterThan	:word32 reln
fp32_isFinite	:word32 -> bool
fp32_isInfinite	:word32 -> bool
fp32_isIntegral	:word32 -> bool
fp32_isNan	:word32 -> bool
fp32_isNormal	:word32 -> bool
fp32_isSignallingNan	:word32 -> bool
fp32_isSubnormal	:word32 -> bool
fp32_isZero	:word32 -> bool
fp32_lessEqual	:word32 reln
fp32_lessThan	:word32 reln
fp32_mul	:rounding -> word32 -> word32 -> word32
fp32_mul_add	:rounding -> word32 -> word32 -> word32 -> word32
fp32_mul_add_with_flags	:rounding -> word32 -> word32 -> word32 -> flags # word32
fp32_mul_sub	:rounding -> word32 -> word32 -> word32 -> word32
fp32_mul_sub_with_flags	:rounding -> word32 -> word32 -> word32 -> flags # word32
fp32_mul_with_flags	:rounding -> word32 -> word32 -> flags # word32
fp32_negInf	:word32
fp32_negMin	:word32
fp32_negZero	:word32
fp32_negate	:word32 -> word32
fp32_posInf	:word32
fp32_posMin	:word32
fp32_posZero	:word32
fp32_roundToIntegral	:rounding -> word32 -> word32
fp32_sqrt	:rounding -> word32 -> word32
fp32_sqrt_with_flags	:rounding -> word32 -> flags # word32
fp32_sub	:rounding -> word32 -> word32 -> word32
fp32_sub_with_flags	:rounding -> word32 -> word32 -> flags # word32
fp32_to_float	:word32 -> single
fp32_to_fp16	:rounding -> word32 -> word16
fp32_to_fp16_with_flags	:rounding -> word32 -> flags # word16
fp32_to_fp64	:word32 -> word64
fp32_to_fp64_with_flags	:word32 -> flags # word64
fp32_to_int	:rounding -> word32 -> int option
fp32_to_real	:word32 -> float_value
fp32_top	:word32
fp64_abs	:word64 -> word64
fp64_add	:rounding -> word64 -> word64 -> word64
fp64_add_with_flags	:rounding -> word64 -> word64 -> flags # word64
fp64_bottom	:word64
fp64_compare	:word64 -> word64 -> float_compare
fp64_div	:rounding -> word64 -> word64 -> word64
fp64_div_with_flags	:rounding -> word64 -> word64 -> flags # word64
fp64_equal	:word64 reln
fp64_greaterEqual	:word64 reln
fp64_greaterThan	:word64 reln
fp64_isFinite	:word64 -> bool
fp64_isInfinite	:word64 -> bool
fp64_isIntegral	:word64 -> bool
fp64_isNan	:word64 -> bool
fp64_isNormal	:word64 -> bool
fp64_isSignallingNan	:word64 -> bool
fp64_isSubnormal	:word64 -> bool
fp64_isZero	:word64 -> bool
fp64_lessEqual	:word64 reln
fp64_lessThan	:word64 reln
fp64_mul	:rounding -> word64 -> word64 -> word64
fp64_mul_add	:rounding -> word64 -> word64 -> word64 -> word64
fp64_mul_add_with_flags	:rounding -> word64 -> word64 -> word64 -> flags # word64
fp64_mul_sub	:rounding -> word64 -> word64 -> word64 -> word64
fp64_mul_sub_with_flags	:rounding -> word64 -> word64 -> word64 -> flags # word64
fp64_mul_with_flags	:rounding -> word64 -> word64 -> flags # word64
fp64_negInf	:word64
fp64_negMin	:word64
fp64_negZero	:word64
fp64_negate	:word64 -> word64
fp64_posInf	:word64
fp64_posMin	:word64
fp64_posZero	:word64
fp64_roundToIntegral	:rounding -> word64 -> word64
fp64_sqrt	:rounding -> word64 -> word64
fp64_sqrt_with_flags	:rounding -> word64 -> flags # word64
fp64_sub	:rounding -> word64 -> word64 -> word64
fp64_sub_with_flags	:rounding -> word64 -> word64 -> flags # word64
fp64_to_float	:word64 -> double
fp64_to_fp16	:rounding -> word64 -> word16
fp64_to_fp16_with_flags	:rounding -> word64 -> flags # word16
fp64_to_fp32	:rounding -> word64 -> word32
fp64_to_fp32_with_flags	:rounding -> word64 -> flags # word32
fp64_to_int	:rounding -> word64 -> int option
fp64_to_real	:word64 -> float_value
fp64_top	:word64
int_to_fp16	:rounding -> int -> word16
int_to_fp32	:rounding -> int -> word32
int_to_fp64	:rounding -> int -> word64
real_to_fp16	:rounding -> real -> word16
real_to_fp16_with_flags	:rounding -> real -> flags # word16
real_to_fp32	:rounding -> real -> word32
real_to_fp32_with_flags	:rounding -> real -> flags # word32
real_to_fp64	:rounding -> real -> word64
real_to_fp64_with_flags	:rounding -> real -> flags # word64

Definitions

fp16_to_float_def

⊢ ∀w.
      fp16_to_float w =
      <|Sign := (15 >< 15) w; Exponent := (14 >< 10) w;
        Significand := (9 >< 0) w|>

float_to_fp16_def

⊢ ∀x. float_to_fp16 x = x.Sign @@ x.Exponent @@ x.Significand

fp16_to_real_def

⊢ fp16_to_real = float_value ∘ fp16_to_float

real_to_fp16_def

⊢ ∀mode. real_to_fp16 mode = float_to_fp16 ∘ real_to_float mode

real_to_fp16_with_flags_def

⊢ ∀mode.
      real_to_fp16_with_flags mode =
      (I ## float_to_fp16) ∘ real_to_float_with_flags mode

int_to_fp16_def

⊢ ∀mode a. int_to_fp16 mode a = real_to_fp16 mode (real_of_int a)

fp16_roundToIntegral_def

⊢ ∀mode.
      fp16_roundToIntegral mode =
      float_to_fp16 ∘ float_round_to_integral mode ∘ fp16_to_float

fp16_to_int_def

⊢ ∀mode. fp16_to_int mode = float_to_int mode ∘ fp16_to_float

fp16_sqrt_def

⊢ ∀mode.
      fp16_sqrt mode = float_to_fp16 ∘ SND ∘ float_sqrt mode ∘ fp16_to_float

fp16_sqrt_with_flags_def

⊢ ∀mode.
      fp16_sqrt_with_flags mode =
      (I ## float_to_fp16) ∘ float_sqrt mode ∘ fp16_to_float

fp16_negate_def

⊢ fp16_negate = float_to_fp16 ∘ float_negate ∘ fp16_to_float

fp16_abs_def

⊢ fp16_abs = float_to_fp16 ∘ float_abs ∘ fp16_to_float

fp16_isNan_def

⊢ fp16_isNan = float_is_nan ∘ fp16_to_float

fp16_isSignallingNan_def

⊢ fp16_isSignallingNan = float_is_signalling ∘ fp16_to_float

fp16_isIntegral_def

⊢ fp16_isIntegral = float_is_integral ∘ fp16_to_float

fp16_isZero_def

⊢ fp16_isZero = float_is_zero ∘ fp16_to_float

fp16_isNormal_def

⊢ fp16_isNormal = float_is_normal ∘ fp16_to_float

fp16_isSubnormal_def

⊢ fp16_isSubnormal = float_is_subnormal ∘ fp16_to_float

fp16_isFinite_def

⊢ fp16_isFinite = float_is_finite ∘ fp16_to_float

fp16_isInfinite_def

⊢ fp16_isInfinite = float_is_infinite ∘ fp16_to_float

fp16_posInf_def

⊢ fp16_posInf = float_to_fp16 (float_plus_infinity (:10 # 5))

fp16_negInf_def

⊢ fp16_negInf = float_to_fp16 (float_minus_infinity (:10 # 5))

fp16_posZero_def

⊢ fp16_posZero = float_to_fp16 (float_plus_zero (:10 # 5))

fp16_negZero_def

⊢ fp16_negZero = float_to_fp16 (float_minus_zero (:10 # 5))

fp16_posMin_def

⊢ fp16_posMin = float_to_fp16 (float_plus_min (:10 # 5))

fp16_negMin_def

⊢ fp16_negMin = float_to_fp16 (float_minus_min (:10 # 5))

fp16_top_def

⊢ fp16_top = float_to_fp16 (float_top (:10 # 5))

fp16_bottom_def

⊢ fp16_bottom = float_to_fp16 (float_bottom (:10 # 5))

fp16_add_def

⊢ ∀mode a b.
      fp16_add mode a b =
      float_to_fp16 (SND ((mode float_add fp16_to_float a) (fp16_to_float b)))

fp16_sub_def

⊢ ∀mode a b.
      fp16_sub mode a b =
      float_to_fp16 (SND ((mode float_sub fp16_to_float a) (fp16_to_float b)))

fp16_mul_def

⊢ ∀mode a b.
      fp16_mul mode a b =
      float_to_fp16 (SND ((mode float_mul fp16_to_float a) (fp16_to_float b)))

fp16_div_def

⊢ ∀mode a b.
      fp16_div mode a b =
      float_to_fp16 (SND ((mode float_div fp16_to_float a) (fp16_to_float b)))

fp16_add_with_flags_def

⊢ ∀mode a b.
      fp16_add_with_flags mode a b =
      (I ## float_to_fp16)
        ((mode float_add fp16_to_float a) (fp16_to_float b))

fp16_sub_with_flags_def

⊢ ∀mode a b.
      fp16_sub_with_flags mode a b =
      (I ## float_to_fp16)
        ((mode float_sub fp16_to_float a) (fp16_to_float b))

fp16_mul_with_flags_def

⊢ ∀mode a b.
      fp16_mul_with_flags mode a b =
      (I ## float_to_fp16)
        ((mode float_mul fp16_to_float a) (fp16_to_float b))

fp16_div_with_flags_def

⊢ ∀mode a b.
      fp16_div_with_flags mode a b =
      (I ## float_to_fp16)
        ((mode float_div fp16_to_float a) (fp16_to_float b))

fp16_compare_def

⊢ ∀a b. fp16_compare a b = float_compare (fp16_to_float a) (fp16_to_float b)

fp16_equal_def

⊢ ∀a b. fp16_equal a b ⇔ float_equal (fp16_to_float a) (fp16_to_float b)

fp16_lessThan_def

⊢ ∀a b.
      fp16_lessThan a b ⇔ float_less_than (fp16_to_float a) (fp16_to_float b)

fp16_lessEqual_def

⊢ ∀a b.
      fp16_lessEqual a b ⇔
      float_less_equal (fp16_to_float a) (fp16_to_float b)

fp16_greaterThan_def

⊢ ∀a b.
      fp16_greaterThan a b ⇔
      float_greater_than (fp16_to_float a) (fp16_to_float b)

fp16_greaterEqual_def

⊢ ∀a b.
      fp16_greaterEqual a b ⇔
      float_greater_equal (fp16_to_float a) (fp16_to_float b)

fp16_mul_add_def

⊢ ∀mode a b c.
      fp16_mul_add mode a b c =
      float_to_fp16
        (SND
           (float_mul_add mode (fp16_to_float a) (fp16_to_float b)
              (fp16_to_float c)))

fp16_mul_sub_def

⊢ ∀mode a b c.
      fp16_mul_sub mode a b c =
      float_to_fp16
        (SND
           (float_mul_sub mode (fp16_to_float a) (fp16_to_float b)
              (fp16_to_float c)))

fp16_mul_add_with_flags_def

⊢ ∀mode a b c.
      fp16_mul_add_with_flags mode a b c =
      (I ## float_to_fp16)
        (float_mul_add mode (fp16_to_float a) (fp16_to_float b)
           (fp16_to_float c))

fp16_mul_sub_with_flags_def

⊢ ∀mode a b c.
      fp16_mul_sub_with_flags mode a b c =
      (I ## float_to_fp16)
        (float_mul_sub mode (fp16_to_float a) (fp16_to_float b)
           (fp16_to_float c))

fp32_to_float_def

⊢ ∀w.
      fp32_to_float w =
      <|Sign := (31 >< 31) w; Exponent := (30 >< 23) w;
        Significand := (22 >< 0) w|>

float_to_fp32_def

⊢ ∀x. float_to_fp32 x = x.Sign @@ x.Exponent @@ x.Significand

fp32_to_real_def

⊢ fp32_to_real = float_value ∘ fp32_to_float

real_to_fp32_def

⊢ ∀mode. real_to_fp32 mode = float_to_fp32 ∘ real_to_float mode

real_to_fp32_with_flags_def

⊢ ∀mode.
      real_to_fp32_with_flags mode =
      (I ## float_to_fp32) ∘ real_to_float_with_flags mode

int_to_fp32_def

⊢ ∀mode a. int_to_fp32 mode a = real_to_fp32 mode (real_of_int a)

fp32_roundToIntegral_def

⊢ ∀mode.
      fp32_roundToIntegral mode =
      float_to_fp32 ∘ float_round_to_integral mode ∘ fp32_to_float

fp32_to_int_def

⊢ ∀mode. fp32_to_int mode = float_to_int mode ∘ fp32_to_float

fp32_sqrt_def

⊢ ∀mode.
      fp32_sqrt mode = float_to_fp32 ∘ SND ∘ float_sqrt mode ∘ fp32_to_float

fp32_sqrt_with_flags_def

⊢ ∀mode.
      fp32_sqrt_with_flags mode =
      (I ## float_to_fp32) ∘ float_sqrt mode ∘ fp32_to_float

fp32_negate_def

⊢ fp32_negate = float_to_fp32 ∘ float_negate ∘ fp32_to_float

fp32_abs_def

⊢ fp32_abs = float_to_fp32 ∘ float_abs ∘ fp32_to_float

fp32_isNan_def

⊢ fp32_isNan = float_is_nan ∘ fp32_to_float

fp32_isSignallingNan_def

⊢ fp32_isSignallingNan = float_is_signalling ∘ fp32_to_float

fp32_isIntegral_def

⊢ fp32_isIntegral = float_is_integral ∘ fp32_to_float

fp32_isZero_def

⊢ fp32_isZero = float_is_zero ∘ fp32_to_float

fp32_isNormal_def

⊢ fp32_isNormal = float_is_normal ∘ fp32_to_float

fp32_isSubnormal_def

⊢ fp32_isSubnormal = float_is_subnormal ∘ fp32_to_float

fp32_isFinite_def

⊢ fp32_isFinite = float_is_finite ∘ fp32_to_float

fp32_isInfinite_def

⊢ fp32_isInfinite = float_is_infinite ∘ fp32_to_float

fp32_posInf_def

⊢ fp32_posInf = float_to_fp32 (float_plus_infinity (:23 # 8))

fp32_negInf_def

⊢ fp32_negInf = float_to_fp32 (float_minus_infinity (:23 # 8))

fp32_posZero_def

⊢ fp32_posZero = float_to_fp32 (float_plus_zero (:23 # 8))

fp32_negZero_def

⊢ fp32_negZero = float_to_fp32 (float_minus_zero (:23 # 8))

fp32_posMin_def

⊢ fp32_posMin = float_to_fp32 (float_plus_min (:23 # 8))

fp32_negMin_def

⊢ fp32_negMin = float_to_fp32 (float_minus_min (:23 # 8))

fp32_top_def

⊢ fp32_top = float_to_fp32 (float_top (:23 # 8))

fp32_bottom_def

⊢ fp32_bottom = float_to_fp32 (float_bottom (:23 # 8))

fp32_add_def

⊢ ∀mode a b.
      fp32_add mode a b =
      float_to_fp32 (SND ((mode float_add fp32_to_float a) (fp32_to_float b)))

fp32_sub_def

⊢ ∀mode a b.
      fp32_sub mode a b =
      float_to_fp32 (SND ((mode float_sub fp32_to_float a) (fp32_to_float b)))

fp32_mul_def

⊢ ∀mode a b.
      fp32_mul mode a b =
      float_to_fp32 (SND ((mode float_mul fp32_to_float a) (fp32_to_float b)))

fp32_div_def

⊢ ∀mode a b.
      fp32_div mode a b =
      float_to_fp32 (SND ((mode float_div fp32_to_float a) (fp32_to_float b)))

fp32_add_with_flags_def

⊢ ∀mode a b.
      fp32_add_with_flags mode a b =
      (I ## float_to_fp32)
        ((mode float_add fp32_to_float a) (fp32_to_float b))

fp32_sub_with_flags_def

⊢ ∀mode a b.
      fp32_sub_with_flags mode a b =
      (I ## float_to_fp32)
        ((mode float_sub fp32_to_float a) (fp32_to_float b))

fp32_mul_with_flags_def

⊢ ∀mode a b.
      fp32_mul_with_flags mode a b =
      (I ## float_to_fp32)
        ((mode float_mul fp32_to_float a) (fp32_to_float b))

fp32_div_with_flags_def

⊢ ∀mode a b.
      fp32_div_with_flags mode a b =
      (I ## float_to_fp32)
        ((mode float_div fp32_to_float a) (fp32_to_float b))

fp32_compare_def

⊢ ∀a b. fp32_compare a b = float_compare (fp32_to_float a) (fp32_to_float b)

fp32_equal_def

⊢ ∀a b. fp32_equal a b ⇔ float_equal (fp32_to_float a) (fp32_to_float b)

fp32_lessThan_def

⊢ ∀a b.
      fp32_lessThan a b ⇔ float_less_than (fp32_to_float a) (fp32_to_float b)

fp32_lessEqual_def

⊢ ∀a b.
      fp32_lessEqual a b ⇔
      float_less_equal (fp32_to_float a) (fp32_to_float b)

fp32_greaterThan_def

⊢ ∀a b.
      fp32_greaterThan a b ⇔
      float_greater_than (fp32_to_float a) (fp32_to_float b)

fp32_greaterEqual_def

⊢ ∀a b.
      fp32_greaterEqual a b ⇔
      float_greater_equal (fp32_to_float a) (fp32_to_float b)

fp32_mul_add_def

⊢ ∀mode a b c.
      fp32_mul_add mode a b c =
      float_to_fp32
        (SND
           (float_mul_add mode (fp32_to_float a) (fp32_to_float b)
              (fp32_to_float c)))

fp32_mul_sub_def

⊢ ∀mode a b c.
      fp32_mul_sub mode a b c =
      float_to_fp32
        (SND
           (float_mul_sub mode (fp32_to_float a) (fp32_to_float b)
              (fp32_to_float c)))

fp32_mul_add_with_flags_def

⊢ ∀mode a b c.
      fp32_mul_add_with_flags mode a b c =
      (I ## float_to_fp32)
        (float_mul_add mode (fp32_to_float a) (fp32_to_float b)
           (fp32_to_float c))

fp32_mul_sub_with_flags_def

⊢ ∀mode a b c.
      fp32_mul_sub_with_flags mode a b c =
      (I ## float_to_fp32)
        (float_mul_sub mode (fp32_to_float a) (fp32_to_float b)
           (fp32_to_float c))

fp64_to_float_def

⊢ ∀w.
      fp64_to_float w =
      <|Sign := (63 >< 63) w; Exponent := (62 >< 52) w;
        Significand := (51 >< 0) w|>

float_to_fp64_def

⊢ ∀x. float_to_fp64 x = x.Sign @@ x.Exponent @@ x.Significand

fp64_to_real_def

⊢ fp64_to_real = float_value ∘ fp64_to_float

real_to_fp64_def

⊢ ∀mode. real_to_fp64 mode = float_to_fp64 ∘ real_to_float mode

real_to_fp64_with_flags_def

⊢ ∀mode.
      real_to_fp64_with_flags mode =
      (I ## float_to_fp64) ∘ real_to_float_with_flags mode

int_to_fp64_def

⊢ ∀mode a. int_to_fp64 mode a = real_to_fp64 mode (real_of_int a)

fp64_roundToIntegral_def

⊢ ∀mode.
      fp64_roundToIntegral mode =
      float_to_fp64 ∘ float_round_to_integral mode ∘ fp64_to_float

fp64_to_int_def

⊢ ∀mode. fp64_to_int mode = float_to_int mode ∘ fp64_to_float

fp64_sqrt_def

⊢ ∀mode.
      fp64_sqrt mode = float_to_fp64 ∘ SND ∘ float_sqrt mode ∘ fp64_to_float

fp64_sqrt_with_flags_def

⊢ ∀mode.
      fp64_sqrt_with_flags mode =
      (I ## float_to_fp64) ∘ float_sqrt mode ∘ fp64_to_float

fp64_negate_def

⊢ fp64_negate = float_to_fp64 ∘ float_negate ∘ fp64_to_float

fp64_abs_def

⊢ fp64_abs = float_to_fp64 ∘ float_abs ∘ fp64_to_float

fp64_isNan_def

⊢ fp64_isNan = float_is_nan ∘ fp64_to_float

fp64_isSignallingNan_def

⊢ fp64_isSignallingNan = float_is_signalling ∘ fp64_to_float

fp64_isIntegral_def

⊢ fp64_isIntegral = float_is_integral ∘ fp64_to_float

fp64_isZero_def

⊢ fp64_isZero = float_is_zero ∘ fp64_to_float

fp64_isNormal_def

⊢ fp64_isNormal = float_is_normal ∘ fp64_to_float

fp64_isSubnormal_def

⊢ fp64_isSubnormal = float_is_subnormal ∘ fp64_to_float

fp64_isFinite_def

⊢ fp64_isFinite = float_is_finite ∘ fp64_to_float

fp64_isInfinite_def

⊢ fp64_isInfinite = float_is_infinite ∘ fp64_to_float

fp64_posInf_def

⊢ fp64_posInf = float_to_fp64 (float_plus_infinity (:52 # 11))

fp64_negInf_def

⊢ fp64_negInf = float_to_fp64 (float_minus_infinity (:52 # 11))

fp64_posZero_def

⊢ fp64_posZero = float_to_fp64 (float_plus_zero (:52 # 11))

fp64_negZero_def

⊢ fp64_negZero = float_to_fp64 (float_minus_zero (:52 # 11))

fp64_posMin_def

⊢ fp64_posMin = float_to_fp64 (float_plus_min (:52 # 11))

fp64_negMin_def

⊢ fp64_negMin = float_to_fp64 (float_minus_min (:52 # 11))

fp64_top_def

⊢ fp64_top = float_to_fp64 (float_top (:52 # 11))

fp64_bottom_def

⊢ fp64_bottom = float_to_fp64 (float_bottom (:52 # 11))

fp64_add_def

⊢ ∀mode a b.
      fp64_add mode a b =
      float_to_fp64 (SND ((mode float_add fp64_to_float a) (fp64_to_float b)))

fp64_sub_def

⊢ ∀mode a b.
      fp64_sub mode a b =
      float_to_fp64 (SND ((mode float_sub fp64_to_float a) (fp64_to_float b)))

fp64_mul_def

⊢ ∀mode a b.
      fp64_mul mode a b =
      float_to_fp64 (SND ((mode float_mul fp64_to_float a) (fp64_to_float b)))

fp64_div_def

⊢ ∀mode a b.
      fp64_div mode a b =
      float_to_fp64 (SND ((mode float_div fp64_to_float a) (fp64_to_float b)))

fp64_add_with_flags_def

⊢ ∀mode a b.
      fp64_add_with_flags mode a b =
      (I ## float_to_fp64)
        ((mode float_add fp64_to_float a) (fp64_to_float b))

fp64_sub_with_flags_def

⊢ ∀mode a b.
      fp64_sub_with_flags mode a b =
      (I ## float_to_fp64)
        ((mode float_sub fp64_to_float a) (fp64_to_float b))

fp64_mul_with_flags_def

⊢ ∀mode a b.
      fp64_mul_with_flags mode a b =
      (I ## float_to_fp64)
        ((mode float_mul fp64_to_float a) (fp64_to_float b))

fp64_div_with_flags_def

⊢ ∀mode a b.
      fp64_div_with_flags mode a b =
      (I ## float_to_fp64)
        ((mode float_div fp64_to_float a) (fp64_to_float b))

fp64_compare_def

⊢ ∀a b. fp64_compare a b = float_compare (fp64_to_float a) (fp64_to_float b)

fp64_equal_def

⊢ ∀a b. fp64_equal a b ⇔ float_equal (fp64_to_float a) (fp64_to_float b)

fp64_lessThan_def

⊢ ∀a b.
      fp64_lessThan a b ⇔ float_less_than (fp64_to_float a) (fp64_to_float b)

fp64_lessEqual_def

⊢ ∀a b.
      fp64_lessEqual a b ⇔
      float_less_equal (fp64_to_float a) (fp64_to_float b)

fp64_greaterThan_def

⊢ ∀a b.
      fp64_greaterThan a b ⇔
      float_greater_than (fp64_to_float a) (fp64_to_float b)

fp64_greaterEqual_def

⊢ ∀a b.
      fp64_greaterEqual a b ⇔
      float_greater_equal (fp64_to_float a) (fp64_to_float b)

fp64_mul_add_def

⊢ ∀mode a b c.
      fp64_mul_add mode a b c =
      float_to_fp64
        (SND
           (float_mul_add mode (fp64_to_float a) (fp64_to_float b)
              (fp64_to_float c)))

fp64_mul_sub_def

⊢ ∀mode a b c.
      fp64_mul_sub mode a b c =
      float_to_fp64
        (SND
           (float_mul_sub mode (fp64_to_float a) (fp64_to_float b)
              (fp64_to_float c)))

fp64_mul_add_with_flags_def

⊢ ∀mode a b c.
      fp64_mul_add_with_flags mode a b c =
      (I ## float_to_fp64)
        (float_mul_add mode (fp64_to_float a) (fp64_to_float b)
           (fp64_to_float c))

fp64_mul_sub_with_flags_def

⊢ ∀mode a b c.
      fp64_mul_sub_with_flags mode a b c =
      (I ## float_to_fp64)
        (float_mul_sub mode (fp64_to_float a) (fp64_to_float b)
           (fp64_to_float c))

convert_def

⊢ ∀to_float from_float from_real_with_flags m w.
      convert to_float from_float from_real_with_flags m w =
      (let
         f = to_float w
       in
         case float_value f of
           Float r => from_real_with_flags m r
         | Infinity =>
           (clear_flags,
            from_float
              (if f.Sign = 0w then float_plus_infinity (:δ # ε)
               else float_minus_infinity (:δ # ε)))
         | NaN => (check_for_signalling [f],from_float (@fp. float_is_nan fp)))

fp16_to_fp32_with_flags_def

⊢ fp16_to_fp32_with_flags =
  convert fp16_to_float float_to_fp32 real_to_fp32_with_flags roundTiesToEven

fp16_to_fp64_with_flags_def

⊢ fp16_to_fp64_with_flags =
  convert fp16_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven

fp32_to_fp64_with_flags_def

⊢ fp32_to_fp64_with_flags =
  convert fp32_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven

fp64_to_fp32_with_flags_def

⊢ fp64_to_fp32_with_flags =
  convert fp64_to_float float_to_fp32 real_to_fp32_with_flags

fp64_to_fp16_with_flags_def

⊢ fp64_to_fp16_with_flags =
  convert fp64_to_float float_to_fp16 real_to_fp16_with_flags

fp32_to_fp16_with_flags_def

⊢ fp32_to_fp16_with_flags =
  convert fp32_to_float float_to_fp16 real_to_fp16_with_flags

fp16_to_fp32_def

⊢ fp16_to_fp32 = SND ∘ fp16_to_fp32_with_flags

fp16_to_fp64_def

⊢ fp16_to_fp64 = SND ∘ fp16_to_fp64_with_flags

fp32_to_fp64_def

⊢ fp32_to_fp64 = SND ∘ fp32_to_fp64_with_flags

fp64_to_fp32_def

⊢ ∀m. fp64_to_fp32 m = SND ∘ fp64_to_fp32_with_flags m

fp64_to_fp16_def

⊢ ∀m. fp64_to_fp16 m = SND ∘ fp64_to_fp16_with_flags m

fp32_to_fp16_def

⊢ ∀m. fp32_to_fp16 m = SND ∘ fp32_to_fp16_with_flags m

Theorems

fp16_to_float_11

⊢ ∀x y. fp16_to_float x = fp16_to_float y ⇔ x = y

float_to_fp16_11

⊢ ∀x y. float_to_fp16 x = float_to_fp16 y ⇔ x = y

float_to_fp16_fp16_to_float

⊢ ∀x. float_to_fp16 (fp16_to_float x) = x

fp16_to_float_float_to_fp16

⊢ ∀x. fp16_to_float (float_to_fp16 x) = x

fp16_nchotomy

⊢ ∀x. ∃y. x = float_to_fp16 y

float_fp16_nchotomy

⊢ ∀x. ∃y. x = fp16_to_float y

fp16_to_float_n2w

⊢ ∀n.
      fp16_to_float (n2w n) =
      (let
         (q,f) = DIVMOD_2EXP 10 n ;
         (s,e) = DIVMOD_2EXP 5 q
       in
         <|Sign := n2w (s MOD 2); Exponent := n2w e; Significand := n2w f|>)

fp16_sqrt

⊢ (∀mode a.
       fp16_sqrt mode (float_to_fp16 a) =
       float_to_fp16 (SND (float_sqrt mode a))) ∧
  ∀mode a.
      fp16_sqrt mode (n2w a) =
      float_to_fp16 (SND (float_sqrt mode (fp16_to_float (n2w a))))

fp16_add

⊢ (∀mode b a.
       fp16_add mode (float_to_fp16 a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_add a) b))) ∧
  (∀mode b a.
       fp16_add mode (float_to_fp16 a) (n2w b) =
       float_to_fp16 (SND ((mode float_add a) (fp16_to_float (n2w b))))) ∧
  (∀mode b a.
       fp16_add mode (n2w a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_add fp16_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp16_add mode (n2w a) (n2w b) =
      float_to_fp16
        (SND ((mode float_add fp16_to_float (n2w a)) (fp16_to_float (n2w b))))

fp16_sub

⊢ (∀mode b a.
       fp16_sub mode (float_to_fp16 a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_sub a) b))) ∧
  (∀mode b a.
       fp16_sub mode (float_to_fp16 a) (n2w b) =
       float_to_fp16 (SND ((mode float_sub a) (fp16_to_float (n2w b))))) ∧
  (∀mode b a.
       fp16_sub mode (n2w a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_sub fp16_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp16_sub mode (n2w a) (n2w b) =
      float_to_fp16
        (SND ((mode float_sub fp16_to_float (n2w a)) (fp16_to_float (n2w b))))

fp16_mul

⊢ (∀mode b a.
       fp16_mul mode (float_to_fp16 a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_mul a) b))) ∧
  (∀mode b a.
       fp16_mul mode (float_to_fp16 a) (n2w b) =
       float_to_fp16 (SND ((mode float_mul a) (fp16_to_float (n2w b))))) ∧
  (∀mode b a.
       fp16_mul mode (n2w a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_mul fp16_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp16_mul mode (n2w a) (n2w b) =
      float_to_fp16
        (SND ((mode float_mul fp16_to_float (n2w a)) (fp16_to_float (n2w b))))

fp16_div

⊢ (∀mode b a.
       fp16_div mode (float_to_fp16 a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_div a) b))) ∧
  (∀mode b a.
       fp16_div mode (float_to_fp16 a) (n2w b) =
       float_to_fp16 (SND ((mode float_div a) (fp16_to_float (n2w b))))) ∧
  (∀mode b a.
       fp16_div mode (n2w a) (float_to_fp16 b) =
       float_to_fp16 (SND ((mode float_div fp16_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp16_div mode (n2w a) (n2w b) =
      float_to_fp16
        (SND ((mode float_div fp16_to_float (n2w a)) (fp16_to_float (n2w b))))

fp16_compare

⊢ (∀b a. fp16_compare (float_to_fp16 a) (float_to_fp16 b) = float_compare a b) ∧
  (∀b a.
       fp16_compare (float_to_fp16 a) (n2w b) =
       float_compare a (fp16_to_float (n2w b))) ∧
  (∀b a.
       fp16_compare (n2w a) (float_to_fp16 b) =
       float_compare (fp16_to_float (n2w a)) b) ∧
  ∀b a.
      fp16_compare (n2w a) (n2w b) =
      float_compare (fp16_to_float (n2w a)) (fp16_to_float (n2w b))

fp16_equal

⊢ (∀b a. fp16_equal (float_to_fp16 a) (float_to_fp16 b) ⇔ float_equal a b) ∧
  (∀b a.
       fp16_equal (float_to_fp16 a) (n2w b) ⇔
       float_equal a (fp16_to_float (n2w b))) ∧
  (∀b a.
       fp16_equal (n2w a) (float_to_fp16 b) ⇔
       float_equal (fp16_to_float (n2w a)) b) ∧
  ∀b a.
      fp16_equal (n2w a) (n2w b) ⇔
      float_equal (fp16_to_float (n2w a)) (fp16_to_float (n2w b))

fp16_lessThan

⊢ (∀b a.
       fp16_lessThan (float_to_fp16 a) (float_to_fp16 b) ⇔ float_less_than a b) ∧
  (∀b a.
       fp16_lessThan (float_to_fp16 a) (n2w b) ⇔
       float_less_than a (fp16_to_float (n2w b))) ∧
  (∀b a.
       fp16_lessThan (n2w a) (float_to_fp16 b) ⇔
       float_less_than (fp16_to_float (n2w a)) b) ∧
  ∀b a.
      fp16_lessThan (n2w a) (n2w b) ⇔
      float_less_than (fp16_to_float (n2w a)) (fp16_to_float (n2w b))

fp16_lessEqual

⊢ (∀b a.
       fp16_lessEqual (float_to_fp16 a) (float_to_fp16 b) ⇔
       float_less_equal a b) ∧
  (∀b a.
       fp16_lessEqual (float_to_fp16 a) (n2w b) ⇔
       float_less_equal a (fp16_to_float (n2w b))) ∧
  (∀b a.
       fp16_lessEqual (n2w a) (float_to_fp16 b) ⇔
       float_less_equal (fp16_to_float (n2w a)) b) ∧
  ∀b a.
      fp16_lessEqual (n2w a) (n2w b) ⇔
      float_less_equal (fp16_to_float (n2w a)) (fp16_to_float (n2w b))

fp16_greaterThan

⊢ (∀b a.
       fp16_greaterThan (float_to_fp16 a) (float_to_fp16 b) ⇔
       float_greater_than a b) ∧
  (∀b a.
       fp16_greaterThan (float_to_fp16 a) (n2w b) ⇔
       float_greater_than a (fp16_to_float (n2w b))) ∧
  (∀b a.
       fp16_greaterThan (n2w a) (float_to_fp16 b) ⇔
       float_greater_than (fp16_to_float (n2w a)) b) ∧
  ∀b a.
      fp16_greaterThan (n2w a) (n2w b) ⇔
      float_greater_than (fp16_to_float (n2w a)) (fp16_to_float (n2w b))

fp16_greaterEqual

⊢ (∀b a.
       fp16_greaterEqual (float_to_fp16 a) (float_to_fp16 b) ⇔
       float_greater_equal a b) ∧
  (∀b a.
       fp16_greaterEqual (float_to_fp16 a) (n2w b) ⇔
       float_greater_equal a (fp16_to_float (n2w b))) ∧
  (∀b a.
       fp16_greaterEqual (n2w a) (float_to_fp16 b) ⇔
       float_greater_equal (fp16_to_float (n2w a)) b) ∧
  ∀b a.
      fp16_greaterEqual (n2w a) (n2w b) ⇔
      float_greater_equal (fp16_to_float (n2w a)) (fp16_to_float (n2w b))

fp16_to_real

⊢ (∀a. fp16_to_real (float_to_fp16 a) = float_value a) ∧
  ∀a. fp16_to_real (n2w a) = float_value (fp16_to_float (n2w a))

fp16_to_int

⊢ (∀mode a. fp16_to_int mode (float_to_fp16 a) = float_to_int mode a) ∧
  ∀mode a.
      fp16_to_int mode (n2w a) = float_to_int mode (fp16_to_float (n2w a))

fp16_abs

⊢ (∀a. fp16_abs (float_to_fp16 a) = float_to_fp16 (float_abs a)) ∧
  ∀a. fp16_abs (n2w a) = float_to_fp16 (float_abs (fp16_to_float (n2w a)))

fp16_negate

⊢ (∀a. fp16_negate (float_to_fp16 a) = float_to_fp16 (float_negate a)) ∧
  ∀a.
      fp16_negate (n2w a) =
      float_to_fp16 (float_negate (fp16_to_float (n2w a)))

fp16_isNan

⊢ (∀a. fp16_isNan (float_to_fp16 a) ⇔ float_is_nan a) ∧
  ∀a. fp16_isNan (n2w a) ⇔ float_is_nan (fp16_to_float (n2w a))

fp16_isSignallingNan

⊢ (∀a. fp16_isSignallingNan (float_to_fp16 a) ⇔ float_is_signalling a) ∧
  ∀a.
      fp16_isSignallingNan (n2w a) ⇔
      float_is_signalling (fp16_to_float (n2w a))

fp16_isIntegral

⊢ (∀a. fp16_isIntegral (float_to_fp16 a) ⇔ float_is_integral a) ∧
  ∀a. fp16_isIntegral (n2w a) ⇔ float_is_integral (fp16_to_float (n2w a))

fp16_isZero

⊢ (∀a. fp16_isZero (float_to_fp16 a) ⇔ float_is_zero a) ∧
  ∀a. fp16_isZero (n2w a) ⇔ float_is_zero (fp16_to_float (n2w a))

fp16_isNormal

⊢ (∀a. fp16_isNormal (float_to_fp16 a) ⇔ float_is_normal a) ∧
  ∀a. fp16_isNormal (n2w a) ⇔ float_is_normal (fp16_to_float (n2w a))

fp16_isSubnormal

⊢ (∀a. fp16_isSubnormal (float_to_fp16 a) ⇔ float_is_subnormal a) ∧
  ∀a. fp16_isSubnormal (n2w a) ⇔ float_is_subnormal (fp16_to_float (n2w a))

fp16_isFinite

⊢ (∀a. fp16_isFinite (float_to_fp16 a) ⇔ float_is_finite a) ∧
  ∀a. fp16_isFinite (n2w a) ⇔ float_is_finite (fp16_to_float (n2w a))

fp16_isInfinite

⊢ (∀a. fp16_isInfinite (float_to_fp16 a) ⇔ float_is_infinite a) ∧
  ∀a. fp16_isInfinite (n2w a) ⇔ float_is_infinite (fp16_to_float (n2w a))

fp16_roundToIntegral

⊢ (∀mode a.
       fp16_roundToIntegral mode (float_to_fp16 a) =
       float_to_fp16 (float_round_to_integral mode a)) ∧
  ∀mode a.
      fp16_roundToIntegral mode (n2w a) =
      float_to_fp16 (float_round_to_integral mode (fp16_to_float (n2w a)))

fp16_sqrt_with_flags

⊢ (∀mode a.
       fp16_sqrt_with_flags mode (float_to_fp16 a) =
       (I ## float_to_fp16) (float_sqrt mode a)) ∧
  ∀mode a.
      fp16_sqrt_with_flags mode (n2w a) =
      (I ## float_to_fp16) (float_sqrt mode (fp16_to_float (n2w a)))

fp16_add_with_flags

⊢ (∀mode b a.
       fp16_add_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_add a) b)) ∧
  (∀mode b a.
       fp16_add_with_flags mode (float_to_fp16 a) (n2w b) =
       (I ## float_to_fp16) ((mode float_add a) (fp16_to_float (n2w b)))) ∧
  (∀mode b a.
       fp16_add_with_flags mode (n2w a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_add fp16_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp16_add_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp16)
        ((mode float_add fp16_to_float (n2w a)) (fp16_to_float (n2w b)))

fp16_sub_with_flags

⊢ (∀mode b a.
       fp16_sub_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_sub a) b)) ∧
  (∀mode b a.
       fp16_sub_with_flags mode (float_to_fp16 a) (n2w b) =
       (I ## float_to_fp16) ((mode float_sub a) (fp16_to_float (n2w b)))) ∧
  (∀mode b a.
       fp16_sub_with_flags mode (n2w a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_sub fp16_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp16_sub_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp16)
        ((mode float_sub fp16_to_float (n2w a)) (fp16_to_float (n2w b)))

fp16_mul_with_flags

⊢ (∀mode b a.
       fp16_mul_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_mul a) b)) ∧
  (∀mode b a.
       fp16_mul_with_flags mode (float_to_fp16 a) (n2w b) =
       (I ## float_to_fp16) ((mode float_mul a) (fp16_to_float (n2w b)))) ∧
  (∀mode b a.
       fp16_mul_with_flags mode (n2w a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_mul fp16_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp16_mul_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp16)
        ((mode float_mul fp16_to_float (n2w a)) (fp16_to_float (n2w b)))

fp16_div_with_flags

⊢ (∀mode b a.
       fp16_div_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_div a) b)) ∧
  (∀mode b a.
       fp16_div_with_flags mode (float_to_fp16 a) (n2w b) =
       (I ## float_to_fp16) ((mode float_div a) (fp16_to_float (n2w b)))) ∧
  (∀mode b a.
       fp16_div_with_flags mode (n2w a) (float_to_fp16 b) =
       (I ## float_to_fp16) ((mode float_div fp16_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp16_div_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp16)
        ((mode float_div fp16_to_float (n2w a)) (fp16_to_float (n2w b)))

fp16_mul_add

⊢ (∀mode c b a.
       fp16_mul_add mode (float_to_fp16 a) (float_to_fp16 b) (float_to_fp16 c) =
       float_to_fp16 (SND (float_mul_add mode a b c))) ∧
  (∀mode c b a.
       fp16_mul_add mode (float_to_fp16 a) (float_to_fp16 b) (n2w c) =
       float_to_fp16 (SND (float_mul_add mode a b (fp16_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp16_mul_add mode (float_to_fp16 a) (n2w b) (float_to_fp16 c) =
       float_to_fp16 (SND (float_mul_add mode a (fp16_to_float (n2w b)) c))) ∧
  (∀mode c b a.
       fp16_mul_add mode (float_to_fp16 a) (n2w b) (n2w c) =
       float_to_fp16
         (SND
            (float_mul_add mode a (fp16_to_float (n2w b))
               (fp16_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp16_mul_add mode (n2w a) (float_to_fp16 b) (float_to_fp16 c) =
       float_to_fp16 (SND (float_mul_add mode (fp16_to_float (n2w a)) b c))) ∧
  (∀mode c b a.
       fp16_mul_add mode (n2w a) (float_to_fp16 b) (n2w c) =
       float_to_fp16
         (SND
            (float_mul_add mode (fp16_to_float (n2w a)) b
               (fp16_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp16_mul_add mode (n2w a) (n2w b) (float_to_fp16 c) =
       float_to_fp16
         (SND
            (float_mul_add mode (fp16_to_float (n2w a))
               (fp16_to_float (n2w b)) c))) ∧
  ∀mode c b a.
      fp16_mul_add mode (n2w a) (n2w b) (n2w c) =
      float_to_fp16
        (SND
           (float_mul_add mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b))
              (fp16_to_float (n2w c))))

fp16_mul_sub

⊢ (∀mode c b a.
       fp16_mul_sub mode (float_to_fp16 a) (float_to_fp16 b) (float_to_fp16 c) =
       float_to_fp16 (SND (float_mul_sub mode a b c))) ∧
  (∀mode c b a.
       fp16_mul_sub mode (float_to_fp16 a) (float_to_fp16 b) (n2w c) =
       float_to_fp16 (SND (float_mul_sub mode a b (fp16_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp16_mul_sub mode (float_to_fp16 a) (n2w b) (float_to_fp16 c) =
       float_to_fp16 (SND (float_mul_sub mode a (fp16_to_float (n2w b)) c))) ∧
  (∀mode c b a.
       fp16_mul_sub mode (float_to_fp16 a) (n2w b) (n2w c) =
       float_to_fp16
         (SND
            (float_mul_sub mode a (fp16_to_float (n2w b))
               (fp16_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp16_mul_sub mode (n2w a) (float_to_fp16 b) (float_to_fp16 c) =
       float_to_fp16 (SND (float_mul_sub mode (fp16_to_float (n2w a)) b c))) ∧
  (∀mode c b a.
       fp16_mul_sub mode (n2w a) (float_to_fp16 b) (n2w c) =
       float_to_fp16
         (SND
            (float_mul_sub mode (fp16_to_float (n2w a)) b
               (fp16_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp16_mul_sub mode (n2w a) (n2w b) (float_to_fp16 c) =
       float_to_fp16
         (SND
            (float_mul_sub mode (fp16_to_float (n2w a))
               (fp16_to_float (n2w b)) c))) ∧
  ∀mode c b a.
      fp16_mul_sub mode (n2w a) (n2w b) (n2w c) =
      float_to_fp16
        (SND
           (float_mul_sub mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b))
              (fp16_to_float (n2w c))))

fp16_mul_add_with_flags

⊢ (∀mode c b a.
       fp16_mul_add_with_flags mode (float_to_fp16 a) (float_to_fp16 b)
         (float_to_fp16 c) = (I ## float_to_fp16) (float_mul_add mode a b c)) ∧
  (∀mode c b a.
       fp16_mul_add_with_flags mode (float_to_fp16 a) (float_to_fp16 b)
         (n2w c) =
       (I ## float_to_fp16) (float_mul_add mode a b (fp16_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp16_mul_add_with_flags mode (float_to_fp16 a) (n2w b)
         (float_to_fp16 c) =
       (I ## float_to_fp16) (float_mul_add mode a (fp16_to_float (n2w b)) c)) ∧
  (∀mode c b a.
       fp16_mul_add_with_flags mode (float_to_fp16 a) (n2w b) (n2w c) =
       (I ## float_to_fp16)
         (float_mul_add mode a (fp16_to_float (n2w b)) (fp16_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp16_mul_add_with_flags mode (n2w a) (float_to_fp16 b)
         (float_to_fp16 c) =
       (I ## float_to_fp16) (float_mul_add mode (fp16_to_float (n2w a)) b c)) ∧
  (∀mode c b a.
       fp16_mul_add_with_flags mode (n2w a) (float_to_fp16 b) (n2w c) =
       (I ## float_to_fp16)
         (float_mul_add mode (fp16_to_float (n2w a)) b (fp16_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp16_mul_add_with_flags mode (n2w a) (n2w b) (float_to_fp16 c) =
       (I ## float_to_fp16)
         (float_mul_add mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b)) c)) ∧
  ∀mode c b a.
      fp16_mul_add_with_flags mode (n2w a) (n2w b) (n2w c) =
      (I ## float_to_fp16)
        (float_mul_add mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b))
           (fp16_to_float (n2w c)))

fp16_mul_sub_with_flags

⊢ (∀mode c b a.
       fp16_mul_sub_with_flags mode (float_to_fp16 a) (float_to_fp16 b)
         (float_to_fp16 c) = (I ## float_to_fp16) (float_mul_sub mode a b c)) ∧
  (∀mode c b a.
       fp16_mul_sub_with_flags mode (float_to_fp16 a) (float_to_fp16 b)
         (n2w c) =
       (I ## float_to_fp16) (float_mul_sub mode a b (fp16_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp16_mul_sub_with_flags mode (float_to_fp16 a) (n2w b)
         (float_to_fp16 c) =
       (I ## float_to_fp16) (float_mul_sub mode a (fp16_to_float (n2w b)) c)) ∧
  (∀mode c b a.
       fp16_mul_sub_with_flags mode (float_to_fp16 a) (n2w b) (n2w c) =
       (I ## float_to_fp16)
         (float_mul_sub mode a (fp16_to_float (n2w b)) (fp16_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp16_mul_sub_with_flags mode (n2w a) (float_to_fp16 b)
         (float_to_fp16 c) =
       (I ## float_to_fp16) (float_mul_sub mode (fp16_to_float (n2w a)) b c)) ∧
  (∀mode c b a.
       fp16_mul_sub_with_flags mode (n2w a) (float_to_fp16 b) (n2w c) =
       (I ## float_to_fp16)
         (float_mul_sub mode (fp16_to_float (n2w a)) b (fp16_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp16_mul_sub_with_flags mode (n2w a) (n2w b) (float_to_fp16 c) =
       (I ## float_to_fp16)
         (float_mul_sub mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b)) c)) ∧
  ∀mode c b a.
      fp16_mul_sub_with_flags mode (n2w a) (n2w b) (n2w c) =
      (I ## float_to_fp16)
        (float_mul_sub mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b))
           (fp16_to_float (n2w c)))

fp32_to_float_11

⊢ ∀x y. fp32_to_float x = fp32_to_float y ⇔ x = y

float_to_fp32_11

⊢ ∀x y. float_to_fp32 x = float_to_fp32 y ⇔ x = y

float_to_fp32_fp32_to_float

⊢ ∀x. float_to_fp32 (fp32_to_float x) = x

fp32_to_float_float_to_fp32

⊢ ∀x. fp32_to_float (float_to_fp32 x) = x

fp32_nchotomy

⊢ ∀x. ∃y. x = float_to_fp32 y

float_fp32_nchotomy

⊢ ∀x. ∃y. x = fp32_to_float y

fp32_to_float_n2w

⊢ ∀n.
      fp32_to_float (n2w n) =
      (let
         (q,f) = DIVMOD_2EXP 23 n ;
         (s,e) = DIVMOD_2EXP 8 q
       in
         <|Sign := n2w (s MOD 2); Exponent := n2w e; Significand := n2w f|>)

fp32_sqrt

⊢ (∀mode a.
       fp32_sqrt mode (float_to_fp32 a) =
       float_to_fp32 (SND (float_sqrt mode a))) ∧
  ∀mode a.
      fp32_sqrt mode (n2w a) =
      float_to_fp32 (SND (float_sqrt mode (fp32_to_float (n2w a))))

fp32_add

⊢ (∀mode b a.
       fp32_add mode (float_to_fp32 a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_add a) b))) ∧
  (∀mode b a.
       fp32_add mode (float_to_fp32 a) (n2w b) =
       float_to_fp32 (SND ((mode float_add a) (fp32_to_float (n2w b))))) ∧
  (∀mode b a.
       fp32_add mode (n2w a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_add fp32_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp32_add mode (n2w a) (n2w b) =
      float_to_fp32
        (SND ((mode float_add fp32_to_float (n2w a)) (fp32_to_float (n2w b))))

fp32_sub

⊢ (∀mode b a.
       fp32_sub mode (float_to_fp32 a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_sub a) b))) ∧
  (∀mode b a.
       fp32_sub mode (float_to_fp32 a) (n2w b) =
       float_to_fp32 (SND ((mode float_sub a) (fp32_to_float (n2w b))))) ∧
  (∀mode b a.
       fp32_sub mode (n2w a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_sub fp32_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp32_sub mode (n2w a) (n2w b) =
      float_to_fp32
        (SND ((mode float_sub fp32_to_float (n2w a)) (fp32_to_float (n2w b))))

fp32_mul

⊢ (∀mode b a.
       fp32_mul mode (float_to_fp32 a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_mul a) b))) ∧
  (∀mode b a.
       fp32_mul mode (float_to_fp32 a) (n2w b) =
       float_to_fp32 (SND ((mode float_mul a) (fp32_to_float (n2w b))))) ∧
  (∀mode b a.
       fp32_mul mode (n2w a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_mul fp32_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp32_mul mode (n2w a) (n2w b) =
      float_to_fp32
        (SND ((mode float_mul fp32_to_float (n2w a)) (fp32_to_float (n2w b))))

fp32_div

⊢ (∀mode b a.
       fp32_div mode (float_to_fp32 a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_div a) b))) ∧
  (∀mode b a.
       fp32_div mode (float_to_fp32 a) (n2w b) =
       float_to_fp32 (SND ((mode float_div a) (fp32_to_float (n2w b))))) ∧
  (∀mode b a.
       fp32_div mode (n2w a) (float_to_fp32 b) =
       float_to_fp32 (SND ((mode float_div fp32_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp32_div mode (n2w a) (n2w b) =
      float_to_fp32
        (SND ((mode float_div fp32_to_float (n2w a)) (fp32_to_float (n2w b))))

fp32_compare

⊢ (∀b a. fp32_compare (float_to_fp32 a) (float_to_fp32 b) = float_compare a b) ∧
  (∀b a.
       fp32_compare (float_to_fp32 a) (n2w b) =
       float_compare a (fp32_to_float (n2w b))) ∧
  (∀b a.
       fp32_compare (n2w a) (float_to_fp32 b) =
       float_compare (fp32_to_float (n2w a)) b) ∧
  ∀b a.
      fp32_compare (n2w a) (n2w b) =
      float_compare (fp32_to_float (n2w a)) (fp32_to_float (n2w b))

fp32_equal

⊢ (∀b a. fp32_equal (float_to_fp32 a) (float_to_fp32 b) ⇔ float_equal a b) ∧
  (∀b a.
       fp32_equal (float_to_fp32 a) (n2w b) ⇔
       float_equal a (fp32_to_float (n2w b))) ∧
  (∀b a.
       fp32_equal (n2w a) (float_to_fp32 b) ⇔
       float_equal (fp32_to_float (n2w a)) b) ∧
  ∀b a.
      fp32_equal (n2w a) (n2w b) ⇔
      float_equal (fp32_to_float (n2w a)) (fp32_to_float (n2w b))

fp32_lessThan

⊢ (∀b a.
       fp32_lessThan (float_to_fp32 a) (float_to_fp32 b) ⇔ float_less_than a b) ∧
  (∀b a.
       fp32_lessThan (float_to_fp32 a) (n2w b) ⇔
       float_less_than a (fp32_to_float (n2w b))) ∧
  (∀b a.
       fp32_lessThan (n2w a) (float_to_fp32 b) ⇔
       float_less_than (fp32_to_float (n2w a)) b) ∧
  ∀b a.
      fp32_lessThan (n2w a) (n2w b) ⇔
      float_less_than (fp32_to_float (n2w a)) (fp32_to_float (n2w b))

fp32_lessEqual

⊢ (∀b a.
       fp32_lessEqual (float_to_fp32 a) (float_to_fp32 b) ⇔
       float_less_equal a b) ∧
  (∀b a.
       fp32_lessEqual (float_to_fp32 a) (n2w b) ⇔
       float_less_equal a (fp32_to_float (n2w b))) ∧
  (∀b a.
       fp32_lessEqual (n2w a) (float_to_fp32 b) ⇔
       float_less_equal (fp32_to_float (n2w a)) b) ∧
  ∀b a.
      fp32_lessEqual (n2w a) (n2w b) ⇔
      float_less_equal (fp32_to_float (n2w a)) (fp32_to_float (n2w b))

fp32_greaterThan

⊢ (∀b a.
       fp32_greaterThan (float_to_fp32 a) (float_to_fp32 b) ⇔
       float_greater_than a b) ∧
  (∀b a.
       fp32_greaterThan (float_to_fp32 a) (n2w b) ⇔
       float_greater_than a (fp32_to_float (n2w b))) ∧
  (∀b a.
       fp32_greaterThan (n2w a) (float_to_fp32 b) ⇔
       float_greater_than (fp32_to_float (n2w a)) b) ∧
  ∀b a.
      fp32_greaterThan (n2w a) (n2w b) ⇔
      float_greater_than (fp32_to_float (n2w a)) (fp32_to_float (n2w b))

fp32_greaterEqual

⊢ (∀b a.
       fp32_greaterEqual (float_to_fp32 a) (float_to_fp32 b) ⇔
       float_greater_equal a b) ∧
  (∀b a.
       fp32_greaterEqual (float_to_fp32 a) (n2w b) ⇔
       float_greater_equal a (fp32_to_float (n2w b))) ∧
  (∀b a.
       fp32_greaterEqual (n2w a) (float_to_fp32 b) ⇔
       float_greater_equal (fp32_to_float (n2w a)) b) ∧
  ∀b a.
      fp32_greaterEqual (n2w a) (n2w b) ⇔
      float_greater_equal (fp32_to_float (n2w a)) (fp32_to_float (n2w b))

fp32_to_real

⊢ (∀a. fp32_to_real (float_to_fp32 a) = float_value a) ∧
  ∀a. fp32_to_real (n2w a) = float_value (fp32_to_float (n2w a))

fp32_to_int

⊢ (∀mode a. fp32_to_int mode (float_to_fp32 a) = float_to_int mode a) ∧
  ∀mode a.
      fp32_to_int mode (n2w a) = float_to_int mode (fp32_to_float (n2w a))

fp32_abs

⊢ (∀a. fp32_abs (float_to_fp32 a) = float_to_fp32 (float_abs a)) ∧
  ∀a. fp32_abs (n2w a) = float_to_fp32 (float_abs (fp32_to_float (n2w a)))

fp32_negate

⊢ (∀a. fp32_negate (float_to_fp32 a) = float_to_fp32 (float_negate a)) ∧
  ∀a.
      fp32_negate (n2w a) =
      float_to_fp32 (float_negate (fp32_to_float (n2w a)))

fp32_isNan

⊢ (∀a. fp32_isNan (float_to_fp32 a) ⇔ float_is_nan a) ∧
  ∀a. fp32_isNan (n2w a) ⇔ float_is_nan (fp32_to_float (n2w a))

fp32_isSignallingNan

⊢ (∀a. fp32_isSignallingNan (float_to_fp32 a) ⇔ float_is_signalling a) ∧
  ∀a.
      fp32_isSignallingNan (n2w a) ⇔
      float_is_signalling (fp32_to_float (n2w a))

fp32_isIntegral

⊢ (∀a. fp32_isIntegral (float_to_fp32 a) ⇔ float_is_integral a) ∧
  ∀a. fp32_isIntegral (n2w a) ⇔ float_is_integral (fp32_to_float (n2w a))

fp32_isZero

⊢ (∀a. fp32_isZero (float_to_fp32 a) ⇔ float_is_zero a) ∧
  ∀a. fp32_isZero (n2w a) ⇔ float_is_zero (fp32_to_float (n2w a))

fp32_isNormal

⊢ (∀a. fp32_isNormal (float_to_fp32 a) ⇔ float_is_normal a) ∧
  ∀a. fp32_isNormal (n2w a) ⇔ float_is_normal (fp32_to_float (n2w a))

fp32_isSubnormal

⊢ (∀a. fp32_isSubnormal (float_to_fp32 a) ⇔ float_is_subnormal a) ∧
  ∀a. fp32_isSubnormal (n2w a) ⇔ float_is_subnormal (fp32_to_float (n2w a))

fp32_isFinite

⊢ (∀a. fp32_isFinite (float_to_fp32 a) ⇔ float_is_finite a) ∧
  ∀a. fp32_isFinite (n2w a) ⇔ float_is_finite (fp32_to_float (n2w a))

fp32_isInfinite

⊢ (∀a. fp32_isInfinite (float_to_fp32 a) ⇔ float_is_infinite a) ∧
  ∀a. fp32_isInfinite (n2w a) ⇔ float_is_infinite (fp32_to_float (n2w a))

fp32_roundToIntegral

⊢ (∀mode a.
       fp32_roundToIntegral mode (float_to_fp32 a) =
       float_to_fp32 (float_round_to_integral mode a)) ∧
  ∀mode a.
      fp32_roundToIntegral mode (n2w a) =
      float_to_fp32 (float_round_to_integral mode (fp32_to_float (n2w a)))

fp32_sqrt_with_flags

⊢ (∀mode a.
       fp32_sqrt_with_flags mode (float_to_fp32 a) =
       (I ## float_to_fp32) (float_sqrt mode a)) ∧
  ∀mode a.
      fp32_sqrt_with_flags mode (n2w a) =
      (I ## float_to_fp32) (float_sqrt mode (fp32_to_float (n2w a)))

fp32_add_with_flags

⊢ (∀mode b a.
       fp32_add_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_add a) b)) ∧
  (∀mode b a.
       fp32_add_with_flags mode (float_to_fp32 a) (n2w b) =
       (I ## float_to_fp32) ((mode float_add a) (fp32_to_float (n2w b)))) ∧
  (∀mode b a.
       fp32_add_with_flags mode (n2w a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_add fp32_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp32_add_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp32)
        ((mode float_add fp32_to_float (n2w a)) (fp32_to_float (n2w b)))

fp32_sub_with_flags

⊢ (∀mode b a.
       fp32_sub_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_sub a) b)) ∧
  (∀mode b a.
       fp32_sub_with_flags mode (float_to_fp32 a) (n2w b) =
       (I ## float_to_fp32) ((mode float_sub a) (fp32_to_float (n2w b)))) ∧
  (∀mode b a.
       fp32_sub_with_flags mode (n2w a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_sub fp32_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp32_sub_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp32)
        ((mode float_sub fp32_to_float (n2w a)) (fp32_to_float (n2w b)))

fp32_mul_with_flags

⊢ (∀mode b a.
       fp32_mul_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_mul a) b)) ∧
  (∀mode b a.
       fp32_mul_with_flags mode (float_to_fp32 a) (n2w b) =
       (I ## float_to_fp32) ((mode float_mul a) (fp32_to_float (n2w b)))) ∧
  (∀mode b a.
       fp32_mul_with_flags mode (n2w a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_mul fp32_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp32_mul_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp32)
        ((mode float_mul fp32_to_float (n2w a)) (fp32_to_float (n2w b)))

fp32_div_with_flags

⊢ (∀mode b a.
       fp32_div_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_div a) b)) ∧
  (∀mode b a.
       fp32_div_with_flags mode (float_to_fp32 a) (n2w b) =
       (I ## float_to_fp32) ((mode float_div a) (fp32_to_float (n2w b)))) ∧
  (∀mode b a.
       fp32_div_with_flags mode (n2w a) (float_to_fp32 b) =
       (I ## float_to_fp32) ((mode float_div fp32_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp32_div_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp32)
        ((mode float_div fp32_to_float (n2w a)) (fp32_to_float (n2w b)))

fp32_mul_add

⊢ (∀mode c b a.
       fp32_mul_add mode (float_to_fp32 a) (float_to_fp32 b) (float_to_fp32 c) =
       float_to_fp32 (SND (float_mul_add mode a b c))) ∧
  (∀mode c b a.
       fp32_mul_add mode (float_to_fp32 a) (float_to_fp32 b) (n2w c) =
       float_to_fp32 (SND (float_mul_add mode a b (fp32_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp32_mul_add mode (float_to_fp32 a) (n2w b) (float_to_fp32 c) =
       float_to_fp32 (SND (float_mul_add mode a (fp32_to_float (n2w b)) c))) ∧
  (∀mode c b a.
       fp32_mul_add mode (float_to_fp32 a) (n2w b) (n2w c) =
       float_to_fp32
         (SND
            (float_mul_add mode a (fp32_to_float (n2w b))
               (fp32_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp32_mul_add mode (n2w a) (float_to_fp32 b) (float_to_fp32 c) =
       float_to_fp32 (SND (float_mul_add mode (fp32_to_float (n2w a)) b c))) ∧
  (∀mode c b a.
       fp32_mul_add mode (n2w a) (float_to_fp32 b) (n2w c) =
       float_to_fp32
         (SND
            (float_mul_add mode (fp32_to_float (n2w a)) b
               (fp32_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp32_mul_add mode (n2w a) (n2w b) (float_to_fp32 c) =
       float_to_fp32
         (SND
            (float_mul_add mode (fp32_to_float (n2w a))
               (fp32_to_float (n2w b)) c))) ∧
  ∀mode c b a.
      fp32_mul_add mode (n2w a) (n2w b) (n2w c) =
      float_to_fp32
        (SND
           (float_mul_add mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b))
              (fp32_to_float (n2w c))))

fp32_mul_sub

⊢ (∀mode c b a.
       fp32_mul_sub mode (float_to_fp32 a) (float_to_fp32 b) (float_to_fp32 c) =
       float_to_fp32 (SND (float_mul_sub mode a b c))) ∧
  (∀mode c b a.
       fp32_mul_sub mode (float_to_fp32 a) (float_to_fp32 b) (n2w c) =
       float_to_fp32 (SND (float_mul_sub mode a b (fp32_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp32_mul_sub mode (float_to_fp32 a) (n2w b) (float_to_fp32 c) =
       float_to_fp32 (SND (float_mul_sub mode a (fp32_to_float (n2w b)) c))) ∧
  (∀mode c b a.
       fp32_mul_sub mode (float_to_fp32 a) (n2w b) (n2w c) =
       float_to_fp32
         (SND
            (float_mul_sub mode a (fp32_to_float (n2w b))
               (fp32_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp32_mul_sub mode (n2w a) (float_to_fp32 b) (float_to_fp32 c) =
       float_to_fp32 (SND (float_mul_sub mode (fp32_to_float (n2w a)) b c))) ∧
  (∀mode c b a.
       fp32_mul_sub mode (n2w a) (float_to_fp32 b) (n2w c) =
       float_to_fp32
         (SND
            (float_mul_sub mode (fp32_to_float (n2w a)) b
               (fp32_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp32_mul_sub mode (n2w a) (n2w b) (float_to_fp32 c) =
       float_to_fp32
         (SND
            (float_mul_sub mode (fp32_to_float (n2w a))
               (fp32_to_float (n2w b)) c))) ∧
  ∀mode c b a.
      fp32_mul_sub mode (n2w a) (n2w b) (n2w c) =
      float_to_fp32
        (SND
           (float_mul_sub mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b))
              (fp32_to_float (n2w c))))

fp32_mul_add_with_flags

⊢ (∀mode c b a.
       fp32_mul_add_with_flags mode (float_to_fp32 a) (float_to_fp32 b)
         (float_to_fp32 c) = (I ## float_to_fp32) (float_mul_add mode a b c)) ∧
  (∀mode c b a.
       fp32_mul_add_with_flags mode (float_to_fp32 a) (float_to_fp32 b)
         (n2w c) =
       (I ## float_to_fp32) (float_mul_add mode a b (fp32_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp32_mul_add_with_flags mode (float_to_fp32 a) (n2w b)
         (float_to_fp32 c) =
       (I ## float_to_fp32) (float_mul_add mode a (fp32_to_float (n2w b)) c)) ∧
  (∀mode c b a.
       fp32_mul_add_with_flags mode (float_to_fp32 a) (n2w b) (n2w c) =
       (I ## float_to_fp32)
         (float_mul_add mode a (fp32_to_float (n2w b)) (fp32_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp32_mul_add_with_flags mode (n2w a) (float_to_fp32 b)
         (float_to_fp32 c) =
       (I ## float_to_fp32) (float_mul_add mode (fp32_to_float (n2w a)) b c)) ∧
  (∀mode c b a.
       fp32_mul_add_with_flags mode (n2w a) (float_to_fp32 b) (n2w c) =
       (I ## float_to_fp32)
         (float_mul_add mode (fp32_to_float (n2w a)) b (fp32_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp32_mul_add_with_flags mode (n2w a) (n2w b) (float_to_fp32 c) =
       (I ## float_to_fp32)
         (float_mul_add mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b)) c)) ∧
  ∀mode c b a.
      fp32_mul_add_with_flags mode (n2w a) (n2w b) (n2w c) =
      (I ## float_to_fp32)
        (float_mul_add mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b))
           (fp32_to_float (n2w c)))

fp32_mul_sub_with_flags

⊢ (∀mode c b a.
       fp32_mul_sub_with_flags mode (float_to_fp32 a) (float_to_fp32 b)
         (float_to_fp32 c) = (I ## float_to_fp32) (float_mul_sub mode a b c)) ∧
  (∀mode c b a.
       fp32_mul_sub_with_flags mode (float_to_fp32 a) (float_to_fp32 b)
         (n2w c) =
       (I ## float_to_fp32) (float_mul_sub mode a b (fp32_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp32_mul_sub_with_flags mode (float_to_fp32 a) (n2w b)
         (float_to_fp32 c) =
       (I ## float_to_fp32) (float_mul_sub mode a (fp32_to_float (n2w b)) c)) ∧
  (∀mode c b a.
       fp32_mul_sub_with_flags mode (float_to_fp32 a) (n2w b) (n2w c) =
       (I ## float_to_fp32)
         (float_mul_sub mode a (fp32_to_float (n2w b)) (fp32_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp32_mul_sub_with_flags mode (n2w a) (float_to_fp32 b)
         (float_to_fp32 c) =
       (I ## float_to_fp32) (float_mul_sub mode (fp32_to_float (n2w a)) b c)) ∧
  (∀mode c b a.
       fp32_mul_sub_with_flags mode (n2w a) (float_to_fp32 b) (n2w c) =
       (I ## float_to_fp32)
         (float_mul_sub mode (fp32_to_float (n2w a)) b (fp32_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp32_mul_sub_with_flags mode (n2w a) (n2w b) (float_to_fp32 c) =
       (I ## float_to_fp32)
         (float_mul_sub mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b)) c)) ∧
  ∀mode c b a.
      fp32_mul_sub_with_flags mode (n2w a) (n2w b) (n2w c) =
      (I ## float_to_fp32)
        (float_mul_sub mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b))
           (fp32_to_float (n2w c)))

fp64_to_float_11

⊢ ∀x y. fp64_to_float x = fp64_to_float y ⇔ x = y

float_to_fp64_11

⊢ ∀x y. float_to_fp64 x = float_to_fp64 y ⇔ x = y

float_to_fp64_fp64_to_float

⊢ ∀x. float_to_fp64 (fp64_to_float x) = x

fp64_to_float_float_to_fp64

⊢ ∀x. fp64_to_float (float_to_fp64 x) = x

fp64_nchotomy

⊢ ∀x. ∃y. x = float_to_fp64 y

float_fp64_nchotomy

⊢ ∀x. ∃y. x = fp64_to_float y

fp64_to_float_n2w

⊢ ∀n.
      fp64_to_float (n2w n) =
      (let
         (q,f) = DIVMOD_2EXP 52 n ;
         (s,e) = DIVMOD_2EXP 11 q
       in
         <|Sign := n2w (s MOD 2); Exponent := n2w e; Significand := n2w f|>)

fp64_sqrt

⊢ (∀mode a.
       fp64_sqrt mode (float_to_fp64 a) =
       float_to_fp64 (SND (float_sqrt mode a))) ∧
  ∀mode a.
      fp64_sqrt mode (n2w a) =
      float_to_fp64 (SND (float_sqrt mode (fp64_to_float (n2w a))))

fp64_add

⊢ (∀mode b a.
       fp64_add mode (float_to_fp64 a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_add a) b))) ∧
  (∀mode b a.
       fp64_add mode (float_to_fp64 a) (n2w b) =
       float_to_fp64 (SND ((mode float_add a) (fp64_to_float (n2w b))))) ∧
  (∀mode b a.
       fp64_add mode (n2w a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_add fp64_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp64_add mode (n2w a) (n2w b) =
      float_to_fp64
        (SND ((mode float_add fp64_to_float (n2w a)) (fp64_to_float (n2w b))))

fp64_sub

⊢ (∀mode b a.
       fp64_sub mode (float_to_fp64 a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_sub a) b))) ∧
  (∀mode b a.
       fp64_sub mode (float_to_fp64 a) (n2w b) =
       float_to_fp64 (SND ((mode float_sub a) (fp64_to_float (n2w b))))) ∧
  (∀mode b a.
       fp64_sub mode (n2w a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_sub fp64_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp64_sub mode (n2w a) (n2w b) =
      float_to_fp64
        (SND ((mode float_sub fp64_to_float (n2w a)) (fp64_to_float (n2w b))))

fp64_mul

⊢ (∀mode b a.
       fp64_mul mode (float_to_fp64 a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_mul a) b))) ∧
  (∀mode b a.
       fp64_mul mode (float_to_fp64 a) (n2w b) =
       float_to_fp64 (SND ((mode float_mul a) (fp64_to_float (n2w b))))) ∧
  (∀mode b a.
       fp64_mul mode (n2w a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_mul fp64_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp64_mul mode (n2w a) (n2w b) =
      float_to_fp64
        (SND ((mode float_mul fp64_to_float (n2w a)) (fp64_to_float (n2w b))))

fp64_div

⊢ (∀mode b a.
       fp64_div mode (float_to_fp64 a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_div a) b))) ∧
  (∀mode b a.
       fp64_div mode (float_to_fp64 a) (n2w b) =
       float_to_fp64 (SND ((mode float_div a) (fp64_to_float (n2w b))))) ∧
  (∀mode b a.
       fp64_div mode (n2w a) (float_to_fp64 b) =
       float_to_fp64 (SND ((mode float_div fp64_to_float (n2w a)) b))) ∧
  ∀mode b a.
      fp64_div mode (n2w a) (n2w b) =
      float_to_fp64
        (SND ((mode float_div fp64_to_float (n2w a)) (fp64_to_float (n2w b))))

fp64_compare

⊢ (∀b a. fp64_compare (float_to_fp64 a) (float_to_fp64 b) = float_compare a b) ∧
  (∀b a.
       fp64_compare (float_to_fp64 a) (n2w b) =
       float_compare a (fp64_to_float (n2w b))) ∧
  (∀b a.
       fp64_compare (n2w a) (float_to_fp64 b) =
       float_compare (fp64_to_float (n2w a)) b) ∧
  ∀b a.
      fp64_compare (n2w a) (n2w b) =
      float_compare (fp64_to_float (n2w a)) (fp64_to_float (n2w b))

fp64_equal

⊢ (∀b a. fp64_equal (float_to_fp64 a) (float_to_fp64 b) ⇔ float_equal a b) ∧
  (∀b a.
       fp64_equal (float_to_fp64 a) (n2w b) ⇔
       float_equal a (fp64_to_float (n2w b))) ∧
  (∀b a.
       fp64_equal (n2w a) (float_to_fp64 b) ⇔
       float_equal (fp64_to_float (n2w a)) b) ∧
  ∀b a.
      fp64_equal (n2w a) (n2w b) ⇔
      float_equal (fp64_to_float (n2w a)) (fp64_to_float (n2w b))

fp64_lessThan

⊢ (∀b a.
       fp64_lessThan (float_to_fp64 a) (float_to_fp64 b) ⇔ float_less_than a b) ∧
  (∀b a.
       fp64_lessThan (float_to_fp64 a) (n2w b) ⇔
       float_less_than a (fp64_to_float (n2w b))) ∧
  (∀b a.
       fp64_lessThan (n2w a) (float_to_fp64 b) ⇔
       float_less_than (fp64_to_float (n2w a)) b) ∧
  ∀b a.
      fp64_lessThan (n2w a) (n2w b) ⇔
      float_less_than (fp64_to_float (n2w a)) (fp64_to_float (n2w b))

fp64_lessEqual

⊢ (∀b a.
       fp64_lessEqual (float_to_fp64 a) (float_to_fp64 b) ⇔
       float_less_equal a b) ∧
  (∀b a.
       fp64_lessEqual (float_to_fp64 a) (n2w b) ⇔
       float_less_equal a (fp64_to_float (n2w b))) ∧
  (∀b a.
       fp64_lessEqual (n2w a) (float_to_fp64 b) ⇔
       float_less_equal (fp64_to_float (n2w a)) b) ∧
  ∀b a.
      fp64_lessEqual (n2w a) (n2w b) ⇔
      float_less_equal (fp64_to_float (n2w a)) (fp64_to_float (n2w b))

fp64_greaterThan

⊢ (∀b a.
       fp64_greaterThan (float_to_fp64 a) (float_to_fp64 b) ⇔
       float_greater_than a b) ∧
  (∀b a.
       fp64_greaterThan (float_to_fp64 a) (n2w b) ⇔
       float_greater_than a (fp64_to_float (n2w b))) ∧
  (∀b a.
       fp64_greaterThan (n2w a) (float_to_fp64 b) ⇔
       float_greater_than (fp64_to_float (n2w a)) b) ∧
  ∀b a.
      fp64_greaterThan (n2w a) (n2w b) ⇔
      float_greater_than (fp64_to_float (n2w a)) (fp64_to_float (n2w b))

fp64_greaterEqual

⊢ (∀b a.
       fp64_greaterEqual (float_to_fp64 a) (float_to_fp64 b) ⇔
       float_greater_equal a b) ∧
  (∀b a.
       fp64_greaterEqual (float_to_fp64 a) (n2w b) ⇔
       float_greater_equal a (fp64_to_float (n2w b))) ∧
  (∀b a.
       fp64_greaterEqual (n2w a) (float_to_fp64 b) ⇔
       float_greater_equal (fp64_to_float (n2w a)) b) ∧
  ∀b a.
      fp64_greaterEqual (n2w a) (n2w b) ⇔
      float_greater_equal (fp64_to_float (n2w a)) (fp64_to_float (n2w b))

fp64_to_real

⊢ (∀a. fp64_to_real (float_to_fp64 a) = float_value a) ∧
  ∀a. fp64_to_real (n2w a) = float_value (fp64_to_float (n2w a))

fp64_to_int

⊢ (∀mode a. fp64_to_int mode (float_to_fp64 a) = float_to_int mode a) ∧
  ∀mode a.
      fp64_to_int mode (n2w a) = float_to_int mode (fp64_to_float (n2w a))

fp64_abs

⊢ (∀a. fp64_abs (float_to_fp64 a) = float_to_fp64 (float_abs a)) ∧
  ∀a. fp64_abs (n2w a) = float_to_fp64 (float_abs (fp64_to_float (n2w a)))

fp64_negate

⊢ (∀a. fp64_negate (float_to_fp64 a) = float_to_fp64 (float_negate a)) ∧
  ∀a.
      fp64_negate (n2w a) =
      float_to_fp64 (float_negate (fp64_to_float (n2w a)))

fp64_isNan

⊢ (∀a. fp64_isNan (float_to_fp64 a) ⇔ float_is_nan a) ∧
  ∀a. fp64_isNan (n2w a) ⇔ float_is_nan (fp64_to_float (n2w a))

fp64_isSignallingNan

⊢ (∀a. fp64_isSignallingNan (float_to_fp64 a) ⇔ float_is_signalling a) ∧
  ∀a.
      fp64_isSignallingNan (n2w a) ⇔
      float_is_signalling (fp64_to_float (n2w a))

fp64_isIntegral

⊢ (∀a. fp64_isIntegral (float_to_fp64 a) ⇔ float_is_integral a) ∧
  ∀a. fp64_isIntegral (n2w a) ⇔ float_is_integral (fp64_to_float (n2w a))

fp64_isZero

⊢ (∀a. fp64_isZero (float_to_fp64 a) ⇔ float_is_zero a) ∧
  ∀a. fp64_isZero (n2w a) ⇔ float_is_zero (fp64_to_float (n2w a))

fp64_isNormal

⊢ (∀a. fp64_isNormal (float_to_fp64 a) ⇔ float_is_normal a) ∧
  ∀a. fp64_isNormal (n2w a) ⇔ float_is_normal (fp64_to_float (n2w a))

fp64_isSubnormal

⊢ (∀a. fp64_isSubnormal (float_to_fp64 a) ⇔ float_is_subnormal a) ∧
  ∀a. fp64_isSubnormal (n2w a) ⇔ float_is_subnormal (fp64_to_float (n2w a))

fp64_isFinite

⊢ (∀a. fp64_isFinite (float_to_fp64 a) ⇔ float_is_finite a) ∧
  ∀a. fp64_isFinite (n2w a) ⇔ float_is_finite (fp64_to_float (n2w a))

fp64_isInfinite

⊢ (∀a. fp64_isInfinite (float_to_fp64 a) ⇔ float_is_infinite a) ∧
  ∀a. fp64_isInfinite (n2w a) ⇔ float_is_infinite (fp64_to_float (n2w a))

fp64_roundToIntegral

⊢ (∀mode a.
       fp64_roundToIntegral mode (float_to_fp64 a) =
       float_to_fp64 (float_round_to_integral mode a)) ∧
  ∀mode a.
      fp64_roundToIntegral mode (n2w a) =
      float_to_fp64 (float_round_to_integral mode (fp64_to_float (n2w a)))

fp64_sqrt_with_flags

⊢ (∀mode a.
       fp64_sqrt_with_flags mode (float_to_fp64 a) =
       (I ## float_to_fp64) (float_sqrt mode a)) ∧
  ∀mode a.
      fp64_sqrt_with_flags mode (n2w a) =
      (I ## float_to_fp64) (float_sqrt mode (fp64_to_float (n2w a)))

fp64_add_with_flags

⊢ (∀mode b a.
       fp64_add_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_add a) b)) ∧
  (∀mode b a.
       fp64_add_with_flags mode (float_to_fp64 a) (n2w b) =
       (I ## float_to_fp64) ((mode float_add a) (fp64_to_float (n2w b)))) ∧
  (∀mode b a.
       fp64_add_with_flags mode (n2w a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_add fp64_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp64_add_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp64)
        ((mode float_add fp64_to_float (n2w a)) (fp64_to_float (n2w b)))

fp64_sub_with_flags

⊢ (∀mode b a.
       fp64_sub_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_sub a) b)) ∧
  (∀mode b a.
       fp64_sub_with_flags mode (float_to_fp64 a) (n2w b) =
       (I ## float_to_fp64) ((mode float_sub a) (fp64_to_float (n2w b)))) ∧
  (∀mode b a.
       fp64_sub_with_flags mode (n2w a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_sub fp64_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp64_sub_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp64)
        ((mode float_sub fp64_to_float (n2w a)) (fp64_to_float (n2w b)))

fp64_mul_with_flags

⊢ (∀mode b a.
       fp64_mul_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_mul a) b)) ∧
  (∀mode b a.
       fp64_mul_with_flags mode (float_to_fp64 a) (n2w b) =
       (I ## float_to_fp64) ((mode float_mul a) (fp64_to_float (n2w b)))) ∧
  (∀mode b a.
       fp64_mul_with_flags mode (n2w a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_mul fp64_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp64_mul_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp64)
        ((mode float_mul fp64_to_float (n2w a)) (fp64_to_float (n2w b)))

fp64_div_with_flags

⊢ (∀mode b a.
       fp64_div_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_div a) b)) ∧
  (∀mode b a.
       fp64_div_with_flags mode (float_to_fp64 a) (n2w b) =
       (I ## float_to_fp64) ((mode float_div a) (fp64_to_float (n2w b)))) ∧
  (∀mode b a.
       fp64_div_with_flags mode (n2w a) (float_to_fp64 b) =
       (I ## float_to_fp64) ((mode float_div fp64_to_float (n2w a)) b)) ∧
  ∀mode b a.
      fp64_div_with_flags mode (n2w a) (n2w b) =
      (I ## float_to_fp64)
        ((mode float_div fp64_to_float (n2w a)) (fp64_to_float (n2w b)))

fp64_mul_add

⊢ (∀mode c b a.
       fp64_mul_add mode (float_to_fp64 a) (float_to_fp64 b) (float_to_fp64 c) =
       float_to_fp64 (SND (float_mul_add mode a b c))) ∧
  (∀mode c b a.
       fp64_mul_add mode (float_to_fp64 a) (float_to_fp64 b) (n2w c) =
       float_to_fp64 (SND (float_mul_add mode a b (fp64_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp64_mul_add mode (float_to_fp64 a) (n2w b) (float_to_fp64 c) =
       float_to_fp64 (SND (float_mul_add mode a (fp64_to_float (n2w b)) c))) ∧
  (∀mode c b a.
       fp64_mul_add mode (float_to_fp64 a) (n2w b) (n2w c) =
       float_to_fp64
         (SND
            (float_mul_add mode a (fp64_to_float (n2w b))
               (fp64_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp64_mul_add mode (n2w a) (float_to_fp64 b) (float_to_fp64 c) =
       float_to_fp64 (SND (float_mul_add mode (fp64_to_float (n2w a)) b c))) ∧
  (∀mode c b a.
       fp64_mul_add mode (n2w a) (float_to_fp64 b) (n2w c) =
       float_to_fp64
         (SND
            (float_mul_add mode (fp64_to_float (n2w a)) b
               (fp64_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp64_mul_add mode (n2w a) (n2w b) (float_to_fp64 c) =
       float_to_fp64
         (SND
            (float_mul_add mode (fp64_to_float (n2w a))
               (fp64_to_float (n2w b)) c))) ∧
  ∀mode c b a.
      fp64_mul_add mode (n2w a) (n2w b) (n2w c) =
      float_to_fp64
        (SND
           (float_mul_add mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b))
              (fp64_to_float (n2w c))))

fp64_mul_sub

⊢ (∀mode c b a.
       fp64_mul_sub mode (float_to_fp64 a) (float_to_fp64 b) (float_to_fp64 c) =
       float_to_fp64 (SND (float_mul_sub mode a b c))) ∧
  (∀mode c b a.
       fp64_mul_sub mode (float_to_fp64 a) (float_to_fp64 b) (n2w c) =
       float_to_fp64 (SND (float_mul_sub mode a b (fp64_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp64_mul_sub mode (float_to_fp64 a) (n2w b) (float_to_fp64 c) =
       float_to_fp64 (SND (float_mul_sub mode a (fp64_to_float (n2w b)) c))) ∧
  (∀mode c b a.
       fp64_mul_sub mode (float_to_fp64 a) (n2w b) (n2w c) =
       float_to_fp64
         (SND
            (float_mul_sub mode a (fp64_to_float (n2w b))
               (fp64_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp64_mul_sub mode (n2w a) (float_to_fp64 b) (float_to_fp64 c) =
       float_to_fp64 (SND (float_mul_sub mode (fp64_to_float (n2w a)) b c))) ∧
  (∀mode c b a.
       fp64_mul_sub mode (n2w a) (float_to_fp64 b) (n2w c) =
       float_to_fp64
         (SND
            (float_mul_sub mode (fp64_to_float (n2w a)) b
               (fp64_to_float (n2w c))))) ∧
  (∀mode c b a.
       fp64_mul_sub mode (n2w a) (n2w b) (float_to_fp64 c) =
       float_to_fp64
         (SND
            (float_mul_sub mode (fp64_to_float (n2w a))
               (fp64_to_float (n2w b)) c))) ∧
  ∀mode c b a.
      fp64_mul_sub mode (n2w a) (n2w b) (n2w c) =
      float_to_fp64
        (SND
           (float_mul_sub mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b))
              (fp64_to_float (n2w c))))

fp64_mul_add_with_flags

⊢ (∀mode c b a.
       fp64_mul_add_with_flags mode (float_to_fp64 a) (float_to_fp64 b)
         (float_to_fp64 c) = (I ## float_to_fp64) (float_mul_add mode a b c)) ∧
  (∀mode c b a.
       fp64_mul_add_with_flags mode (float_to_fp64 a) (float_to_fp64 b)
         (n2w c) =
       (I ## float_to_fp64) (float_mul_add mode a b (fp64_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp64_mul_add_with_flags mode (float_to_fp64 a) (n2w b)
         (float_to_fp64 c) =
       (I ## float_to_fp64) (float_mul_add mode a (fp64_to_float (n2w b)) c)) ∧
  (∀mode c b a.
       fp64_mul_add_with_flags mode (float_to_fp64 a) (n2w b) (n2w c) =
       (I ## float_to_fp64)
         (float_mul_add mode a (fp64_to_float (n2w b)) (fp64_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp64_mul_add_with_flags mode (n2w a) (float_to_fp64 b)
         (float_to_fp64 c) =
       (I ## float_to_fp64) (float_mul_add mode (fp64_to_float (n2w a)) b c)) ∧
  (∀mode c b a.
       fp64_mul_add_with_flags mode (n2w a) (float_to_fp64 b) (n2w c) =
       (I ## float_to_fp64)
         (float_mul_add mode (fp64_to_float (n2w a)) b (fp64_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp64_mul_add_with_flags mode (n2w a) (n2w b) (float_to_fp64 c) =
       (I ## float_to_fp64)
         (float_mul_add mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b)) c)) ∧
  ∀mode c b a.
      fp64_mul_add_with_flags mode (n2w a) (n2w b) (n2w c) =
      (I ## float_to_fp64)
        (float_mul_add mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b))
           (fp64_to_float (n2w c)))

fp64_mul_sub_with_flags

⊢ (∀mode c b a.
       fp64_mul_sub_with_flags mode (float_to_fp64 a) (float_to_fp64 b)
         (float_to_fp64 c) = (I ## float_to_fp64) (float_mul_sub mode a b c)) ∧
  (∀mode c b a.
       fp64_mul_sub_with_flags mode (float_to_fp64 a) (float_to_fp64 b)
         (n2w c) =
       (I ## float_to_fp64) (float_mul_sub mode a b (fp64_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp64_mul_sub_with_flags mode (float_to_fp64 a) (n2w b)
         (float_to_fp64 c) =
       (I ## float_to_fp64) (float_mul_sub mode a (fp64_to_float (n2w b)) c)) ∧
  (∀mode c b a.
       fp64_mul_sub_with_flags mode (float_to_fp64 a) (n2w b) (n2w c) =
       (I ## float_to_fp64)
         (float_mul_sub mode a (fp64_to_float (n2w b)) (fp64_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp64_mul_sub_with_flags mode (n2w a) (float_to_fp64 b)
         (float_to_fp64 c) =
       (I ## float_to_fp64) (float_mul_sub mode (fp64_to_float (n2w a)) b c)) ∧
  (∀mode c b a.
       fp64_mul_sub_with_flags mode (n2w a) (float_to_fp64 b) (n2w c) =
       (I ## float_to_fp64)
         (float_mul_sub mode (fp64_to_float (n2w a)) b (fp64_to_float (n2w c)))) ∧
  (∀mode c b a.
       fp64_mul_sub_with_flags mode (n2w a) (n2w b) (float_to_fp64 c) =
       (I ## float_to_fp64)
         (float_mul_sub mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b)) c)) ∧
  ∀mode c b a.
      fp64_mul_sub_with_flags mode (n2w a) (n2w b) (n2w c) =
      (I ## float_to_fp64)
        (float_mul_sub mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b))
           (fp64_to_float (n2w c)))