Structure machine_ieeeTheory


Source File Identifier index Theory binding index

signature machine_ieeeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val convert_def : thm
    val float_to_fp16_def : thm
    val float_to_fp32_def : thm
    val float_to_fp64_def : thm
    val fp16_abs_def : thm
    val fp16_add_def : thm
    val fp16_add_with_flags_def : thm
    val fp16_bottom_def : thm
    val fp16_compare_def : thm
    val fp16_div_def : thm
    val fp16_div_with_flags_def : thm
    val fp16_equal_def : thm
    val fp16_greaterEqual_def : thm
    val fp16_greaterThan_def : thm
    val fp16_isFinite_def : thm
    val fp16_isInfinite_def : thm
    val fp16_isIntegral_def : thm
    val fp16_isNan_def : thm
    val fp16_isNormal_def : thm
    val fp16_isSignallingNan_def : thm
    val fp16_isSubnormal_def : thm
    val fp16_isZero_def : thm
    val fp16_lessEqual_def : thm
    val fp16_lessThan_def : thm
    val fp16_mul_add_def : thm
    val fp16_mul_add_with_flags_def : thm
    val fp16_mul_def : thm
    val fp16_mul_sub_def : thm
    val fp16_mul_sub_with_flags_def : thm
    val fp16_mul_with_flags_def : thm
    val fp16_negInf_def : thm
    val fp16_negMin_def : thm
    val fp16_negZero_def : thm
    val fp16_negate_def : thm
    val fp16_posInf_def : thm
    val fp16_posMin_def : thm
    val fp16_posZero_def : thm
    val fp16_roundToIntegral_def : thm
    val fp16_sqrt_def : thm
    val fp16_sqrt_with_flags_def : thm
    val fp16_sub_def : thm
    val fp16_sub_with_flags_def : thm
    val fp16_to_float_def : thm
    val fp16_to_fp32_def : thm
    val fp16_to_fp32_with_flags_def : thm
    val fp16_to_fp64_def : thm
    val fp16_to_fp64_with_flags_def : thm
    val fp16_to_int_def : thm
    val fp16_to_real_def : thm
    val fp16_to_value_def : thm
    val fp16_top_def : thm
    val fp32_abs_def : thm
    val fp32_add_def : thm
    val fp32_add_with_flags_def : thm
    val fp32_bottom_def : thm
    val fp32_compare_def : thm
    val fp32_div_def : thm
    val fp32_div_with_flags_def : thm
    val fp32_equal_def : thm
    val fp32_greaterEqual_def : thm
    val fp32_greaterThan_def : thm
    val fp32_isFinite_def : thm
    val fp32_isInfinite_def : thm
    val fp32_isIntegral_def : thm
    val fp32_isNan_def : thm
    val fp32_isNormal_def : thm
    val fp32_isSignallingNan_def : thm
    val fp32_isSubnormal_def : thm
    val fp32_isZero_def : thm
    val fp32_lessEqual_def : thm
    val fp32_lessThan_def : thm
    val fp32_mul_add_def : thm
    val fp32_mul_add_with_flags_def : thm
    val fp32_mul_def : thm
    val fp32_mul_sub_def : thm
    val fp32_mul_sub_with_flags_def : thm
    val fp32_mul_with_flags_def : thm
    val fp32_negInf_def : thm
    val fp32_negMin_def : thm
    val fp32_negZero_def : thm
    val fp32_negate_def : thm
    val fp32_posInf_def : thm
    val fp32_posMin_def : thm
    val fp32_posZero_def : thm
    val fp32_roundToIntegral_def : thm
    val fp32_sqrt_def : thm
    val fp32_sqrt_with_flags_def : thm
    val fp32_sub_def : thm
    val fp32_sub_with_flags_def : thm
    val fp32_to_float_def : thm
    val fp32_to_fp16_def : thm
    val fp32_to_fp16_with_flags_def : thm
    val fp32_to_fp64_def : thm
    val fp32_to_fp64_with_flags_def : thm
    val fp32_to_int_def : thm
    val fp32_to_real_def : thm
    val fp32_to_value_def : thm
    val fp32_top_def : thm
    val fp64_abs_def : thm
    val fp64_add_def : thm
    val fp64_add_with_flags_def : thm
    val fp64_bottom_def : thm
    val fp64_compare_def : thm
    val fp64_div_def : thm
    val fp64_div_with_flags_def : thm
    val fp64_equal_def : thm
    val fp64_greaterEqual_def : thm
    val fp64_greaterThan_def : thm
    val fp64_isFinite_def : thm
    val fp64_isInfinite_def : thm
    val fp64_isIntegral_def : thm
    val fp64_isNan_def : thm
    val fp64_isNormal_def : thm
    val fp64_isSignallingNan_def : thm
    val fp64_isSubnormal_def : thm
    val fp64_isZero_def : thm
    val fp64_lessEqual_def : thm
    val fp64_lessThan_def : thm
    val fp64_mul_add_def : thm
    val fp64_mul_add_with_flags_def : thm
    val fp64_mul_def : thm
    val fp64_mul_sub_def : thm
    val fp64_mul_sub_with_flags_def : thm
    val fp64_mul_with_flags_def : thm
    val fp64_negInf_def : thm
    val fp64_negMin_def : thm
    val fp64_negZero_def : thm
    val fp64_negate_def : thm
    val fp64_posInf_def : thm
    val fp64_posMin_def : thm
    val fp64_posZero_def : thm
    val fp64_roundToIntegral_def : thm
    val fp64_sqrt_def : thm
    val fp64_sqrt_with_flags_def : thm
    val fp64_sub_def : thm
    val fp64_sub_with_flags_def : thm
    val fp64_to_float_def : thm
    val fp64_to_fp16_def : thm
    val fp64_to_fp16_with_flags_def : thm
    val fp64_to_fp32_def : thm
    val fp64_to_fp32_with_flags_def : thm
    val fp64_to_int_def : thm
    val fp64_to_real_def : thm
    val fp64_to_value_def : thm
    val fp64_top_def : thm
    val int_to_fp16_def : thm
    val int_to_fp32_def : thm
    val int_to_fp64_def : thm
    val real_to_fp16_def : thm
    val real_to_fp16_with_flags_def : thm
    val real_to_fp32_def : thm
    val real_to_fp32_with_flags_def : thm
    val real_to_fp64_def : thm
    val real_to_fp64_with_flags_def : thm
  
  (*  Theorems  *)
    val float_fp16_nchotomy : thm
    val float_fp32_nchotomy : thm
    val float_fp64_nchotomy : thm
    val float_to_fp16_11 : thm
    val float_to_fp16_fp16_to_float : thm
    val float_to_fp32_11 : thm
    val float_to_fp32_fp32_to_float : thm
    val float_to_fp64_11 : thm
    val float_to_fp64_fp64_to_float : thm
    val fp16_abs : thm
    val fp16_add : thm
    val fp16_add_with_flags : thm
    val fp16_compare : thm
    val fp16_div : thm
    val fp16_div_with_flags : thm
    val fp16_equal : thm
    val fp16_greaterEqual : thm
    val fp16_greaterThan : thm
    val fp16_isFinite : thm
    val fp16_isInfinite : thm
    val fp16_isIntegral : thm
    val fp16_isNan : thm
    val fp16_isNormal : thm
    val fp16_isSignallingNan : thm
    val fp16_isSubnormal : thm
    val fp16_isZero : thm
    val fp16_lessEqual : thm
    val fp16_lessThan : thm
    val fp16_mul : thm
    val fp16_mul_add : thm
    val fp16_mul_add_with_flags : thm
    val fp16_mul_sub : thm
    val fp16_mul_sub_with_flags : thm
    val fp16_mul_with_flags : thm
    val fp16_nchotomy : thm
    val fp16_negate : thm
    val fp16_roundToIntegral : thm
    val fp16_sqrt : thm
    val fp16_sqrt_with_flags : thm
    val fp16_sub : thm
    val fp16_sub_with_flags : thm
    val fp16_to_float_11 : thm
    val fp16_to_float_float_to_fp16 : thm
    val fp16_to_float_n2w : thm
    val fp16_to_int : thm
    val fp16_to_real : thm
    val fp16_to_value : thm
    val fp32_abs : thm
    val fp32_add : thm
    val fp32_add_with_flags : thm
    val fp32_compare : thm
    val fp32_div : thm
    val fp32_div_with_flags : thm
    val fp32_equal : thm
    val fp32_greaterEqual : thm
    val fp32_greaterThan : thm
    val fp32_isFinite : thm
    val fp32_isInfinite : thm
    val fp32_isIntegral : thm
    val fp32_isNan : thm
    val fp32_isNormal : thm
    val fp32_isSignallingNan : thm
    val fp32_isSubnormal : thm
    val fp32_isZero : thm
    val fp32_lessEqual : thm
    val fp32_lessThan : thm
    val fp32_mul : thm
    val fp32_mul_add : thm
    val fp32_mul_add_with_flags : thm
    val fp32_mul_sub : thm
    val fp32_mul_sub_with_flags : thm
    val fp32_mul_with_flags : thm
    val fp32_nchotomy : thm
    val fp32_negate : thm
    val fp32_roundToIntegral : thm
    val fp32_sqrt : thm
    val fp32_sqrt_with_flags : thm
    val fp32_sub : thm
    val fp32_sub_with_flags : thm
    val fp32_to_float_11 : thm
    val fp32_to_float_float_to_fp32 : thm
    val fp32_to_float_n2w : thm
    val fp32_to_int : thm
    val fp32_to_real : thm
    val fp32_to_value : thm
    val fp64_abs : thm
    val fp64_add : thm
    val fp64_add_with_flags : thm
    val fp64_compare : thm
    val fp64_div : thm
    val fp64_div_with_flags : thm
    val fp64_equal : thm
    val fp64_greaterEqual : thm
    val fp64_greaterThan : thm
    val fp64_isFinite : thm
    val fp64_isInfinite : thm
    val fp64_isIntegral : thm
    val fp64_isNan : thm
    val fp64_isNormal : thm
    val fp64_isSignallingNan : thm
    val fp64_isSubnormal : thm
    val fp64_isZero : thm
    val fp64_lessEqual : thm
    val fp64_lessThan : thm
    val fp64_mul : thm
    val fp64_mul_add : thm
    val fp64_mul_add_with_flags : thm
    val fp64_mul_sub : thm
    val fp64_mul_sub_with_flags : thm
    val fp64_mul_with_flags : thm
    val fp64_nchotomy : thm
    val fp64_negate : thm
    val fp64_roundToIntegral : thm
    val fp64_sqrt : thm
    val fp64_sqrt_with_flags : thm
    val fp64_sub : thm
    val fp64_sub_with_flags : thm
    val fp64_to_float_11 : thm
    val fp64_to_float_float_to_fp64 : thm
    val fp64_to_float_n2w : thm
    val fp64_to_int : thm
    val fp64_to_real : thm
    val fp64_to_value : thm
  
  val machine_ieee_grammars : type_grammar.grammar * term_grammar.grammar
  
  val sqrt_CONV: Conv.conv ref
  val add_CONV: Conv.conv ref
  val sub_CONV: Conv.conv ref
  val mul_CONV: Conv.conv ref
  val div_CONV: Conv.conv ref
  val compare_CONV: Conv.conv ref
  val eq_CONV: Conv.conv ref
  val lt_CONV: Conv.conv ref
  val le_CONV: Conv.conv ref
  val gt_CONV: Conv.conv ref
  val ge_CONV: Conv.conv ref
  
(*
   [binary_ieee] Parent theory of "machine_ieee"
   
   [convert_def]  Definition
      
      ⊢ ∀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)))
   
   [float_to_fp16_def]  Definition
      
      ⊢ ∀x. float_to_fp16 x = x.Sign @@ x.Exponent @@ x.Significand
   
   [float_to_fp32_def]  Definition
      
      ⊢ ∀x. float_to_fp32 x = x.Sign @@ x.Exponent @@ x.Significand
   
   [float_to_fp64_def]  Definition
      
      ⊢ ∀x. float_to_fp64 x = x.Sign @@ x.Exponent @@ x.Significand
   
   [fp16_abs_def]  Definition
      
      ⊢ fp16_abs = float_to_fp16 ∘ float_abs ∘ fp16_to_float
   
   [fp16_add_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_add mode a b =
          float_to_fp16
            (SND (float_add mode (fp16_to_float a) (fp16_to_float b)))
   
   [fp16_add_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_add_with_flags mode a b =
          (I ## float_to_fp16)
            (float_add mode (fp16_to_float a) (fp16_to_float b))
   
   [fp16_bottom_def]  Definition
      
      ⊢ fp16_bottom = float_to_fp16 (float_bottom (:10 # 5))
   
   [fp16_compare_def]  Definition
      
      ⊢ ∀a b.
          fp16_compare a b =
          float_compare (fp16_to_float a) (fp16_to_float b)
   
   [fp16_div_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_div mode a b =
          float_to_fp16
            (SND (float_div mode (fp16_to_float a) (fp16_to_float b)))
   
   [fp16_div_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_div_with_flags mode a b =
          (I ## float_to_fp16)
            (float_div mode (fp16_to_float a) (fp16_to_float b))
   
   [fp16_equal_def]  Definition
      
      ⊢ ∀a b.
          fp16_equal a b ⇔ float_equal (fp16_to_float a) (fp16_to_float b)
   
   [fp16_greaterEqual_def]  Definition
      
      ⊢ ∀a b.
          fp16_greaterEqual a b ⇔
          float_greater_equal (fp16_to_float a) (fp16_to_float b)
   
   [fp16_greaterThan_def]  Definition
      
      ⊢ ∀a b.
          fp16_greaterThan a b ⇔
          float_greater_than (fp16_to_float a) (fp16_to_float b)
   
   [fp16_isFinite_def]  Definition
      
      ⊢ fp16_isFinite = float_is_finite ∘ fp16_to_float
   
   [fp16_isInfinite_def]  Definition
      
      ⊢ fp16_isInfinite = float_is_infinite ∘ fp16_to_float
   
   [fp16_isIntegral_def]  Definition
      
      ⊢ fp16_isIntegral = float_is_integral ∘ fp16_to_float
   
   [fp16_isNan_def]  Definition
      
      ⊢ fp16_isNan = float_is_nan ∘ fp16_to_float
   
   [fp16_isNormal_def]  Definition
      
      ⊢ fp16_isNormal = float_is_normal ∘ fp16_to_float
   
   [fp16_isSignallingNan_def]  Definition
      
      ⊢ fp16_isSignallingNan = float_is_signalling ∘ fp16_to_float
   
   [fp16_isSubnormal_def]  Definition
      
      ⊢ fp16_isSubnormal = float_is_subnormal ∘ fp16_to_float
   
   [fp16_isZero_def]  Definition
      
      ⊢ fp16_isZero = float_is_zero ∘ fp16_to_float
   
   [fp16_lessEqual_def]  Definition
      
      ⊢ ∀a b.
          fp16_lessEqual a b ⇔
          float_less_equal (fp16_to_float a) (fp16_to_float b)
   
   [fp16_lessThan_def]  Definition
      
      ⊢ ∀a b.
          fp16_lessThan a b ⇔
          float_less_than (fp16_to_float a) (fp16_to_float b)
   
   [fp16_mul_add_def]  Definition
      
      ⊢ ∀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_add_with_flags_def]  Definition
      
      ⊢ ∀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_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_mul mode a b =
          float_to_fp16
            (SND (float_mul mode (fp16_to_float a) (fp16_to_float b)))
   
   [fp16_mul_sub_def]  Definition
      
      ⊢ ∀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_sub_with_flags_def]  Definition
      
      ⊢ ∀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))
   
   [fp16_mul_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_mul_with_flags mode a b =
          (I ## float_to_fp16)
            (float_mul mode (fp16_to_float a) (fp16_to_float b))
   
   [fp16_negInf_def]  Definition
      
      ⊢ fp16_negInf = float_to_fp16 (float_minus_infinity (:10 # 5))
   
   [fp16_negMin_def]  Definition
      
      ⊢ fp16_negMin = float_to_fp16 (float_minus_min (:10 # 5))
   
   [fp16_negZero_def]  Definition
      
      ⊢ fp16_negZero = float_to_fp16 (float_minus_zero (:10 # 5))
   
   [fp16_negate_def]  Definition
      
      ⊢ fp16_negate = float_to_fp16 ∘ float_negate ∘ fp16_to_float
   
   [fp16_posInf_def]  Definition
      
      ⊢ fp16_posInf = float_to_fp16 (float_plus_infinity (:10 # 5))
   
   [fp16_posMin_def]  Definition
      
      ⊢ fp16_posMin = float_to_fp16 (float_plus_min (:10 # 5))
   
   [fp16_posZero_def]  Definition
      
      ⊢ fp16_posZero = float_to_fp16 (float_plus_zero (:10 # 5))
   
   [fp16_roundToIntegral_def]  Definition
      
      ⊢ ∀mode.
          fp16_roundToIntegral mode =
          float_to_fp16 ∘ float_round_to_integral mode ∘ fp16_to_float
   
   [fp16_sqrt_def]  Definition
      
      ⊢ ∀mode.
          fp16_sqrt mode =
          float_to_fp16 ∘ SND ∘ float_sqrt mode ∘ fp16_to_float
   
   [fp16_sqrt_with_flags_def]  Definition
      
      ⊢ ∀mode.
          fp16_sqrt_with_flags mode =
          (I ## float_to_fp16) ∘ float_sqrt mode ∘ fp16_to_float
   
   [fp16_sub_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_sub mode a b =
          float_to_fp16
            (SND (float_sub mode (fp16_to_float a) (fp16_to_float b)))
   
   [fp16_sub_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp16_sub_with_flags mode a b =
          (I ## float_to_fp16)
            (float_sub mode (fp16_to_float a) (fp16_to_float b))
   
   [fp16_to_float_def]  Definition
      
      ⊢ ∀w. fp16_to_float w =
            <|Sign := (15 >< 15) w; Exponent := (14 >< 10) w;
              Significand := (9 >< 0) w|>
   
   [fp16_to_fp32_def]  Definition
      
      ⊢ fp16_to_fp32 = SND ∘ fp16_to_fp32_with_flags
   
   [fp16_to_fp32_with_flags_def]  Definition
      
      ⊢ fp16_to_fp32_with_flags =
        convert fp16_to_float float_to_fp32 real_to_fp32_with_flags
          roundTiesToEven
   
   [fp16_to_fp64_def]  Definition
      
      ⊢ fp16_to_fp64 = SND ∘ fp16_to_fp64_with_flags
   
   [fp16_to_fp64_with_flags_def]  Definition
      
      ⊢ fp16_to_fp64_with_flags =
        convert fp16_to_float float_to_fp64 real_to_fp64_with_flags
          roundTiesToEven
   
   [fp16_to_int_def]  Definition
      
      ⊢ ∀mode. fp16_to_int mode = float_to_int mode ∘ fp16_to_float
   
   [fp16_to_real_def]  Definition
      
      ⊢ fp16_to_real = float_to_real ∘ fp16_to_float
   
   [fp16_to_value_def]  Definition
      
      ⊢ fp16_to_value = float_value ∘ fp16_to_float
   
   [fp16_top_def]  Definition
      
      ⊢ fp16_top = float_to_fp16 (float_top (:10 # 5))
   
   [fp32_abs_def]  Definition
      
      ⊢ fp32_abs = float_to_fp32 ∘ float_abs ∘ fp32_to_float
   
   [fp32_add_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_add mode a b =
          float_to_fp32
            (SND (float_add mode (fp32_to_float a) (fp32_to_float b)))
   
   [fp32_add_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_add_with_flags mode a b =
          (I ## float_to_fp32)
            (float_add mode (fp32_to_float a) (fp32_to_float b))
   
   [fp32_bottom_def]  Definition
      
      ⊢ fp32_bottom = float_to_fp32 (float_bottom (:23 # 8))
   
   [fp32_compare_def]  Definition
      
      ⊢ ∀a b.
          fp32_compare a b =
          float_compare (fp32_to_float a) (fp32_to_float b)
   
   [fp32_div_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_div mode a b =
          float_to_fp32
            (SND (float_div mode (fp32_to_float a) (fp32_to_float b)))
   
   [fp32_div_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_div_with_flags mode a b =
          (I ## float_to_fp32)
            (float_div mode (fp32_to_float a) (fp32_to_float b))
   
   [fp32_equal_def]  Definition
      
      ⊢ ∀a b.
          fp32_equal a b ⇔ float_equal (fp32_to_float a) (fp32_to_float b)
   
   [fp32_greaterEqual_def]  Definition
      
      ⊢ ∀a b.
          fp32_greaterEqual a b ⇔
          float_greater_equal (fp32_to_float a) (fp32_to_float b)
   
   [fp32_greaterThan_def]  Definition
      
      ⊢ ∀a b.
          fp32_greaterThan a b ⇔
          float_greater_than (fp32_to_float a) (fp32_to_float b)
   
   [fp32_isFinite_def]  Definition
      
      ⊢ fp32_isFinite = float_is_finite ∘ fp32_to_float
   
   [fp32_isInfinite_def]  Definition
      
      ⊢ fp32_isInfinite = float_is_infinite ∘ fp32_to_float
   
   [fp32_isIntegral_def]  Definition
      
      ⊢ fp32_isIntegral = float_is_integral ∘ fp32_to_float
   
   [fp32_isNan_def]  Definition
      
      ⊢ fp32_isNan = float_is_nan ∘ fp32_to_float
   
   [fp32_isNormal_def]  Definition
      
      ⊢ fp32_isNormal = float_is_normal ∘ fp32_to_float
   
   [fp32_isSignallingNan_def]  Definition
      
      ⊢ fp32_isSignallingNan = float_is_signalling ∘ fp32_to_float
   
   [fp32_isSubnormal_def]  Definition
      
      ⊢ fp32_isSubnormal = float_is_subnormal ∘ fp32_to_float
   
   [fp32_isZero_def]  Definition
      
      ⊢ fp32_isZero = float_is_zero ∘ fp32_to_float
   
   [fp32_lessEqual_def]  Definition
      
      ⊢ ∀a b.
          fp32_lessEqual a b ⇔
          float_less_equal (fp32_to_float a) (fp32_to_float b)
   
   [fp32_lessThan_def]  Definition
      
      ⊢ ∀a b.
          fp32_lessThan a b ⇔
          float_less_than (fp32_to_float a) (fp32_to_float b)
   
   [fp32_mul_add_def]  Definition
      
      ⊢ ∀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_add_with_flags_def]  Definition
      
      ⊢ ∀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_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_mul mode a b =
          float_to_fp32
            (SND (float_mul mode (fp32_to_float a) (fp32_to_float b)))
   
   [fp32_mul_sub_def]  Definition
      
      ⊢ ∀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_sub_with_flags_def]  Definition
      
      ⊢ ∀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))
   
   [fp32_mul_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_mul_with_flags mode a b =
          (I ## float_to_fp32)
            (float_mul mode (fp32_to_float a) (fp32_to_float b))
   
   [fp32_negInf_def]  Definition
      
      ⊢ fp32_negInf = float_to_fp32 (float_minus_infinity (:23 # 8))
   
   [fp32_negMin_def]  Definition
      
      ⊢ fp32_negMin = float_to_fp32 (float_minus_min (:23 # 8))
   
   [fp32_negZero_def]  Definition
      
      ⊢ fp32_negZero = float_to_fp32 (float_minus_zero (:23 # 8))
   
   [fp32_negate_def]  Definition
      
      ⊢ fp32_negate = float_to_fp32 ∘ float_negate ∘ fp32_to_float
   
   [fp32_posInf_def]  Definition
      
      ⊢ fp32_posInf = float_to_fp32 (float_plus_infinity (:23 # 8))
   
   [fp32_posMin_def]  Definition
      
      ⊢ fp32_posMin = float_to_fp32 (float_plus_min (:23 # 8))
   
   [fp32_posZero_def]  Definition
      
      ⊢ fp32_posZero = float_to_fp32 (float_plus_zero (:23 # 8))
   
   [fp32_roundToIntegral_def]  Definition
      
      ⊢ ∀mode.
          fp32_roundToIntegral mode =
          float_to_fp32 ∘ float_round_to_integral mode ∘ fp32_to_float
   
   [fp32_sqrt_def]  Definition
      
      ⊢ ∀mode.
          fp32_sqrt mode =
          float_to_fp32 ∘ SND ∘ float_sqrt mode ∘ fp32_to_float
   
   [fp32_sqrt_with_flags_def]  Definition
      
      ⊢ ∀mode.
          fp32_sqrt_with_flags mode =
          (I ## float_to_fp32) ∘ float_sqrt mode ∘ fp32_to_float
   
   [fp32_sub_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_sub mode a b =
          float_to_fp32
            (SND (float_sub mode (fp32_to_float a) (fp32_to_float b)))
   
   [fp32_sub_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp32_sub_with_flags mode a b =
          (I ## float_to_fp32)
            (float_sub mode (fp32_to_float a) (fp32_to_float b))
   
   [fp32_to_float_def]  Definition
      
      ⊢ ∀w. fp32_to_float w =
            <|Sign := (31 >< 31) w; Exponent := (30 >< 23) w;
              Significand := (22 >< 0) w|>
   
   [fp32_to_fp16_def]  Definition
      
      ⊢ ∀m. fp32_to_fp16 m = SND ∘ fp32_to_fp16_with_flags m
   
   [fp32_to_fp16_with_flags_def]  Definition
      
      ⊢ fp32_to_fp16_with_flags =
        convert fp32_to_float float_to_fp16 real_to_fp16_with_flags
   
   [fp32_to_fp64_def]  Definition
      
      ⊢ fp32_to_fp64 = SND ∘ fp32_to_fp64_with_flags
   
   [fp32_to_fp64_with_flags_def]  Definition
      
      ⊢ fp32_to_fp64_with_flags =
        convert fp32_to_float float_to_fp64 real_to_fp64_with_flags
          roundTiesToEven
   
   [fp32_to_int_def]  Definition
      
      ⊢ ∀mode. fp32_to_int mode = float_to_int mode ∘ fp32_to_float
   
   [fp32_to_real_def]  Definition
      
      ⊢ fp32_to_real = float_to_real ∘ fp32_to_float
   
   [fp32_to_value_def]  Definition
      
      ⊢ fp32_to_value = float_value ∘ fp32_to_float
   
   [fp32_top_def]  Definition
      
      ⊢ fp32_top = float_to_fp32 (float_top (:23 # 8))
   
   [fp64_abs_def]  Definition
      
      ⊢ fp64_abs = float_to_fp64 ∘ float_abs ∘ fp64_to_float
   
   [fp64_add_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_add mode a b =
          float_to_fp64
            (SND (float_add mode (fp64_to_float a) (fp64_to_float b)))
   
   [fp64_add_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_add_with_flags mode a b =
          (I ## float_to_fp64)
            (float_add mode (fp64_to_float a) (fp64_to_float b))
   
   [fp64_bottom_def]  Definition
      
      ⊢ fp64_bottom = float_to_fp64 (float_bottom (:52 # 11))
   
   [fp64_compare_def]  Definition
      
      ⊢ ∀a b.
          fp64_compare a b =
          float_compare (fp64_to_float a) (fp64_to_float b)
   
   [fp64_div_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_div mode a b =
          float_to_fp64
            (SND (float_div mode (fp64_to_float a) (fp64_to_float b)))
   
   [fp64_div_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_div_with_flags mode a b =
          (I ## float_to_fp64)
            (float_div mode (fp64_to_float a) (fp64_to_float b))
   
   [fp64_equal_def]  Definition
      
      ⊢ ∀a b.
          fp64_equal a b ⇔ float_equal (fp64_to_float a) (fp64_to_float b)
   
   [fp64_greaterEqual_def]  Definition
      
      ⊢ ∀a b.
          fp64_greaterEqual a b ⇔
          float_greater_equal (fp64_to_float a) (fp64_to_float b)
   
   [fp64_greaterThan_def]  Definition
      
      ⊢ ∀a b.
          fp64_greaterThan a b ⇔
          float_greater_than (fp64_to_float a) (fp64_to_float b)
   
   [fp64_isFinite_def]  Definition
      
      ⊢ fp64_isFinite = float_is_finite ∘ fp64_to_float
   
   [fp64_isInfinite_def]  Definition
      
      ⊢ fp64_isInfinite = float_is_infinite ∘ fp64_to_float
   
   [fp64_isIntegral_def]  Definition
      
      ⊢ fp64_isIntegral = float_is_integral ∘ fp64_to_float
   
   [fp64_isNan_def]  Definition
      
      ⊢ fp64_isNan = float_is_nan ∘ fp64_to_float
   
   [fp64_isNormal_def]  Definition
      
      ⊢ fp64_isNormal = float_is_normal ∘ fp64_to_float
   
   [fp64_isSignallingNan_def]  Definition
      
      ⊢ fp64_isSignallingNan = float_is_signalling ∘ fp64_to_float
   
   [fp64_isSubnormal_def]  Definition
      
      ⊢ fp64_isSubnormal = float_is_subnormal ∘ fp64_to_float
   
   [fp64_isZero_def]  Definition
      
      ⊢ fp64_isZero = float_is_zero ∘ fp64_to_float
   
   [fp64_lessEqual_def]  Definition
      
      ⊢ ∀a b.
          fp64_lessEqual a b ⇔
          float_less_equal (fp64_to_float a) (fp64_to_float b)
   
   [fp64_lessThan_def]  Definition
      
      ⊢ ∀a b.
          fp64_lessThan a b ⇔
          float_less_than (fp64_to_float a) (fp64_to_float b)
   
   [fp64_mul_add_def]  Definition
      
      ⊢ ∀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_add_with_flags_def]  Definition
      
      ⊢ ∀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_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_mul mode a b =
          float_to_fp64
            (SND (float_mul mode (fp64_to_float a) (fp64_to_float b)))
   
   [fp64_mul_sub_def]  Definition
      
      ⊢ ∀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_sub_with_flags_def]  Definition
      
      ⊢ ∀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))
   
   [fp64_mul_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_mul_with_flags mode a b =
          (I ## float_to_fp64)
            (float_mul mode (fp64_to_float a) (fp64_to_float b))
   
   [fp64_negInf_def]  Definition
      
      ⊢ fp64_negInf = float_to_fp64 (float_minus_infinity (:52 # 11))
   
   [fp64_negMin_def]  Definition
      
      ⊢ fp64_negMin = float_to_fp64 (float_minus_min (:52 # 11))
   
   [fp64_negZero_def]  Definition
      
      ⊢ fp64_negZero = float_to_fp64 (float_minus_zero (:52 # 11))
   
   [fp64_negate_def]  Definition
      
      ⊢ fp64_negate = float_to_fp64 ∘ float_negate ∘ fp64_to_float
   
   [fp64_posInf_def]  Definition
      
      ⊢ fp64_posInf = float_to_fp64 (float_plus_infinity (:52 # 11))
   
   [fp64_posMin_def]  Definition
      
      ⊢ fp64_posMin = float_to_fp64 (float_plus_min (:52 # 11))
   
   [fp64_posZero_def]  Definition
      
      ⊢ fp64_posZero = float_to_fp64 (float_plus_zero (:52 # 11))
   
   [fp64_roundToIntegral_def]  Definition
      
      ⊢ ∀mode.
          fp64_roundToIntegral mode =
          float_to_fp64 ∘ float_round_to_integral mode ∘ fp64_to_float
   
   [fp64_sqrt_def]  Definition
      
      ⊢ ∀mode.
          fp64_sqrt mode =
          float_to_fp64 ∘ SND ∘ float_sqrt mode ∘ fp64_to_float
   
   [fp64_sqrt_with_flags_def]  Definition
      
      ⊢ ∀mode.
          fp64_sqrt_with_flags mode =
          (I ## float_to_fp64) ∘ float_sqrt mode ∘ fp64_to_float
   
   [fp64_sub_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_sub mode a b =
          float_to_fp64
            (SND (float_sub mode (fp64_to_float a) (fp64_to_float b)))
   
   [fp64_sub_with_flags_def]  Definition
      
      ⊢ ∀mode a b.
          fp64_sub_with_flags mode a b =
          (I ## float_to_fp64)
            (float_sub mode (fp64_to_float a) (fp64_to_float b))
   
   [fp64_to_float_def]  Definition
      
      ⊢ ∀w. fp64_to_float w =
            <|Sign := (63 >< 63) w; Exponent := (62 >< 52) w;
              Significand := (51 >< 0) w|>
   
   [fp64_to_fp16_def]  Definition
      
      ⊢ ∀m. fp64_to_fp16 m = SND ∘ fp64_to_fp16_with_flags m
   
   [fp64_to_fp16_with_flags_def]  Definition
      
      ⊢ fp64_to_fp16_with_flags =
        convert fp64_to_float float_to_fp16 real_to_fp16_with_flags
   
   [fp64_to_fp32_def]  Definition
      
      ⊢ ∀m. fp64_to_fp32 m = SND ∘ fp64_to_fp32_with_flags m
   
   [fp64_to_fp32_with_flags_def]  Definition
      
      ⊢ fp64_to_fp32_with_flags =
        convert fp64_to_float float_to_fp32 real_to_fp32_with_flags
   
   [fp64_to_int_def]  Definition
      
      ⊢ ∀mode. fp64_to_int mode = float_to_int mode ∘ fp64_to_float
   
   [fp64_to_real_def]  Definition
      
      ⊢ fp64_to_real = float_to_real ∘ fp64_to_float
   
   [fp64_to_value_def]  Definition
      
      ⊢ fp64_to_value = float_value ∘ fp64_to_float
   
   [fp64_top_def]  Definition
      
      ⊢ fp64_top = float_to_fp64 (float_top (:52 # 11))
   
   [int_to_fp16_def]  Definition
      
      ⊢ ∀mode a. int_to_fp16 mode a = real_to_fp16 mode (real_of_int a)
   
   [int_to_fp32_def]  Definition
      
      ⊢ ∀mode a. int_to_fp32 mode a = real_to_fp32 mode (real_of_int a)
   
   [int_to_fp64_def]  Definition
      
      ⊢ ∀mode a. int_to_fp64 mode a = real_to_fp64 mode (real_of_int a)
   
   [real_to_fp16_def]  Definition
      
      ⊢ ∀mode. real_to_fp16 mode = float_to_fp16 ∘ real_to_float mode
   
   [real_to_fp16_with_flags_def]  Definition
      
      ⊢ ∀mode.
          real_to_fp16_with_flags mode =
          (I ## float_to_fp16) ∘ real_to_float_with_flags mode
   
   [real_to_fp32_def]  Definition
      
      ⊢ ∀mode. real_to_fp32 mode = float_to_fp32 ∘ real_to_float mode
   
   [real_to_fp32_with_flags_def]  Definition
      
      ⊢ ∀mode.
          real_to_fp32_with_flags mode =
          (I ## float_to_fp32) ∘ real_to_float_with_flags mode
   
   [real_to_fp64_def]  Definition
      
      ⊢ ∀mode. real_to_fp64 mode = float_to_fp64 ∘ real_to_float mode
   
   [real_to_fp64_with_flags_def]  Definition
      
      ⊢ ∀mode.
          real_to_fp64_with_flags mode =
          (I ## float_to_fp64) ∘ real_to_float_with_flags mode
   
   [float_fp16_nchotomy]  Theorem
      
      ⊢ ∀x. ∃y. x = fp16_to_float y
   
   [float_fp32_nchotomy]  Theorem
      
      ⊢ ∀x. ∃y. x = fp32_to_float y
   
   [float_fp64_nchotomy]  Theorem
      
      ⊢ ∀x. ∃y. x = fp64_to_float y
   
   [float_to_fp16_11]  Theorem
      
      ⊢ ∀x y. float_to_fp16 x = float_to_fp16 y ⇔ x = y
   
   [float_to_fp16_fp16_to_float]  Theorem
      
      ⊢ ∀x. float_to_fp16 (fp16_to_float x) = x
   
   [float_to_fp32_11]  Theorem
      
      ⊢ ∀x y. float_to_fp32 x = float_to_fp32 y ⇔ x = y
   
   [float_to_fp32_fp32_to_float]  Theorem
      
      ⊢ ∀x. float_to_fp32 (fp32_to_float x) = x
   
   [float_to_fp64_11]  Theorem
      
      ⊢ ∀x y. float_to_fp64 x = float_to_fp64 y ⇔ x = y
   
   [float_to_fp64_fp64_to_float]  Theorem
      
      ⊢ ∀x. float_to_fp64 (fp64_to_float x) = x
   
   [fp16_abs]  Theorem
      
      ⊢ (∀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_add]  Theorem
      
      ⊢ (∀mode b a.
           fp16_add mode (float_to_fp16 a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_add mode a b))) ∧
        (∀mode b a.
           fp16_add mode (float_to_fp16 a) (n2w b) =
           float_to_fp16 (SND (float_add mode a (fp16_to_float (n2w b))))) ∧
        (∀mode b a.
           fp16_add mode (n2w a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_add mode (fp16_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp16_add mode (n2w a) (n2w b) =
          float_to_fp16
            (SND
               (float_add mode (fp16_to_float (n2w a))
                  (fp16_to_float (n2w b))))
   
   [fp16_add_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp16_add_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_add mode a b)) ∧
        (∀mode b a.
           fp16_add_with_flags mode (float_to_fp16 a) (n2w b) =
           (I ## float_to_fp16) (float_add mode a (fp16_to_float (n2w b)))) ∧
        (∀mode b a.
           fp16_add_with_flags mode (n2w a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_add mode (fp16_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp16_add_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp16)
            (float_add mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b)))
   
   [fp16_compare]  Theorem
      
      ⊢ (∀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_div]  Theorem
      
      ⊢ (∀mode b a.
           fp16_div mode (float_to_fp16 a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_div mode a b))) ∧
        (∀mode b a.
           fp16_div mode (float_to_fp16 a) (n2w b) =
           float_to_fp16 (SND (float_div mode a (fp16_to_float (n2w b))))) ∧
        (∀mode b a.
           fp16_div mode (n2w a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_div mode (fp16_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp16_div mode (n2w a) (n2w b) =
          float_to_fp16
            (SND
               (float_div mode (fp16_to_float (n2w a))
                  (fp16_to_float (n2w b))))
   
   [fp16_div_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp16_div_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_div mode a b)) ∧
        (∀mode b a.
           fp16_div_with_flags mode (float_to_fp16 a) (n2w b) =
           (I ## float_to_fp16) (float_div mode a (fp16_to_float (n2w b)))) ∧
        (∀mode b a.
           fp16_div_with_flags mode (n2w a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_div mode (fp16_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp16_div_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp16)
            (float_div mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b)))
   
   [fp16_equal]  Theorem
      
      ⊢ (∀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_greaterEqual]  Theorem
      
      ⊢ (∀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_greaterThan]  Theorem
      
      ⊢ (∀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_isFinite]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_isIntegral]  Theorem
      
      ⊢ (∀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_isNan]  Theorem
      
      ⊢ (∀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_isNormal]  Theorem
      
      ⊢ (∀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_isSignallingNan]  Theorem
      
      ⊢ (∀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_isSubnormal]  Theorem
      
      ⊢ (∀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_isZero]  Theorem
      
      ⊢ (∀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_lessEqual]  Theorem
      
      ⊢ (∀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_lessThan]  Theorem
      
      ⊢ (∀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_mul]  Theorem
      
      ⊢ (∀mode b a.
           fp16_mul mode (float_to_fp16 a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_mul mode a b))) ∧
        (∀mode b a.
           fp16_mul mode (float_to_fp16 a) (n2w b) =
           float_to_fp16 (SND (float_mul mode a (fp16_to_float (n2w b))))) ∧
        (∀mode b a.
           fp16_mul mode (n2w a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_mul mode (fp16_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp16_mul mode (n2w a) (n2w b) =
          float_to_fp16
            (SND
               (float_mul mode (fp16_to_float (n2w a))
                  (fp16_to_float (n2w b))))
   
   [fp16_mul_add]  Theorem
      
      ⊢ (∀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_add_with_flags]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_sub_with_flags]  Theorem
      
      ⊢ (∀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)))
   
   [fp16_mul_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp16_mul_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_mul mode a b)) ∧
        (∀mode b a.
           fp16_mul_with_flags mode (float_to_fp16 a) (n2w b) =
           (I ## float_to_fp16) (float_mul mode a (fp16_to_float (n2w b)))) ∧
        (∀mode b a.
           fp16_mul_with_flags mode (n2w a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_mul mode (fp16_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp16_mul_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp16)
            (float_mul mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b)))
   
   [fp16_nchotomy]  Theorem
      
      ⊢ ∀x. ∃y. x = float_to_fp16 y
   
   [fp16_negate]  Theorem
      
      ⊢ (∀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_roundToIntegral]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_sqrt_with_flags]  Theorem
      
      ⊢ (∀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_sub]  Theorem
      
      ⊢ (∀mode b a.
           fp16_sub mode (float_to_fp16 a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_sub mode a b))) ∧
        (∀mode b a.
           fp16_sub mode (float_to_fp16 a) (n2w b) =
           float_to_fp16 (SND (float_sub mode a (fp16_to_float (n2w b))))) ∧
        (∀mode b a.
           fp16_sub mode (n2w a) (float_to_fp16 b) =
           float_to_fp16 (SND (float_sub mode (fp16_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp16_sub mode (n2w a) (n2w b) =
          float_to_fp16
            (SND
               (float_sub mode (fp16_to_float (n2w a))
                  (fp16_to_float (n2w b))))
   
   [fp16_sub_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp16_sub_with_flags mode (float_to_fp16 a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_sub mode a b)) ∧
        (∀mode b a.
           fp16_sub_with_flags mode (float_to_fp16 a) (n2w b) =
           (I ## float_to_fp16) (float_sub mode a (fp16_to_float (n2w b)))) ∧
        (∀mode b a.
           fp16_sub_with_flags mode (n2w a) (float_to_fp16 b) =
           (I ## float_to_fp16) (float_sub mode (fp16_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp16_sub_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp16)
            (float_sub mode (fp16_to_float (n2w a)) (fp16_to_float (n2w b)))
   
   [fp16_to_float_11]  Theorem
      
      ⊢ ∀x y. fp16_to_float x = fp16_to_float y ⇔ x = y
   
   [fp16_to_float_float_to_fp16]  Theorem
      
      ⊢ ∀x. fp16_to_float (float_to_fp16 x) = x
   
   [fp16_to_float_n2w]  Theorem
      
      ⊢ ∀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_to_int]  Theorem
      
      ⊢ (∀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_to_real]  Theorem
      
      ⊢ (∀a. fp16_to_real (float_to_fp16 a) = float_to_real a) ∧
        ∀a. fp16_to_real (n2w a) = float_to_real (fp16_to_float (n2w a))
   
   [fp16_to_value]  Theorem
      
      ⊢ (∀a. fp16_to_value (float_to_fp16 a) = float_value a) ∧
        ∀a. fp16_to_value (n2w a) = float_value (fp16_to_float (n2w a))
   
   [fp32_abs]  Theorem
      
      ⊢ (∀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_add]  Theorem
      
      ⊢ (∀mode b a.
           fp32_add mode (float_to_fp32 a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_add mode a b))) ∧
        (∀mode b a.
           fp32_add mode (float_to_fp32 a) (n2w b) =
           float_to_fp32 (SND (float_add mode a (fp32_to_float (n2w b))))) ∧
        (∀mode b a.
           fp32_add mode (n2w a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_add mode (fp32_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp32_add mode (n2w a) (n2w b) =
          float_to_fp32
            (SND
               (float_add mode (fp32_to_float (n2w a))
                  (fp32_to_float (n2w b))))
   
   [fp32_add_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp32_add_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_add mode a b)) ∧
        (∀mode b a.
           fp32_add_with_flags mode (float_to_fp32 a) (n2w b) =
           (I ## float_to_fp32) (float_add mode a (fp32_to_float (n2w b)))) ∧
        (∀mode b a.
           fp32_add_with_flags mode (n2w a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_add mode (fp32_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp32_add_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp32)
            (float_add mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b)))
   
   [fp32_compare]  Theorem
      
      ⊢ (∀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_div]  Theorem
      
      ⊢ (∀mode b a.
           fp32_div mode (float_to_fp32 a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_div mode a b))) ∧
        (∀mode b a.
           fp32_div mode (float_to_fp32 a) (n2w b) =
           float_to_fp32 (SND (float_div mode a (fp32_to_float (n2w b))))) ∧
        (∀mode b a.
           fp32_div mode (n2w a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_div mode (fp32_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp32_div mode (n2w a) (n2w b) =
          float_to_fp32
            (SND
               (float_div mode (fp32_to_float (n2w a))
                  (fp32_to_float (n2w b))))
   
   [fp32_div_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp32_div_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_div mode a b)) ∧
        (∀mode b a.
           fp32_div_with_flags mode (float_to_fp32 a) (n2w b) =
           (I ## float_to_fp32) (float_div mode a (fp32_to_float (n2w b)))) ∧
        (∀mode b a.
           fp32_div_with_flags mode (n2w a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_div mode (fp32_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp32_div_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp32)
            (float_div mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b)))
   
   [fp32_equal]  Theorem
      
      ⊢ (∀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_greaterEqual]  Theorem
      
      ⊢ (∀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_greaterThan]  Theorem
      
      ⊢ (∀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_isFinite]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_isIntegral]  Theorem
      
      ⊢ (∀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_isNan]  Theorem
      
      ⊢ (∀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_isNormal]  Theorem
      
      ⊢ (∀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_isSignallingNan]  Theorem
      
      ⊢ (∀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_isSubnormal]  Theorem
      
      ⊢ (∀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_isZero]  Theorem
      
      ⊢ (∀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_lessEqual]  Theorem
      
      ⊢ (∀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_lessThan]  Theorem
      
      ⊢ (∀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_mul]  Theorem
      
      ⊢ (∀mode b a.
           fp32_mul mode (float_to_fp32 a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_mul mode a b))) ∧
        (∀mode b a.
           fp32_mul mode (float_to_fp32 a) (n2w b) =
           float_to_fp32 (SND (float_mul mode a (fp32_to_float (n2w b))))) ∧
        (∀mode b a.
           fp32_mul mode (n2w a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_mul mode (fp32_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp32_mul mode (n2w a) (n2w b) =
          float_to_fp32
            (SND
               (float_mul mode (fp32_to_float (n2w a))
                  (fp32_to_float (n2w b))))
   
   [fp32_mul_add]  Theorem
      
      ⊢ (∀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_add_with_flags]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_sub_with_flags]  Theorem
      
      ⊢ (∀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)))
   
   [fp32_mul_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp32_mul_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_mul mode a b)) ∧
        (∀mode b a.
           fp32_mul_with_flags mode (float_to_fp32 a) (n2w b) =
           (I ## float_to_fp32) (float_mul mode a (fp32_to_float (n2w b)))) ∧
        (∀mode b a.
           fp32_mul_with_flags mode (n2w a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_mul mode (fp32_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp32_mul_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp32)
            (float_mul mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b)))
   
   [fp32_nchotomy]  Theorem
      
      ⊢ ∀x. ∃y. x = float_to_fp32 y
   
   [fp32_negate]  Theorem
      
      ⊢ (∀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_roundToIntegral]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_sqrt_with_flags]  Theorem
      
      ⊢ (∀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_sub]  Theorem
      
      ⊢ (∀mode b a.
           fp32_sub mode (float_to_fp32 a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_sub mode a b))) ∧
        (∀mode b a.
           fp32_sub mode (float_to_fp32 a) (n2w b) =
           float_to_fp32 (SND (float_sub mode a (fp32_to_float (n2w b))))) ∧
        (∀mode b a.
           fp32_sub mode (n2w a) (float_to_fp32 b) =
           float_to_fp32 (SND (float_sub mode (fp32_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp32_sub mode (n2w a) (n2w b) =
          float_to_fp32
            (SND
               (float_sub mode (fp32_to_float (n2w a))
                  (fp32_to_float (n2w b))))
   
   [fp32_sub_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp32_sub_with_flags mode (float_to_fp32 a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_sub mode a b)) ∧
        (∀mode b a.
           fp32_sub_with_flags mode (float_to_fp32 a) (n2w b) =
           (I ## float_to_fp32) (float_sub mode a (fp32_to_float (n2w b)))) ∧
        (∀mode b a.
           fp32_sub_with_flags mode (n2w a) (float_to_fp32 b) =
           (I ## float_to_fp32) (float_sub mode (fp32_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp32_sub_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp32)
            (float_sub mode (fp32_to_float (n2w a)) (fp32_to_float (n2w b)))
   
   [fp32_to_float_11]  Theorem
      
      ⊢ ∀x y. fp32_to_float x = fp32_to_float y ⇔ x = y
   
   [fp32_to_float_float_to_fp32]  Theorem
      
      ⊢ ∀x. fp32_to_float (float_to_fp32 x) = x
   
   [fp32_to_float_n2w]  Theorem
      
      ⊢ ∀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_to_int]  Theorem
      
      ⊢ (∀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_to_real]  Theorem
      
      ⊢ (∀a. fp32_to_real (float_to_fp32 a) = float_to_real a) ∧
        ∀a. fp32_to_real (n2w a) = float_to_real (fp32_to_float (n2w a))
   
   [fp32_to_value]  Theorem
      
      ⊢ (∀a. fp32_to_value (float_to_fp32 a) = float_value a) ∧
        ∀a. fp32_to_value (n2w a) = float_value (fp32_to_float (n2w a))
   
   [fp64_abs]  Theorem
      
      ⊢ (∀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_add]  Theorem
      
      ⊢ (∀mode b a.
           fp64_add mode (float_to_fp64 a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_add mode a b))) ∧
        (∀mode b a.
           fp64_add mode (float_to_fp64 a) (n2w b) =
           float_to_fp64 (SND (float_add mode a (fp64_to_float (n2w b))))) ∧
        (∀mode b a.
           fp64_add mode (n2w a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_add mode (fp64_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp64_add mode (n2w a) (n2w b) =
          float_to_fp64
            (SND
               (float_add mode (fp64_to_float (n2w a))
                  (fp64_to_float (n2w b))))
   
   [fp64_add_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp64_add_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_add mode a b)) ∧
        (∀mode b a.
           fp64_add_with_flags mode (float_to_fp64 a) (n2w b) =
           (I ## float_to_fp64) (float_add mode a (fp64_to_float (n2w b)))) ∧
        (∀mode b a.
           fp64_add_with_flags mode (n2w a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_add mode (fp64_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp64_add_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp64)
            (float_add mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b)))
   
   [fp64_compare]  Theorem
      
      ⊢ (∀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_div]  Theorem
      
      ⊢ (∀mode b a.
           fp64_div mode (float_to_fp64 a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_div mode a b))) ∧
        (∀mode b a.
           fp64_div mode (float_to_fp64 a) (n2w b) =
           float_to_fp64 (SND (float_div mode a (fp64_to_float (n2w b))))) ∧
        (∀mode b a.
           fp64_div mode (n2w a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_div mode (fp64_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp64_div mode (n2w a) (n2w b) =
          float_to_fp64
            (SND
               (float_div mode (fp64_to_float (n2w a))
                  (fp64_to_float (n2w b))))
   
   [fp64_div_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp64_div_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_div mode a b)) ∧
        (∀mode b a.
           fp64_div_with_flags mode (float_to_fp64 a) (n2w b) =
           (I ## float_to_fp64) (float_div mode a (fp64_to_float (n2w b)))) ∧
        (∀mode b a.
           fp64_div_with_flags mode (n2w a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_div mode (fp64_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp64_div_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp64)
            (float_div mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b)))
   
   [fp64_equal]  Theorem
      
      ⊢ (∀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_greaterEqual]  Theorem
      
      ⊢ (∀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_greaterThan]  Theorem
      
      ⊢ (∀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_isFinite]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_isIntegral]  Theorem
      
      ⊢ (∀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_isNan]  Theorem
      
      ⊢ (∀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_isNormal]  Theorem
      
      ⊢ (∀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_isSignallingNan]  Theorem
      
      ⊢ (∀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_isSubnormal]  Theorem
      
      ⊢ (∀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_isZero]  Theorem
      
      ⊢ (∀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_lessEqual]  Theorem
      
      ⊢ (∀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_lessThan]  Theorem
      
      ⊢ (∀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_mul]  Theorem
      
      ⊢ (∀mode b a.
           fp64_mul mode (float_to_fp64 a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_mul mode a b))) ∧
        (∀mode b a.
           fp64_mul mode (float_to_fp64 a) (n2w b) =
           float_to_fp64 (SND (float_mul mode a (fp64_to_float (n2w b))))) ∧
        (∀mode b a.
           fp64_mul mode (n2w a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_mul mode (fp64_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp64_mul mode (n2w a) (n2w b) =
          float_to_fp64
            (SND
               (float_mul mode (fp64_to_float (n2w a))
                  (fp64_to_float (n2w b))))
   
   [fp64_mul_add]  Theorem
      
      ⊢ (∀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_add_with_flags]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_sub_with_flags]  Theorem
      
      ⊢ (∀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)))
   
   [fp64_mul_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp64_mul_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_mul mode a b)) ∧
        (∀mode b a.
           fp64_mul_with_flags mode (float_to_fp64 a) (n2w b) =
           (I ## float_to_fp64) (float_mul mode a (fp64_to_float (n2w b)))) ∧
        (∀mode b a.
           fp64_mul_with_flags mode (n2w a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_mul mode (fp64_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp64_mul_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp64)
            (float_mul mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b)))
   
   [fp64_nchotomy]  Theorem
      
      ⊢ ∀x. ∃y. x = float_to_fp64 y
   
   [fp64_negate]  Theorem
      
      ⊢ (∀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_roundToIntegral]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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_sqrt_with_flags]  Theorem
      
      ⊢ (∀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_sub]  Theorem
      
      ⊢ (∀mode b a.
           fp64_sub mode (float_to_fp64 a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_sub mode a b))) ∧
        (∀mode b a.
           fp64_sub mode (float_to_fp64 a) (n2w b) =
           float_to_fp64 (SND (float_sub mode a (fp64_to_float (n2w b))))) ∧
        (∀mode b a.
           fp64_sub mode (n2w a) (float_to_fp64 b) =
           float_to_fp64 (SND (float_sub mode (fp64_to_float (n2w a)) b))) ∧
        ∀mode b a.
          fp64_sub mode (n2w a) (n2w b) =
          float_to_fp64
            (SND
               (float_sub mode (fp64_to_float (n2w a))
                  (fp64_to_float (n2w b))))
   
   [fp64_sub_with_flags]  Theorem
      
      ⊢ (∀mode b a.
           fp64_sub_with_flags mode (float_to_fp64 a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_sub mode a b)) ∧
        (∀mode b a.
           fp64_sub_with_flags mode (float_to_fp64 a) (n2w b) =
           (I ## float_to_fp64) (float_sub mode a (fp64_to_float (n2w b)))) ∧
        (∀mode b a.
           fp64_sub_with_flags mode (n2w a) (float_to_fp64 b) =
           (I ## float_to_fp64) (float_sub mode (fp64_to_float (n2w a)) b)) ∧
        ∀mode b a.
          fp64_sub_with_flags mode (n2w a) (n2w b) =
          (I ## float_to_fp64)
            (float_sub mode (fp64_to_float (n2w a)) (fp64_to_float (n2w b)))
   
   [fp64_to_float_11]  Theorem
      
      ⊢ ∀x y. fp64_to_float x = fp64_to_float y ⇔ x = y
   
   [fp64_to_float_float_to_fp64]  Theorem
      
      ⊢ ∀x. fp64_to_float (float_to_fp64 x) = x
   
   [fp64_to_float_n2w]  Theorem
      
      ⊢ ∀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_to_int]  Theorem
      
      ⊢ (∀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_to_real]  Theorem
      
      ⊢ (∀a. fp64_to_real (float_to_fp64 a) = float_to_real a) ∧
        ∀a. fp64_to_real (n2w a) = float_to_real (fp64_to_float (n2w a))
   
   [fp64_to_value]  Theorem
      
      ⊢ (∀a. fp64_to_value (float_to_fp64 a) = float_value a) ∧
        ∀a. fp64_to_value (n2w a) = float_value (fp64_to_float (n2w a))
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14