Structure binary_ieeeTheory


Source File Identifier index Theory binding index

signature binary_ieeeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ULP_def_primitive : thm
    val check_for_signalling_def : thm
    val clear_flags_def : thm
    val closest_def : thm
    val closest_such_def : thm
    val dividezero_flags_def : thm
    val exponent_boundary_def : thm
    val flags_TY_DEF : thm
    val flags_case_def : thm
    val flags_size_def : thm
    val float_TY_DEF : thm
    val float_abs_def : thm
    val float_add_def : thm
    val float_bottom_def : thm
    val float_case_def : thm
    val float_compare_BIJ : thm
    val float_compare_CASE : thm
    val float_compare_TY_DEF : thm
    val float_compare_def : thm
    val float_compare_size_def : thm
    val float_div_def : thm
    val float_equal_def : thm
    val float_greater_equal_def : thm
    val float_greater_than_def : thm
    val float_is_finite_def : thm
    val float_is_infinite_def : thm
    val float_is_integral_def : thm
    val float_is_nan_def : thm
    val float_is_normal_def : thm
    val float_is_signalling_def : thm
    val float_is_subnormal_def : thm
    val float_is_zero_def : thm
    val float_less_equal_def : thm
    val float_less_than_def : thm
    val float_minus_infinity_def : thm
    val float_minus_min_def : thm
    val float_minus_zero_def : thm
    val float_mul_add_def : thm
    val float_mul_def : thm
    val float_mul_sub_def : thm
    val float_negate_def : thm
    val float_plus_infinity_def : thm
    val float_plus_min_def : thm
    val float_plus_zero_def : thm
    val float_round_def : thm
    val float_round_to_integral_def : thm
    val float_round_with_flags_def : thm
    val float_size_def : thm
    val float_some_qnan_def : thm
    val float_sqrt_def : thm
    val float_sub_def : thm
    val float_to_int_def : thm
    val float_to_real_def : thm
    val float_top_def : thm
    val float_unordered_def : thm
    val float_value_TY_DEF : thm
    val float_value_case_def : thm
    val float_value_def : thm
    val float_value_size_def : thm
    val fp_op_TY_DEF : thm
    val fp_op_case_def : thm
    val fp_op_size_def : thm
    val integral_round_def : thm
    val invalidop_flags_def : thm
    val is_closest_def : thm
    val is_integral_def : thm
    val largest_def : thm
    val real_to_float_def : thm
    val real_to_float_with_flags_def : thm
    val recordtype_flags_seldef_DivideByZero_def : thm
    val recordtype_flags_seldef_DivideByZero_fupd_def : thm
    val recordtype_flags_seldef_InvalidOp_def : thm
    val recordtype_flags_seldef_InvalidOp_fupd_def : thm
    val recordtype_flags_seldef_Overflow_def : thm
    val recordtype_flags_seldef_Overflow_fupd_def : thm
    val recordtype_flags_seldef_Precision_def : thm
    val recordtype_flags_seldef_Precision_fupd_def : thm
    val recordtype_flags_seldef_Underflow_AfterRounding_def : thm
    val recordtype_flags_seldef_Underflow_AfterRounding_fupd_def : thm
    val recordtype_flags_seldef_Underflow_BeforeRounding_def : thm
    val recordtype_flags_seldef_Underflow_BeforeRounding_fupd_def : thm
    val recordtype_float_seldef_Exponent_def : thm
    val recordtype_float_seldef_Exponent_fupd_def : thm
    val recordtype_float_seldef_Sign_def : thm
    val recordtype_float_seldef_Sign_fupd_def : thm
    val recordtype_float_seldef_Significand_def : thm
    val recordtype_float_seldef_Significand_fupd_def : thm
    val round_def : thm
    val rounding_BIJ : thm
    val rounding_CASE : thm
    val rounding_TY_DEF : thm
    val rounding_size_def : thm
    val threshold_def : thm
    val ulp_def : thm
  
  (*  Theorems  *)
    val EXISTS_flags : thm
    val EXISTS_float : thm
    val FINITE_floatsets : thm
    val FORALL_flags : thm
    val FORALL_float : thm
    val NMUL_EQ_2 : thm
    val ULP_def : thm
    val ULP_ind : thm
    val ULP_le_mono : thm
    val ULP_nonzero : thm
    val ULP_positive : thm
    val abs_float_value : thm
    val bottom_properties : thm
    val datatype_flags : thm
    val datatype_float : thm
    val datatype_float_compare : thm
    val datatype_float_value : thm
    val datatype_fp_op : thm
    val datatype_rounding : thm
    val diff_float_ULP : thm
    val diff_lt_ulp_eq0 : thm
    val diff_lt_ulp_even : thm
    val diff_lt_ulp_even4 : thm
    val div_eq0 : thm
    val exp_ge2 : thm
    val exp_gt2 : thm
    val flags_11 : thm
    val flags_Axiom : thm
    val flags_accessors : thm
    val flags_accfupds : thm
    val flags_case_cong : thm
    val flags_case_eq : thm
    val flags_component_equality : thm
    val flags_fn_updates : thm
    val flags_fupdcanon : thm
    val flags_fupdcanon_comp : thm
    val flags_fupdfupds : thm
    val flags_fupdfupds_comp : thm
    val flags_induction : thm
    val flags_literal_11 : thm
    val flags_literal_nchotomy : thm
    val flags_nchotomy : thm
    val flags_updates_eq_literal : thm
    val float_11 : thm
    val float_Axiom : thm
    val float_accessors : thm
    val float_accfupds : thm
    val float_add_compute : thm
    val float_add_finite : thm
    val float_add_finite_minus_infinity : thm
    val float_add_finite_plus_infinity : thm
    val float_add_minus_infinity_finite : thm
    val float_add_nan : thm
    val float_add_plus_infinity_finite : thm
    val float_case_cong : thm
    val float_case_eq : thm
    val float_cases : thm
    val float_cases_finite : thm
    val float_compare2num_11 : thm
    val float_compare2num_ONTO : thm
    val float_compare2num_num2float_compare : thm
    val float_compare2num_thm : thm
    val float_compare_Axiom : thm
    val float_compare_EQ_float_compare : thm
    val float_compare_case_cong : thm
    val float_compare_case_def : thm
    val float_compare_case_eq : thm
    val float_compare_distinct : thm
    val float_compare_induction : thm
    val float_compare_nchotomy : thm
    val float_component_equality : thm
    val float_components : thm
    val float_distinct : thm
    val float_distinct_finite : thm
    val float_div_compute : thm
    val float_div_finite : thm
    val float_div_finite_minus_infinity : thm
    val float_div_finite_plus_infinity : thm
    val float_div_minus_infinity_finite : thm
    val float_div_nan : thm
    val float_div_plus_infinity_finite : thm
    val float_fn_updates : thm
    val float_fupdcanon : thm
    val float_fupdcanon_comp : thm
    val float_fupdfupds : thm
    val float_fupdfupds_comp : thm
    val float_induction : thm
    val float_infinities : thm
    val float_infinities_distinct : thm
    val float_infinity_negate_abs : thm
    val float_is_distinct : thm
    val float_is_finite : thm
    val float_is_nan_impl : thm
    val float_is_zero : thm
    val float_is_zero_impl : thm
    val float_is_zero_to_real : thm
    val float_literal_11 : thm
    val float_literal_nchotomy : thm
    val float_minus_infinity : thm
    val float_minus_zero : thm
    val float_mul_compute : thm
    val float_mul_finite : thm
    val float_mul_finite_minus_infinity : thm
    val float_mul_finite_plus_infinity : thm
    val float_mul_minus_infinity_finite : thm
    val float_mul_nan : thm
    val float_mul_plus_infinity_finite : thm
    val float_nchotomy : thm
    val float_negate_negate : thm
    val float_round_bottom : thm
    val float_round_minus_infinity : thm
    val float_round_non_zero : thm
    val float_round_plus_infinity : thm
    val float_round_roundTowardNegative_minus_infinity : thm
    val float_round_roundTowardNegative_top : thm
    val float_round_roundTowardPositive_bottom : thm
    val float_round_roundTowardPositive_plus_infinity : thm
    val float_round_roundTowardZero_bottom : thm
    val float_round_roundTowardZero_top : thm
    val float_round_to_integral_compute : thm
    val float_round_top : thm
    val float_sets : thm
    val float_sub_compute : thm
    val float_sub_finite : thm
    val float_sub_finite_minus_infinity : thm
    val float_sub_finite_plus_infinity : thm
    val float_sub_minus_infinity_finite : thm
    val float_sub_nan : thm
    val float_sub_plus_infinity_finite : thm
    val float_tests : thm
    val float_to_real : thm
    val float_to_real_EQ0 : thm
    val float_to_real_eq : thm
    val float_to_real_negate : thm
    val float_to_real_round0 : thm
    val float_to_real_zeroes : thm
    val float_updates_eq_literal : thm
    val float_value_11 : thm
    val float_value_Axiom : thm
    val float_value_case_cong : thm
    val float_value_case_eq : thm
    val float_value_distinct : thm
    val float_value_induction : thm
    val float_value_nchotomy : thm
    val float_values : thm
    val fp_op_11 : thm
    val fp_op_Axiom : thm
    val fp_op_case_cong : thm
    val fp_op_case_eq : thm
    val fp_op_distinct : thm
    val fp_op_induction : thm
    val fp_op_nchotomy : thm
    val infinity_properties : thm
    val is_closestP_finite_float_exists : thm
    val is_closest_exists : thm
    val is_closest_finite_AND : thm
    val is_closest_float_is_finite_0 : thm
    val largest : thm
    val largest_is_positive : thm
    val largest_is_top : thm
    val largest_lt_threshold : thm
    val le2 : thm
    val less_than_ulp : thm
    val min_properties : thm
    val neg_ulp : thm
    val num2float_compare_11 : thm
    val num2float_compare_ONTO : thm
    val num2float_compare_float_compare2num : thm
    val num2float_compare_thm : thm
    val num2rounding_11 : thm
    val num2rounding_ONTO : thm
    val num2rounding_rounding2num : thm
    val num2rounding_thm : thm
    val round_roundTiesToEven : thm
    val round_roundTiesToEven0 : thm
    val round_roundTiesToEven_is_minus_zero : thm
    val round_roundTiesToEven_is_plus_zero : thm
    val round_roundTiesToEven_is_zero : thm
    val round_roundTiesToEven_minus_infinity : thm
    val round_roundTiesToEven_plus_infinity : thm
    val round_roundTowardNegative_minus_infinity : thm
    val round_roundTowardNegative_top : thm
    val round_roundTowardPositive_bottom : thm
    val round_roundTowardPositive_plus_infinity : thm
    val round_roundTowardZero : thm
    val round_roundTowardZero_bottom : thm
    val round_roundTowardZero_is_minus_zero : thm
    val round_roundTowardZero_is_plus_zero : thm
    val round_roundTowardZero_is_zero : thm
    val round_roundTowardZero_top : thm
    val rounding2num_11 : thm
    val rounding2num_ONTO : thm
    val rounding2num_num2rounding : thm
    val rounding2num_thm : thm
    val rounding_Axiom : thm
    val rounding_EQ_rounding : thm
    val rounding_case_cong : thm
    val rounding_case_def : thm
    val rounding_case_eq : thm
    val rounding_distinct : thm
    val rounding_induction : thm
    val rounding_nchotomy : thm
    val sign_not_zero : thm
    val some_nan_properties : thm
    val threshold : thm
    val threshold_is_positive : thm
    val top_properties : thm
    val ulp : thm
    val ulp_lt_ULP : thm
    val ulp_lt_largest : thm
    val ulp_lt_threshold : thm
    val ulp_nonzero : thm
    val ulp_positive : thm
    val zero_le_pos_div_twopow : thm
    val zero_le_twopow : thm
    val zero_lt_twopow : thm
    val zero_neq_twopow : thm
    val zero_properties : thm
    val zero_to_real : thm
    val zeroes_are_finite_floats : thm
  
  val binary_ieee_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [intreal] Parent theory of "binary_ieee"
   
   [set_relation] Parent theory of "binary_ieee"
   
   [words] Parent theory of "binary_ieee"
   
   [ULP_def_primitive]  Definition
      
      ⊢ ULP =
        WFREC (@R. WF R)
          (λULP a.
               case a of
                 (v,v1) =>
                   I
                     (2 pow (if v = 0w then 1 else w2n v) /
                      2 pow (bias (:χ) + precision (:τ))))
   
   [check_for_signalling_def]  Definition
      
      ⊢ ∀l. check_for_signalling l =
            clear_flags with InvalidOp := EXISTS float_is_signalling l
   
   [clear_flags_def]  Definition
      
      ⊢ clear_flags =
        <|DivideByZero := F; InvalidOp := F; Overflow := F; Precision := F;
          Underflow_BeforeRounding := F; Underflow_AfterRounding := F|>
   
   [closest_def]  Definition
      
      ⊢ closest = closest_such (K T)
   
   [closest_such_def]  Definition
      
      ⊢ ∀p s x.
          closest_such p s x =
          @a. is_closest s x a ∧ ∀b. is_closest s x b ∧ p b ⇒ p a
   
   [dividezero_flags_def]  Definition
      
      ⊢ dividezero_flags = clear_flags with DivideByZero := T
   
   [exponent_boundary_def]  Definition
      
      ⊢ ∀y x.
          exponent_boundary y x ⇔
          x.Sign = y.Sign ∧ w2n x.Exponent = w2n y.Exponent + 1 ∧
          x.Exponent ≠ 1w ∧ y.Significand = -1w ∧ x.Significand = 0w
   
   [flags_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('flags').
                   (∀a0'.
                      (∃a0 a1 a2 a3 a4 a5.
                         a0' =
                         (λa0 a1 a2 a3 a4 a5.
                              ind_type$CONSTR 0 (a0,a1,a2,a3,a4,a5)
                                (λn. ind_type$BOTTOM)) a0 a1 a2 a3 a4 a5) ⇒
                      $var$('flags') a0') ⇒
                   $var$('flags') a0') rep
   
   [flags_case_def]  Definition
      
      ⊢ ∀a0 a1 a2 a3 a4 a5 f.
          flags_CASE (flags a0 a1 a2 a3 a4 a5) f = f a0 a1 a2 a3 a4 a5
   
   [flags_size_def]  Definition
      
      ⊢ ∀a0 a1 a2 a3 a4 a5.
          flags_size (flags a0 a1 a2 a3 a4 a5) =
          1 +
          (bool_size a0 +
           (bool_size a1 +
            (bool_size a2 + (bool_size a3 + (bool_size a4 + bool_size a5)))))
   
   [float_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('float').
                   (∀a0'.
                      (∃a0 a1 a2.
                         a0' =
                         (λa0 a1 a2.
                              ind_type$CONSTR 0 (a0,a1,a2)
                                (λn. ind_type$BOTTOM)) a0 a1 a2) ⇒
                      $var$('float') a0') ⇒
                   $var$('float') a0') rep
   
   [float_abs_def]  Definition
      
      ⊢ ∀x. float_abs x = x with Sign := 0w
   
   [float_add_def]  Definition
      
      ⊢ ∀mode x y.
          float_add mode x y =
          case (float_value x,float_value y) of
            (Float r1,Float r2) =>
              float_round_with_flags mode
                (if r1 = 0 ∧ r2 = 0 ∧ x.Sign = y.Sign then x.Sign = 1w
                 else (mode = roundTowardNegative)) (r1 + r2)
          | (Float r1,Infinity) => (clear_flags,y)
          | (Float r1,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Add mode x y))
          | (Infinity,Float v7) => (clear_flags,x)
          | (Infinity,Infinity) =>
            if x.Sign = y.Sign then (clear_flags,x)
            else (invalidop_flags,float_some_qnan (FP_Add mode x y))
          | (Infinity,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Add mode x y))
          | (NaN,v1) =>
            (check_for_signalling [x; y],float_some_qnan (FP_Add mode x y))
   
   [float_bottom_def]  Definition
      
      ⊢ float_bottom (:τ # χ) = float_negate (float_top (:τ # χ))
   
   [float_case_def]  Definition
      
      ⊢ ∀a0 a1 a2 f. float_CASE (float a0 a1 a2) f = f a0 a1 a2
   
   [float_compare_BIJ]  Definition
      
      ⊢ (∀a. num2float_compare (float_compare2num a) = a) ∧
        ∀r. (λn. n < 4) r ⇔ float_compare2num (num2float_compare r) = r
   
   [float_compare_CASE]  Definition
      
      ⊢ ∀x v0 v1 v2 v3.
          (case x of LT => v0 | EQ => v1 | GT => v2 | UN => v3) =
          (λm.
               if m < 1 then v0
               else if m < 2 then v1
               else if m = 2 then v2
               else v3) (float_compare2num x)
   
   [float_compare_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep
   
   [float_compare_def]  Definition
      
      ⊢ ∀x y.
          float_compare x y =
          case (float_value x,float_value y) of
            (Float r1,Float r2) =>
              if r1 < r2 then LT else if r1 = r2 then EQ else GT
          | (Float r1,Infinity) => if y.Sign = 1w then GT else LT
          | (Float r1,NaN) => UN
          | (Infinity,Float v7) => if x.Sign = 1w then LT else GT
          | (Infinity,Infinity) =>
            if x.Sign = y.Sign then EQ else if x.Sign = 1w then LT else GT
          | (Infinity,NaN) => UN
          | (NaN,v1) => UN
   
   [float_compare_size_def]  Definition
      
      ⊢ ∀x. float_compare_size x = 0
   
   [float_div_def]  Definition
      
      ⊢ ∀mode x y.
          float_div mode x y =
          case (float_value x,float_value y) of
            (Float 0,Float 0) =>
              (invalidop_flags,float_some_qnan (FP_Div mode x y))
          | (Float r1,Float 0) =>
            (dividezero_flags,
             if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
          | (Float r1,Float r2) =>
            float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 / r2)
          | (Float r1,Infinity) =>
            (clear_flags,if x.Sign = y.Sign then POS0 else NEG0)
          | (Float r1,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Div mode x y))
          | (Infinity,Float v7) =>
            (clear_flags,
             if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
          | (Infinity,Infinity) =>
            (invalidop_flags,float_some_qnan (FP_Div mode x y))
          | (Infinity,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Div mode x y))
          | (NaN,v1) =>
            (check_for_signalling [x; y],float_some_qnan (FP_Div mode x y))
   
   [float_equal_def]  Definition
      
      ⊢ ∀x y. float_equal x y ⇔ float_compare x y = EQ
   
   [float_greater_equal_def]  Definition
      
      ⊢ ∀x y.
          float_greater_equal x y ⇔
          case float_compare x y of LT => F | EQ => T | GT => T | UN => F
   
   [float_greater_than_def]  Definition
      
      ⊢ ∀x y. float_greater_than x y ⇔ float_compare x y = GT
   
   [float_is_finite_def]  Definition
      
      ⊢ ∀x. float_is_finite x ⇔
            case float_value x of Float v1 => T | Infinity => F | NaN => F
   
   [float_is_infinite_def]  Definition
      
      ⊢ ∀x. float_is_infinite x ⇔
            case float_value x of Float v1 => F | Infinity => T | NaN => F
   
   [float_is_integral_def]  Definition
      
      ⊢ ∀x. float_is_integral x ⇔
            case float_value x of
              Float r => is_integral r
            | Infinity => F
            | NaN => F
   
   [float_is_nan_def]  Definition
      
      ⊢ ∀x. float_is_nan x ⇔
            case float_value x of Float v1 => F | Infinity => F | NaN => T
   
   [float_is_normal_def]  Definition
      
      ⊢ ∀x. float_is_normal x ⇔ x.Exponent ≠ 0w ∧ x.Exponent ≠ UINT_MAXw
   
   [float_is_signalling_def]  Definition
      
      ⊢ ∀x. float_is_signalling x ⇔
            float_is_nan x ∧ ¬word_msb x.Significand
   
   [float_is_subnormal_def]  Definition
      
      ⊢ ∀x. float_is_subnormal x ⇔ x.Exponent = 0w ∧ x.Significand ≠ 0w
   
   [float_is_zero_def]  Definition
      
      ⊢ ∀x. float_is_zero x ⇔
            case float_value x of
              Float r => r = 0
            | Infinity => F
            | NaN => F
   
   [float_less_equal_def]  Definition
      
      ⊢ ∀x y.
          float_less_equal x y ⇔
          case float_compare x y of LT => T | EQ => T | GT => F | UN => F
   
   [float_less_than_def]  Definition
      
      ⊢ ∀x y. float_less_than x y ⇔ float_compare x y = LT
   
   [float_minus_infinity_def]  Definition
      
      ⊢ float_minus_infinity (:τ # χ) =
        float_negate (float_plus_infinity (:τ # χ))
   
   [float_minus_min_def]  Definition
      
      ⊢ float_minus_min (:τ # χ) = float_negate (float_plus_min (:τ # χ))
   
   [float_minus_zero_def]  Definition
      
      ⊢ NEG0 = float_negate POS0
   
   [float_mul_add_def]  Definition
      
      ⊢ ∀mode x y z.
          float_mul_add mode x y z =
          (let
             signP = x.Sign ⊕ y.Sign;
             infP = (float_is_infinite x ∨ float_is_infinite y)
           in
             if float_is_nan x ∨ float_is_nan y ∨ float_is_nan z then
               (check_for_signalling [x; y; z],
                float_some_qnan (FP_MulAdd mode x y z))
             else if
               float_is_infinite x ∧ float_is_zero y ∨
               float_is_zero x ∧ float_is_infinite y ∨
               float_is_infinite z ∧ infP ∧ signP ≠ z.Sign
             then
               (invalidop_flags,float_some_qnan (FP_MulAdd mode x y z))
             else if
               float_is_infinite z ∧ z.Sign = 0w ∨ infP ∧ signP = 0w
             then
               (clear_flags,float_plus_infinity (:τ # χ))
             else if
               float_is_infinite z ∧ z.Sign = 1w ∨ infP ∧ signP = 1w
             then
               (clear_flags,float_minus_infinity (:τ # χ))
             else
               (let
                  r1 = float_to_real x * float_to_real y;
                  r2 = float_to_real z;
                  r = r1 + r2
                in
                  float_round_with_flags mode
                    (r = 0 ∧
                     (if r1 = 0 ∧ r2 = 0 ∧ signP = z.Sign then signP = 1w
                      else mode = roundTowardNegative) ∨ r < 0) r))
   
   [float_mul_def]  Definition
      
      ⊢ ∀mode x y.
          float_mul mode x y =
          case (float_value x,float_value y) of
            (Float r',Float r2) =>
              float_round_with_flags mode (x.Sign ≠ y.Sign) (r' * r2)
          | (Float 0,Infinity) =>
            (invalidop_flags,float_some_qnan (FP_Mul mode x y))
          | (Float r',Infinity) =>
            (clear_flags,
             if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
          | (Float r',NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Mul mode x y))
          | (Infinity,Float 0) =>
            (invalidop_flags,float_some_qnan (FP_Mul mode x y))
          | (Infinity,Float r) =>
            (clear_flags,
             if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
          | (Infinity,Infinity) =>
            (clear_flags,
             if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
          | (Infinity,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Mul mode x y))
          | (NaN,v1) =>
            (check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y))
   
   [float_mul_sub_def]  Definition
      
      ⊢ ∀mode x y z.
          float_mul_sub mode x y z =
          (let
             signP = x.Sign ⊕ y.Sign;
             infP = (float_is_infinite x ∨ float_is_infinite y)
           in
             if float_is_nan x ∨ float_is_nan y ∨ float_is_nan z then
               (check_for_signalling [x; y; z],
                float_some_qnan (FP_MulSub mode x y z))
             else if
               float_is_infinite x ∧ float_is_zero y ∨
               float_is_zero x ∧ float_is_infinite y ∨
               float_is_infinite z ∧ infP ∧ signP = z.Sign
             then
               (invalidop_flags,float_some_qnan (FP_MulAdd mode x y z))
             else if
               float_is_infinite z ∧ z.Sign = 1w ∨ infP ∧ signP = 0w
             then
               (clear_flags,float_plus_infinity (:τ # χ))
             else if
               float_is_infinite z ∧ z.Sign = 0w ∨ infP ∧ signP = 1w
             then
               (clear_flags,float_minus_infinity (:τ # χ))
             else
               (let
                  r1 = float_to_real x * float_to_real y and
                  r2 = float_to_real z
                in
                  float_round_with_flags mode
                    (if r1 = 0 ∧ r2 = 0 ∧ signP ≠ z.Sign then signP = 1w
                     else (mode = roundTowardNegative)) (r1 − r2)))
   
   [float_negate_def]  Definition
      
      ⊢ ∀x. float_negate x = x with Sign := ¬x.Sign
   
   [float_plus_infinity_def]  Definition
      
      ⊢ float_plus_infinity (:τ # χ) =
        <|Sign := 0w; Exponent := UINT_MAXw; Significand := 0w|>
   
   [float_plus_min_def]  Definition
      
      ⊢ float_plus_min (:τ # χ) =
        <|Sign := 0w; Exponent := 0w; Significand := 1w|>
   
   [float_plus_zero_def]  Definition
      
      ⊢ POS0 = <|Sign := 0w; Exponent := 0w; Significand := 0w|>
   
   [float_round_def]  Definition
      
      ⊢ ∀mode toneg r.
          float_round mode toneg r =
          (let
             x = round mode r
           in
             if float_is_zero x then if toneg then NEG0 else POS0 else x)
   
   [float_round_to_integral_def]  Definition
      
      ⊢ ∀mode x.
          float_round_to_integral mode x =
          case float_value x of
            Float r => integral_round mode r
          | Infinity => x
          | NaN => x
   
   [float_round_with_flags_def]  Definition
      
      ⊢ ∀mode to_neg r.
          float_round_with_flags mode to_neg r =
          (let
             x = float_round mode to_neg r and a = abs r;
             inexact = (float_value x ≠ Float r)
           in
             (clear_flags with
              <|Overflow := (float_is_infinite x ∨ 2 pow INT_MIN (:χ) ≤ a);
                Underflow_BeforeRounding :=
                  (inexact ∧ a < 2 / 2 pow bias (:χ));
                Underflow_AfterRounding :=
                  (inexact ∧
                   (float_round mode to_neg r).Exponent ≤₊
                   n2w (INT_MIN (:χ))); Precision := inexact|>,x))
   
   [float_size_def]  Definition
      
      ⊢ ∀f f1 a0 a1 a2.
          float_size f f1 (float a0 a1 a2) =
          1 + (w2n a0 + (w2n a1 + w2n a2))
   
   [float_some_qnan_def]  Definition
      
      ⊢ ∀fp_op.
          float_some_qnan fp_op =
          (@f. (let
                  qnan = f fp_op
                in
                  float_is_nan qnan ∧ ¬float_is_signalling qnan)) fp_op
   
   [float_sqrt_def]  Definition
      
      ⊢ ∀mode x.
          float_sqrt mode x =
          if x.Sign = 0w then
            case float_value x of
              Float r => float_round_with_flags mode F (sqrt r)
            | Infinity => (clear_flags,float_plus_infinity (:τ # χ))
            | NaN =>
              (check_for_signalling [x],float_some_qnan (FP_Sqrt mode x))
          else if x = NEG0 then (clear_flags,NEG0)
          else (invalidop_flags,float_some_qnan (FP_Sqrt mode x))
   
   [float_sub_def]  Definition
      
      ⊢ ∀mode x y.
          float_sub mode x y =
          case (float_value x,float_value y) of
            (Float r1,Float r2) =>
              float_round_with_flags mode
                (if r1 = 0 ∧ r2 = 0 ∧ x.Sign ≠ y.Sign then x.Sign = 1w
                 else (mode = roundTowardNegative)) (r1 − r2)
          | (Float r1,Infinity) => (clear_flags,float_negate y)
          | (Float r1,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Sub mode x y))
          | (Infinity,Float v7) => (clear_flags,x)
          | (Infinity,Infinity) =>
            if x.Sign = y.Sign then
              (invalidop_flags,float_some_qnan (FP_Sub mode x y))
            else (clear_flags,x)
          | (Infinity,NaN) =>
            (check_for_signalling [y],float_some_qnan (FP_Sub mode x y))
          | (NaN,v1) =>
            (check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y))
   
   [float_to_int_def]  Definition
      
      ⊢ ∀mode x.
          float_to_int mode x =
          case float_value x of
            Float r =>
              SOME
                (case mode of
                   roundTiesToEven =>
                     (let
                        f = ⌊r⌋;
                        df = abs (r − real_of_int f)
                      in
                        if
                          df < 1 / 2 ∨ df = 1 / 2 ∧ EVEN (Num (ABS f))
                        then
                          f
                        else ⌈r⌉)
                 | roundTowardPositive => ⌈r⌉
                 | roundTowardNegative => ⌊r⌋
                 | roundTowardZero => if x.Sign = 1w then ⌈r⌉ else ⌊r⌋)
          | Infinity => NONE
          | NaN => NONE
   
   [float_to_real_def]  Definition
      
      ⊢ ∀x. float_to_real x =
            if x.Exponent = 0w then
              -1 pow w2n x.Sign * (2 / 2 pow bias (:χ)) *
              (&w2n x.Significand / 2 pow precision (:τ))
            else
              -1 pow w2n x.Sign *
              (2 pow w2n x.Exponent / 2 pow bias (:χ)) *
              (1 + &w2n x.Significand / 2 pow precision (:τ))
   
   [float_top_def]  Definition
      
      ⊢ float_top (:τ # χ) =
        <|Sign := 0w; Exponent := UINT_MAXw − 1w;
          Significand := UINT_MAXw|>
   
   [float_unordered_def]  Definition
      
      ⊢ ∀x y. float_unordered x y ⇔ float_compare x y = UN
   
   [float_value_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0.
                 ∀ $var$('float_value').
                   (∀a0.
                      (∃a. a0 =
                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
                             a) ∨
                      a0 =
                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ∨
                      a0 =
                      ind_type$CONSTR (SUC (SUC 0)) ARB
                        (λn. ind_type$BOTTOM) ⇒
                      $var$('float_value') a0) ⇒
                   $var$('float_value') a0) rep
   
   [float_value_case_def]  Definition
      
      ⊢ (∀a f v v1. float_value_CASE (Float a) f v v1 = f a) ∧
        (∀f v v1. float_value_CASE Infinity f v v1 = v) ∧
        ∀f v v1. float_value_CASE NaN f v v1 = v1
   
   [float_value_def]  Definition
      
      ⊢ ∀x. float_value x =
            if x.Exponent = UINT_MAXw then
              if x.Significand = 0w then Infinity else NaN
            else Float (float_to_real x)
   
   [float_value_size_def]  Definition
      
      ⊢ (∀a. float_value_size (Float a) = 1) ∧
        float_value_size Infinity = 0 ∧ float_value_size NaN = 0
   
   [fp_op_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('fp_op').
                   (∀a0'.
                      (∃a0 a1.
                         a0' =
                         (λa0 a1.
                              ind_type$CONSTR 0 (a0,a1,ARB,ARB)
                                (λn. ind_type$BOTTOM)) a0 a1) ∨
                      (∃a0 a1 a2.
                         a0' =
                         (λa0 a1 a2.
                              ind_type$CONSTR (SUC 0) (a0,a1,a2,ARB)
                                (λn. ind_type$BOTTOM)) a0 a1 a2) ∨
                      (∃a0 a1 a2.
                         a0' =
                         (λa0 a1 a2.
                              ind_type$CONSTR (SUC (SUC 0)) (a0,a1,a2,ARB)
                                (λn. ind_type$BOTTOM)) a0 a1 a2) ∨
                      (∃a0 a1 a2.
                         a0' =
                         (λa0 a1 a2.
                              ind_type$CONSTR (SUC (SUC (SUC 0)))
                                (a0,a1,a2,ARB) (λn. ind_type$BOTTOM)) a0 a1
                           a2) ∨
                      (∃a0 a1 a2.
                         a0' =
                         (λa0 a1 a2.
                              ind_type$CONSTR (SUC (SUC (SUC (SUC 0))))
                                (a0,a1,a2,ARB) (λn. ind_type$BOTTOM)) a0 a1
                           a2) ∨
                      (∃a0 a1 a2 a3.
                         a0' =
                         (λa0 a1 a2 a3.
                              ind_type$CONSTR
                                (SUC (SUC (SUC (SUC (SUC 0)))))
                                (a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0 a1
                           a2 a3) ∨
                      (∃a0 a1 a2 a3.
                         a0' =
                         (λa0 a1 a2 a3.
                              ind_type$CONSTR
                                (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                                (a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0 a1
                           a2 a3) ⇒
                      $var$('fp_op') a0') ⇒
                   $var$('fp_op') a0') rep
   
   [fp_op_case_def]  Definition
      
      ⊢ (∀a0 a1 f f1 f2 f3 f4 f5 f6.
           fp_op_CASE (FP_Sqrt a0 a1) f f1 f2 f3 f4 f5 f6 = f a0 a1) ∧
        (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
           fp_op_CASE (FP_Add a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f1 a0 a1 a2) ∧
        (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
           fp_op_CASE (FP_Sub a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f2 a0 a1 a2) ∧
        (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
           fp_op_CASE (FP_Mul a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f3 a0 a1 a2) ∧
        (∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
           fp_op_CASE (FP_Div a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f4 a0 a1 a2) ∧
        (∀a0 a1 a2 a3 f f1 f2 f3 f4 f5 f6.
           fp_op_CASE (FP_MulAdd a0 a1 a2 a3) f f1 f2 f3 f4 f5 f6 =
           f5 a0 a1 a2 a3) ∧
        ∀a0 a1 a2 a3 f f1 f2 f3 f4 f5 f6.
          fp_op_CASE (FP_MulSub a0 a1 a2 a3) f f1 f2 f3 f4 f5 f6 =
          f6 a0 a1 a2 a3
   
   [fp_op_size_def]  Definition
      
      ⊢ (∀f f1 a0 a1.
           fp_op_size f f1 (FP_Sqrt a0 a1) =
           1 + (rounding_size a0 + float_size f f1 a1)) ∧
        (∀f f1 a0 a1 a2.
           fp_op_size f f1 (FP_Add a0 a1 a2) =
           1 +
           (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
        (∀f f1 a0 a1 a2.
           fp_op_size f f1 (FP_Sub a0 a1 a2) =
           1 +
           (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
        (∀f f1 a0 a1 a2.
           fp_op_size f f1 (FP_Mul a0 a1 a2) =
           1 +
           (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
        (∀f f1 a0 a1 a2.
           fp_op_size f f1 (FP_Div a0 a1 a2) =
           1 +
           (rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
        (∀f f1 a0 a1 a2 a3.
           fp_op_size f f1 (FP_MulAdd a0 a1 a2 a3) =
           1 +
           (rounding_size a0 +
            (float_size f f1 a1 +
             (float_size f f1 a2 + float_size f f1 a3)))) ∧
        ∀f f1 a0 a1 a2 a3.
          fp_op_size f f1 (FP_MulSub a0 a1 a2 a3) =
          1 +
          (rounding_size a0 +
           (float_size f f1 a1 + (float_size f f1 a2 + float_size f f1 a3)))
   
   [integral_round_def]  Definition
      
      ⊢ ∀mode x.
          integral_round mode x =
          case mode of
            roundTiesToEven =>
              (let
                 t = threshold (:τ # χ)
               in
                 if x ≤ -t then float_minus_infinity (:τ # χ)
                 else if x ≥ t then float_plus_infinity (:τ # χ)
                 else
                   closest_such
                     (λa. ∃n. EVEN n ∧ abs (float_to_real a) = &n)
                     float_is_integral x)
          | roundTowardPositive =>
            (let
               t = largest (:τ # χ)
             in
               if x < -t then float_bottom (:τ # χ)
               else if x > t then float_plus_infinity (:τ # χ)
               else
                 closest {a | float_is_integral a ∧ float_to_real a ≥ x} x)
          | roundTowardNegative =>
            (let
               t = largest (:τ # χ)
             in
               if x < -t then float_minus_infinity (:τ # χ)
               else if x > t then float_top (:τ # χ)
               else
                 closest {a | float_is_integral a ∧ float_to_real a ≤ x} x)
          | roundTowardZero =>
            (let
               t = largest (:τ # χ)
             in
               if x < -t then float_bottom (:τ # χ)
               else if x > t then float_top (:τ # χ)
               else
                 closest
                   {a | float_is_integral a ∧ abs (float_to_real a) ≤ abs x}
                   x)
   
   [invalidop_flags_def]  Definition
      
      ⊢ invalidop_flags = clear_flags with InvalidOp := T
   
   [is_closest_def]  Definition
      
      ⊢ ∀s x a.
          is_closest s x a ⇔
          a ∈ s ∧
          ∀b. b ∈ s ⇒ abs (float_to_real a − x) ≤ abs (float_to_real b − x)
   
   [is_integral_def]  Definition
      
      ⊢ ∀r. is_integral r ⇔ ∃n. abs r = &n
   
   [largest_def]  Definition
      
      ⊢ largest (:τ # χ) =
        2 pow (UINT_MAX (:χ) − 1) / 2 pow bias (:χ) *
        (2 − (2 pow precision (:τ))⁻¹)
   
   [real_to_float_def]  Definition
      
      ⊢ ∀m. real_to_float m = float_round m (m = roundTowardNegative)
   
   [real_to_float_with_flags_def]  Definition
      
      ⊢ ∀m. real_to_float_with_flags m =
            float_round_with_flags m (m = roundTowardNegative)
   
   [recordtype_flags_seldef_DivideByZero_def]  Definition
      
      ⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b
   
   [recordtype_flags_seldef_DivideByZero_fupd_def]  Definition
      
      ⊢ ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with DivideByZero updated_by f =
          flags (f b) b0 b1 b2 b3 b4
   
   [recordtype_flags_seldef_InvalidOp_def]  Definition
      
      ⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0
   
   [recordtype_flags_seldef_InvalidOp_fupd_def]  Definition
      
      ⊢ ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with InvalidOp updated_by f =
          flags b (f b0) b1 b2 b3 b4
   
   [recordtype_flags_seldef_Overflow_def]  Definition
      
      ⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1
   
   [recordtype_flags_seldef_Overflow_fupd_def]  Definition
      
      ⊢ ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with Overflow updated_by f =
          flags b b0 (f b1) b2 b3 b4
   
   [recordtype_flags_seldef_Precision_def]  Definition
      
      ⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2
   
   [recordtype_flags_seldef_Precision_fupd_def]  Definition
      
      ⊢ ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with Precision updated_by f =
          flags b b0 b1 (f b2) b3 b4
   
   [recordtype_flags_seldef_Underflow_AfterRounding_def]  Definition
      
      ⊢ ∀b b0 b1 b2 b3 b4.
          (flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ b4
   
   [recordtype_flags_seldef_Underflow_AfterRounding_fupd_def]  Definition
      
      ⊢ ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with Underflow_AfterRounding updated_by f =
          flags b b0 b1 b2 b3 (f b4)
   
   [recordtype_flags_seldef_Underflow_BeforeRounding_def]  Definition
      
      ⊢ ∀b b0 b1 b2 b3 b4.
          (flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3
   
   [recordtype_flags_seldef_Underflow_BeforeRounding_fupd_def]  Definition
      
      ⊢ ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with Underflow_BeforeRounding updated_by f =
          flags b b0 b1 b2 (f b3) b4
   
   [recordtype_float_seldef_Exponent_def]  Definition
      
      ⊢ ∀c c0 c1. (float c c0 c1).Exponent = c0
   
   [recordtype_float_seldef_Exponent_fupd_def]  Definition
      
      ⊢ ∀f c c0 c1.
          float c c0 c1 with Exponent updated_by f = float c (f c0) c1
   
   [recordtype_float_seldef_Sign_def]  Definition
      
      ⊢ ∀c c0 c1. (float c c0 c1).Sign = c
   
   [recordtype_float_seldef_Sign_fupd_def]  Definition
      
      ⊢ ∀f c c0 c1.
          float c c0 c1 with Sign updated_by f = float (f c) c0 c1
   
   [recordtype_float_seldef_Significand_def]  Definition
      
      ⊢ ∀c c0 c1. (float c c0 c1).Significand = c1
   
   [recordtype_float_seldef_Significand_fupd_def]  Definition
      
      ⊢ ∀f c c0 c1.
          float c c0 c1 with Significand updated_by f = float c c0 (f c1)
   
   [round_def]  Definition
      
      ⊢ ∀mode x.
          round mode x =
          case mode of
            roundTiesToEven =>
              (let
                 t = threshold (:τ # χ)
               in
                 if x ≤ -t then float_minus_infinity (:τ # χ)
                 else if x ≥ t then float_plus_infinity (:τ # χ)
                 else
                   closest_such (λa. ¬word_lsb a.Significand)
                     float_is_finite x)
          | roundTowardPositive =>
            (let
               t = largest (:τ # χ)
             in
               if x < -t then float_bottom (:τ # χ)
               else if x > t then float_plus_infinity (:τ # χ)
               else closest {a | float_is_finite a ∧ float_to_real a ≥ x} x)
          | roundTowardNegative =>
            (let
               t = largest (:τ # χ)
             in
               if x < -t then float_minus_infinity (:τ # χ)
               else if x > t then float_top (:τ # χ)
               else closest {a | float_is_finite a ∧ float_to_real a ≤ x} x)
          | roundTowardZero =>
            (let
               t = largest (:τ # χ)
             in
               if x < -t then float_bottom (:τ # χ)
               else if x > t then float_top (:τ # χ)
               else
                 closest
                   {a | float_is_finite a ∧ abs (float_to_real a) ≤ abs x}
                   x)
   
   [rounding_BIJ]  Definition
      
      ⊢ (∀a. num2rounding (rounding2num a) = a) ∧
        ∀r. (λn. n < 4) r ⇔ rounding2num (num2rounding r) = r
   
   [rounding_CASE]  Definition
      
      ⊢ ∀x v0 v1 v2 v3.
          (case x of
             roundTiesToEven => v0
           | roundTowardPositive => v1
           | roundTowardNegative => v2
           | roundTowardZero => v3) =
          (λm.
               if m < 1 then v0
               else if m < 2 then v1
               else if m = 2 then v2
               else v3) (rounding2num x)
   
   [rounding_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep
   
   [rounding_size_def]  Definition
      
      ⊢ ∀x. rounding_size x = 0
   
   [threshold_def]  Definition
      
      ⊢ threshold (:τ # χ) =
        2 pow (UINT_MAX (:χ) − 1) / 2 pow bias (:χ) *
        (2 − (2 pow SUC (precision (:τ)))⁻¹)
   
   [ulp_def]  Definition
      
      ⊢ ulp (:τ # χ) = ULP (0w,(:τ))
   
   [EXISTS_flags]  Theorem
      
      ⊢ ∀P. (∃f. P f) ⇔
            ∃b4 b3 b2 b1 b0 b.
              P
                <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
                  Precision := b1; Underflow_BeforeRounding := b0;
                  Underflow_AfterRounding := b|>
   
   [EXISTS_float]  Theorem
      
      ⊢ ∀P. (∃f. P f) ⇔
            ∃c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>
   
   [FINITE_floatsets]  Theorem
      
      ⊢ ∀s. FINITE s
   
   [FORALL_flags]  Theorem
      
      ⊢ ∀P. (∀f. P f) ⇔
            ∀b4 b3 b2 b1 b0 b.
              P
                <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
                  Precision := b1; Underflow_BeforeRounding := b0;
                  Underflow_AfterRounding := b|>
   
   [FORALL_float]  Theorem
      
      ⊢ ∀P. (∀f. P f) ⇔
            ∀c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>
   
   [NMUL_EQ_2]  Theorem
      
      ⊢ m * n = 2 ⇔ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1
   
   [ULP_def]  Theorem
      
      ⊢ ULP (e,(:τ)) =
        2 pow (if e = 0w then 1 else w2n e) /
        2 pow (bias (:χ) + precision (:τ))
   
   [ULP_ind]  Theorem
      
      ⊢ ∀P. (∀e. P (e,(:τ))) ⇒ ∀v v1. P (v,v1)
   
   [ULP_le_mono]  Theorem
      
      ⊢ ∀e1 e2. e2 ≠ 0w ⇒ (ULP (e1,(:τ)) ≤ ULP (e2,(:τ)) ⇔ e1 ≤₊ e2)
   
   [ULP_nonzero]  Theorem
      
      ⊢ ULP (e,(:τ)) ≠ 0
   
   [ULP_positive]  Theorem
      
      ⊢ 0 < ULP (e,i) ∧ 0 ≤ ULP (e,i) ∧ ¬(ULP (e,i) < 0) ∧ ¬(ULP (e,i) ≤ 0)
   
   [abs_float_value]  Theorem
      
      ⊢ (∀b c d. abs (-1 pow w2n b * c * d) = abs (c * d)) ∧
        ∀b c. abs (-1 pow w2n b * c) = abs c
   
   [bottom_properties]  Theorem
      
      ⊢ ¬float_is_zero (float_bottom (:τ # χ)) ∧
        float_is_finite (float_bottom (:τ # χ)) ∧
        ¬float_is_nan (float_bottom (:τ # χ)) ∧
        (float_is_normal (float_bottom (:τ # χ)) ⇔ precision (:χ) ≠ 1) ∧
        (float_is_subnormal (float_bottom (:τ # χ)) ⇔ precision (:χ) = 1) ∧
        ¬float_is_infinite (float_bottom (:τ # χ))
   
   [datatype_flags]  Theorem
      
      ⊢ DATATYPE
          (record flags DivideByZero InvalidOp Overflow Precision
             Underflow_BeforeRounding Underflow_AfterRounding)
   
   [datatype_float]  Theorem
      
      ⊢ DATATYPE (record float Sign Exponent Significand)
   
   [datatype_float_compare]  Theorem
      
      ⊢ DATATYPE (float_compare LT EQ GT UN)
   
   [datatype_float_value]  Theorem
      
      ⊢ DATATYPE (float_value Float Infinity NaN)
   
   [datatype_fp_op]  Theorem
      
      ⊢ DATATYPE
          (fp_op FP_Sqrt FP_Add FP_Sub FP_Mul FP_Div FP_MulAdd FP_MulSub)
   
   [datatype_rounding]  Theorem
      
      ⊢ DATATYPE
          (rounding roundTiesToEven roundTowardPositive roundTowardNegative
             roundTowardZero)
   
   [diff_float_ULP]  Theorem
      
      ⊢ ∀x y.
          float_to_real x ≠ float_to_real y ∧ ¬exponent_boundary y x ⇒
          ULP (x.Exponent,(:τ)) ≤ abs (float_to_real x − float_to_real y)
   
   [diff_lt_ulp_eq0]  Theorem
      
      ⊢ ∀a b x.
          ¬exponent_boundary b a ∧
          abs (x − float_to_real a) < ULP (a.Exponent,(:τ)) ∧
          abs (x − float_to_real b) < ULP (a.Exponent,(:τ)) ∧
          abs (float_to_real a) ≤ abs x ∧ abs (float_to_real b) ≤ abs x ∧
          ¬float_is_zero a ⇒
          b = a
   
   [diff_lt_ulp_even]  Theorem
      
      ⊢ ∀a b x.
          ¬exponent_boundary b a ∧
          2 * abs (float_to_real a − x) < ULP (a.Exponent,(:τ)) ∧
          2 * abs (float_to_real b − x) < ULP (a.Exponent,(:τ)) ∧
          ¬float_is_zero a ⇒
          b = a
   
   [diff_lt_ulp_even4]  Theorem
      
      ⊢ ∀a b x.
          ¬exponent_boundary b a ∧
          4 * abs (float_to_real a − x) ≤ ULP (a.Exponent,(:τ)) ∧
          4 * abs (float_to_real b − x) ≤ ULP (a.Exponent,(:τ)) ∧
          ¬float_is_zero a ⇒
          b = a
   
   [div_eq0]  Theorem
      
      ⊢ ∀a b. 0 < b ⇒ (a / b = 0 ⇔ a = 0)
   
   [exp_ge2]  Theorem
      
      ⊢ ∀b. 2 ≤ 2 ** b ⇔ 1 ≤ b
   
   [exp_gt2]  Theorem
      
      ⊢ ∀b. 2 < 2 ** b ⇔ 1 < b
   
   [flags_11]  Theorem
      
      ⊢ ∀a0 a1 a2 a3 a4 a5 a0' a1' a2' a3' a4' a5'.
          flags a0 a1 a2 a3 a4 a5 = flags a0' a1' a2' a3' a4' a5' ⇔
          (a0 ⇔ a0') ∧ (a1 ⇔ a1') ∧ (a2 ⇔ a2') ∧ (a3 ⇔ a3') ∧ (a4 ⇔ a4') ∧
          (a5 ⇔ a5')
   
   [flags_Axiom]  Theorem
      
      ⊢ ∀f. ∃fn. ∀a0 a1 a2 a3 a4 a5.
          fn (flags a0 a1 a2 a3 a4 a5) = f a0 a1 a2 a3 a4 a5
   
   [flags_accessors]  Theorem
      
      ⊢ (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b) ∧
        (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0) ∧
        (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1) ∧
        (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2) ∧
        (∀b b0 b1 b2 b3 b4.
           (flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3) ∧
        ∀b b0 b1 b2 b3 b4.
          (flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ b4
   
   [flags_accfupds]  Theorem
      
      ⊢ (∀f0 f.
           (f with InvalidOp updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
        (∀f0 f.
           (f with Overflow updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
        (∀f0 f.
           (f with Precision updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
        (∀f0 f.
           (f with Underflow_BeforeRounding updated_by f0).DivideByZero ⇔
           f.DivideByZero) ∧
        (∀f0 f.
           (f with Underflow_AfterRounding updated_by f0).DivideByZero ⇔
           f.DivideByZero) ∧
        (∀f0 f. (f with DivideByZero updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
        (∀f0 f. (f with Overflow updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
        (∀f0 f. (f with Precision updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
        (∀f0 f.
           (f with Underflow_BeforeRounding updated_by f0).InvalidOp ⇔
           f.InvalidOp) ∧
        (∀f0 f.
           (f with Underflow_AfterRounding updated_by f0).InvalidOp ⇔
           f.InvalidOp) ∧
        (∀f0 f. (f with DivideByZero updated_by f0).Overflow ⇔ f.Overflow) ∧
        (∀f0 f. (f with InvalidOp updated_by f0).Overflow ⇔ f.Overflow) ∧
        (∀f0 f. (f with Precision updated_by f0).Overflow ⇔ f.Overflow) ∧
        (∀f0 f.
           (f with Underflow_BeforeRounding updated_by f0).Overflow ⇔
           f.Overflow) ∧
        (∀f0 f.
           (f with Underflow_AfterRounding updated_by f0).Overflow ⇔
           f.Overflow) ∧
        (∀f0 f. (f with DivideByZero updated_by f0).Precision ⇔ f.Precision) ∧
        (∀f0 f. (f with InvalidOp updated_by f0).Precision ⇔ f.Precision) ∧
        (∀f0 f. (f with Overflow updated_by f0).Precision ⇔ f.Precision) ∧
        (∀f0 f.
           (f with Underflow_BeforeRounding updated_by f0).Precision ⇔
           f.Precision) ∧
        (∀f0 f.
           (f with Underflow_AfterRounding updated_by f0).Precision ⇔
           f.Precision) ∧
        (∀f0 f.
           (f with DivideByZero updated_by f0).Underflow_BeforeRounding ⇔
           f.Underflow_BeforeRounding) ∧
        (∀f0 f.
           (f with InvalidOp updated_by f0).Underflow_BeforeRounding ⇔
           f.Underflow_BeforeRounding) ∧
        (∀f0 f.
           (f with Overflow updated_by f0).Underflow_BeforeRounding ⇔
           f.Underflow_BeforeRounding) ∧
        (∀f0 f.
           (f with Precision updated_by f0).Underflow_BeforeRounding ⇔
           f.Underflow_BeforeRounding) ∧
        (∀f0 f.
           (f with Underflow_AfterRounding updated_by f0).
           Underflow_BeforeRounding ⇔ f.Underflow_BeforeRounding) ∧
        (∀f0 f.
           (f with DivideByZero updated_by f0).Underflow_AfterRounding ⇔
           f.Underflow_AfterRounding) ∧
        (∀f0 f.
           (f with InvalidOp updated_by f0).Underflow_AfterRounding ⇔
           f.Underflow_AfterRounding) ∧
        (∀f0 f.
           (f with Overflow updated_by f0).Underflow_AfterRounding ⇔
           f.Underflow_AfterRounding) ∧
        (∀f0 f.
           (f with Precision updated_by f0).Underflow_AfterRounding ⇔
           f.Underflow_AfterRounding) ∧
        (∀f0 f.
           (f with Underflow_BeforeRounding updated_by f0).
           Underflow_AfterRounding ⇔ f.Underflow_AfterRounding) ∧
        (∀f0 f.
           (f with DivideByZero updated_by f0).DivideByZero ⇔
           f0 f.DivideByZero) ∧
        (∀f0 f. (f with InvalidOp updated_by f0).InvalidOp ⇔ f0 f.InvalidOp) ∧
        (∀f0 f. (f with Overflow updated_by f0).Overflow ⇔ f0 f.Overflow) ∧
        (∀f0 f. (f with Precision updated_by f0).Precision ⇔ f0 f.Precision) ∧
        (∀f0 f.
           (f with Underflow_BeforeRounding updated_by f0).
           Underflow_BeforeRounding ⇔ f0 f.Underflow_BeforeRounding) ∧
        ∀f0 f.
          (f with Underflow_AfterRounding updated_by f0).
          Underflow_AfterRounding ⇔ f0 f.Underflow_AfterRounding
   
   [flags_case_cong]  Theorem
      
      ⊢ ∀M M' f.
          M = M' ∧
          (∀a0 a1 a2 a3 a4 a5.
             M' = flags a0 a1 a2 a3 a4 a5 ⇒
             f a0 a1 a2 a3 a4 a5 = f' a0 a1 a2 a3 a4 a5) ⇒
          flags_CASE M f = flags_CASE M' f'
   
   [flags_case_eq]  Theorem
      
      ⊢ flags_CASE x f = v ⇔
        ∃b b0 b1 b2 b3 b4.
          x = flags b b0 b1 b2 b3 b4 ∧ f b b0 b1 b2 b3 b4 = v
   
   [flags_component_equality]  Theorem
      
      ⊢ ∀f1 f2.
          f1 = f2 ⇔
          (f1.DivideByZero ⇔ f2.DivideByZero) ∧
          (f1.InvalidOp ⇔ f2.InvalidOp) ∧ (f1.Overflow ⇔ f2.Overflow) ∧
          (f1.Precision ⇔ f2.Precision) ∧
          (f1.Underflow_BeforeRounding ⇔ f2.Underflow_BeforeRounding) ∧
          (f1.Underflow_AfterRounding ⇔ f2.Underflow_AfterRounding)
   
   [flags_fn_updates]  Theorem
      
      ⊢ (∀f b b0 b1 b2 b3 b4.
           flags b b0 b1 b2 b3 b4 with DivideByZero updated_by f =
           flags (f b) b0 b1 b2 b3 b4) ∧
        (∀f b b0 b1 b2 b3 b4.
           flags b b0 b1 b2 b3 b4 with InvalidOp updated_by f =
           flags b (f b0) b1 b2 b3 b4) ∧
        (∀f b b0 b1 b2 b3 b4.
           flags b b0 b1 b2 b3 b4 with Overflow updated_by f =
           flags b b0 (f b1) b2 b3 b4) ∧
        (∀f b b0 b1 b2 b3 b4.
           flags b b0 b1 b2 b3 b4 with Precision updated_by f =
           flags b b0 b1 (f b2) b3 b4) ∧
        (∀f b b0 b1 b2 b3 b4.
           flags b b0 b1 b2 b3 b4 with
           Underflow_BeforeRounding updated_by f =
           flags b b0 b1 b2 (f b3) b4) ∧
        ∀f b b0 b1 b2 b3 b4.
          flags b b0 b1 b2 b3 b4 with Underflow_AfterRounding updated_by f =
          flags b b0 b1 b2 b3 (f b4)
   
   [flags_fupdcanon]  Theorem
      
      ⊢ (∀g f0 f.
           f with <|InvalidOp updated_by f0; DivideByZero updated_by g|> =
           f with <|DivideByZero updated_by g; InvalidOp updated_by f0|>) ∧
        (∀g f0 f.
           f with <|Overflow updated_by f0; DivideByZero updated_by g|> =
           f with <|DivideByZero updated_by g; Overflow updated_by f0|>) ∧
        (∀g f0 f.
           f with <|Overflow updated_by f0; InvalidOp updated_by g|> =
           f with <|InvalidOp updated_by g; Overflow updated_by f0|>) ∧
        (∀g f0 f.
           f with <|Precision updated_by f0; DivideByZero updated_by g|> =
           f with <|DivideByZero updated_by g; Precision updated_by f0|>) ∧
        (∀g f0 f.
           f with <|Precision updated_by f0; InvalidOp updated_by g|> =
           f with <|InvalidOp updated_by g; Precision updated_by f0|>) ∧
        (∀g f0 f.
           f with <|Precision updated_by f0; Overflow updated_by g|> =
           f with <|Overflow updated_by g; Precision updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_BeforeRounding updated_by f0;
             DivideByZero updated_by g|> =
           f with
           <|DivideByZero updated_by g;
             Underflow_BeforeRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_BeforeRounding updated_by f0;
             InvalidOp updated_by g|> =
           f with
           <|InvalidOp updated_by g;
             Underflow_BeforeRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_BeforeRounding updated_by f0;
             Overflow updated_by g|> =
           f with
           <|Overflow updated_by g;
             Underflow_BeforeRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_BeforeRounding updated_by f0;
             Precision updated_by g|> =
           f with
           <|Precision updated_by g;
             Underflow_BeforeRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_AfterRounding updated_by f0;
             DivideByZero updated_by g|> =
           f with
           <|DivideByZero updated_by g;
             Underflow_AfterRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_AfterRounding updated_by f0;
             InvalidOp updated_by g|> =
           f with
           <|InvalidOp updated_by g;
             Underflow_AfterRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_AfterRounding updated_by f0; Overflow updated_by g|> =
           f with
           <|Overflow updated_by g; Underflow_AfterRounding updated_by f0|>) ∧
        (∀g f0 f.
           f with
           <|Underflow_AfterRounding updated_by f0;
             Precision updated_by g|> =
           f with
           <|Precision updated_by g;
             Underflow_AfterRounding updated_by f0|>) ∧
        ∀g f0 f.
          f with
          <|Underflow_AfterRounding updated_by f0;
            Underflow_BeforeRounding updated_by g|> =
          f with
          <|Underflow_BeforeRounding updated_by g;
            Underflow_AfterRounding updated_by f0|>
   
   [flags_fupdcanon_comp]  Theorem
      
      ⊢ ((∀g f0.
            InvalidOp_fupd f0 ∘ DivideByZero_fupd g =
            DivideByZero_fupd g ∘ InvalidOp_fupd f0) ∧
         ∀h g f0.
           InvalidOp_fupd f0 ∘ DivideByZero_fupd g ∘ h =
           DivideByZero_fupd g ∘ InvalidOp_fupd f0 ∘ h) ∧
        ((∀g f0.
            Overflow_fupd f0 ∘ DivideByZero_fupd g =
            DivideByZero_fupd g ∘ Overflow_fupd f0) ∧
         ∀h g f0.
           Overflow_fupd f0 ∘ DivideByZero_fupd g ∘ h =
           DivideByZero_fupd g ∘ Overflow_fupd f0 ∘ h) ∧
        ((∀g f0.
            Overflow_fupd f0 ∘ InvalidOp_fupd g =
            InvalidOp_fupd g ∘ Overflow_fupd f0) ∧
         ∀h g f0.
           Overflow_fupd f0 ∘ InvalidOp_fupd g ∘ h =
           InvalidOp_fupd g ∘ Overflow_fupd f0 ∘ h) ∧
        ((∀g f0.
            Precision_fupd f0 ∘ DivideByZero_fupd g =
            DivideByZero_fupd g ∘ Precision_fupd f0) ∧
         ∀h g f0.
           Precision_fupd f0 ∘ DivideByZero_fupd g ∘ h =
           DivideByZero_fupd g ∘ Precision_fupd f0 ∘ h) ∧
        ((∀g f0.
            Precision_fupd f0 ∘ InvalidOp_fupd g =
            InvalidOp_fupd g ∘ Precision_fupd f0) ∧
         ∀h g f0.
           Precision_fupd f0 ∘ InvalidOp_fupd g ∘ h =
           InvalidOp_fupd g ∘ Precision_fupd f0 ∘ h) ∧
        ((∀g f0.
            Precision_fupd f0 ∘ Overflow_fupd g =
            Overflow_fupd g ∘ Precision_fupd f0) ∧
         ∀h g f0.
           Precision_fupd f0 ∘ Overflow_fupd g ∘ h =
           Overflow_fupd g ∘ Precision_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_BeforeRounding_fupd f0 ∘ DivideByZero_fupd g =
            DivideByZero_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_BeforeRounding_fupd f0 ∘ DivideByZero_fupd g ∘ h =
           DivideByZero_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_BeforeRounding_fupd f0 ∘ InvalidOp_fupd g =
            InvalidOp_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_BeforeRounding_fupd f0 ∘ InvalidOp_fupd g ∘ h =
           InvalidOp_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_BeforeRounding_fupd f0 ∘ Overflow_fupd g =
            Overflow_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_BeforeRounding_fupd f0 ∘ Overflow_fupd g ∘ h =
           Overflow_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_BeforeRounding_fupd f0 ∘ Precision_fupd g =
            Precision_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_BeforeRounding_fupd f0 ∘ Precision_fupd g ∘ h =
           Precision_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_AfterRounding_fupd f0 ∘ DivideByZero_fupd g =
            DivideByZero_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_AfterRounding_fupd f0 ∘ DivideByZero_fupd g ∘ h =
           DivideByZero_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_AfterRounding_fupd f0 ∘ InvalidOp_fupd g =
            InvalidOp_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_AfterRounding_fupd f0 ∘ InvalidOp_fupd g ∘ h =
           InvalidOp_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_AfterRounding_fupd f0 ∘ Overflow_fupd g =
            Overflow_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_AfterRounding_fupd f0 ∘ Overflow_fupd g ∘ h =
           Overflow_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
        ((∀g f0.
            Underflow_AfterRounding_fupd f0 ∘ Precision_fupd g =
            Precision_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
         ∀h g f0.
           Underflow_AfterRounding_fupd f0 ∘ Precision_fupd g ∘ h =
           Precision_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
        (∀g f0.
           Underflow_AfterRounding_fupd f0 ∘
           Underflow_BeforeRounding_fupd g =
           Underflow_BeforeRounding_fupd g ∘
           Underflow_AfterRounding_fupd f0) ∧
        ∀h g f0.
          Underflow_AfterRounding_fupd f0 ∘
          Underflow_BeforeRounding_fupd g ∘ h =
          Underflow_BeforeRounding_fupd g ∘
          Underflow_AfterRounding_fupd f0 ∘ h
   
   [flags_fupdfupds]  Theorem
      
      ⊢ (∀g f0 f.
           f with <|DivideByZero updated_by f0; DivideByZero updated_by g|> =
           f with DivideByZero updated_by f0 ∘ g) ∧
        (∀g f0 f.
           f with <|InvalidOp updated_by f0; InvalidOp updated_by g|> =
           f with InvalidOp updated_by f0 ∘ g) ∧
        (∀g f0 f.
           f with <|Overflow updated_by f0; Overflow updated_by g|> =
           f with Overflow updated_by f0 ∘ g) ∧
        (∀g f0 f.
           f with <|Precision updated_by f0; Precision updated_by g|> =
           f with Precision updated_by f0 ∘ g) ∧
        (∀g f0 f.
           f with
           <|Underflow_BeforeRounding updated_by f0;
             Underflow_BeforeRounding updated_by g|> =
           f with Underflow_BeforeRounding updated_by f0 ∘ g) ∧
        ∀g f0 f.
          f with
          <|Underflow_AfterRounding updated_by f0;
            Underflow_AfterRounding updated_by g|> =
          f with Underflow_AfterRounding updated_by f0 ∘ g
   
   [flags_fupdfupds_comp]  Theorem
      
      ⊢ ((∀g f0.
            DivideByZero_fupd f0 ∘ DivideByZero_fupd g =
            DivideByZero_fupd (f0 ∘ g)) ∧
         ∀h g f0.
           DivideByZero_fupd f0 ∘ DivideByZero_fupd g ∘ h =
           DivideByZero_fupd (f0 ∘ g) ∘ h) ∧
        ((∀g f0.
            InvalidOp_fupd f0 ∘ InvalidOp_fupd g = InvalidOp_fupd (f0 ∘ g)) ∧
         ∀h g f0.
           InvalidOp_fupd f0 ∘ InvalidOp_fupd g ∘ h =
           InvalidOp_fupd (f0 ∘ g) ∘ h) ∧
        ((∀g f0.
            Overflow_fupd f0 ∘ Overflow_fupd g = Overflow_fupd (f0 ∘ g)) ∧
         ∀h g f0.
           Overflow_fupd f0 ∘ Overflow_fupd g ∘ h =
           Overflow_fupd (f0 ∘ g) ∘ h) ∧
        ((∀g f0.
            Precision_fupd f0 ∘ Precision_fupd g = Precision_fupd (f0 ∘ g)) ∧
         ∀h g f0.
           Precision_fupd f0 ∘ Precision_fupd g ∘ h =
           Precision_fupd (f0 ∘ g) ∘ h) ∧
        ((∀g f0.
            Underflow_BeforeRounding_fupd f0 ∘
            Underflow_BeforeRounding_fupd g =
            Underflow_BeforeRounding_fupd (f0 ∘ g)) ∧
         ∀h g f0.
           Underflow_BeforeRounding_fupd f0 ∘
           Underflow_BeforeRounding_fupd g ∘ h =
           Underflow_BeforeRounding_fupd (f0 ∘ g) ∘ h) ∧
        (∀g f0.
           Underflow_AfterRounding_fupd f0 ∘ Underflow_AfterRounding_fupd g =
           Underflow_AfterRounding_fupd (f0 ∘ g)) ∧
        ∀h g f0.
          Underflow_AfterRounding_fupd f0 ∘
          Underflow_AfterRounding_fupd g ∘ h =
          Underflow_AfterRounding_fupd (f0 ∘ g) ∘ h
   
   [flags_induction]  Theorem
      
      ⊢ ∀P. (∀b b0 b1 b2 b3 b4. P (flags b b0 b1 b2 b3 b4)) ⇒ ∀f. P f
   
   [flags_literal_11]  Theorem
      
      ⊢ ∀b41 b31 b21 b11 b01 b1 b42 b32 b22 b12 b02 b2.
          <|DivideByZero := b41; InvalidOp := b31; Overflow := b21;
            Precision := b11; Underflow_BeforeRounding := b01;
            Underflow_AfterRounding := b1|> =
          <|DivideByZero := b42; InvalidOp := b32; Overflow := b22;
            Precision := b12; Underflow_BeforeRounding := b02;
            Underflow_AfterRounding := b2|> ⇔
          (b41 ⇔ b42) ∧ (b31 ⇔ b32) ∧ (b21 ⇔ b22) ∧ (b11 ⇔ b12) ∧
          (b01 ⇔ b02) ∧ (b1 ⇔ b2)
   
   [flags_literal_nchotomy]  Theorem
      
      ⊢ ∀f. ∃b4 b3 b2 b1 b0 b.
          f =
          <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
            Precision := b1; Underflow_BeforeRounding := b0;
            Underflow_AfterRounding := b|>
   
   [flags_nchotomy]  Theorem
      
      ⊢ ∀ff. ∃b b0 b1 b2 b3 b4. ff = flags b b0 b1 b2 b3 b4
   
   [flags_updates_eq_literal]  Theorem
      
      ⊢ ∀f b4 b3 b2 b1 b0 b.
          f with
          <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
            Precision := b1; Underflow_BeforeRounding := b0;
            Underflow_AfterRounding := b|> =
          <|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
            Precision := b1; Underflow_BeforeRounding := b0;
            Underflow_AfterRounding := b|>
   
   [float_11]  Theorem
      
      ⊢ ∀a0 a1 a2 a0' a1' a2'.
          float a0 a1 a2 = float a0' a1' a2' ⇔
          a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
   
   [float_Axiom]  Theorem
      
      ⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (float a0 a1 a2) = f a0 a1 a2
   
   [float_accessors]  Theorem
      
      ⊢ (∀c c0 c1. (float c c0 c1).Sign = c) ∧
        (∀c c0 c1. (float c c0 c1).Exponent = c0) ∧
        ∀c c0 c1. (float c c0 c1).Significand = c1
   
   [float_accfupds]  Theorem
      
      ⊢ (∀f0 f. (f with Exponent updated_by f0).Sign = f.Sign) ∧
        (∀f0 f. (f with Significand updated_by f0).Sign = f.Sign) ∧
        (∀f0 f. (f with Sign updated_by f0).Exponent = f.Exponent) ∧
        (∀f0 f. (f with Significand updated_by f0).Exponent = f.Exponent) ∧
        (∀f0 f. (f with Sign updated_by f0).Significand = f.Significand) ∧
        (∀f0 f. (f with Exponent updated_by f0).Significand = f.Significand) ∧
        (∀f0 f. (f with Sign updated_by f0).Sign = f0 f.Sign) ∧
        (∀f0 f. (f with Exponent updated_by f0).Exponent = f0 f.Exponent) ∧
        ∀f0 f.
          (f with Significand updated_by f0).Significand = f0 f.Significand
   
   [float_add_compute]  Theorem
      
      ⊢ (∀mode x fp_op.
           float_add mode (float_some_qnan fp_op) x =
           (check_for_signalling [x],
            float_some_qnan (FP_Add mode (float_some_qnan fp_op) x))) ∧
        (∀mode x fp_op.
           float_add mode x (float_some_qnan fp_op) =
           (check_for_signalling [x],
            float_some_qnan (FP_Add mode x (float_some_qnan fp_op)))) ∧
        (∀mode.
           float_add mode (float_minus_infinity (:τ # χ))
             (float_minus_infinity (:τ # χ)) =
           (clear_flags,float_minus_infinity (:τ # χ))) ∧
        (∀mode.
           float_add mode (float_minus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (invalidop_flags,
            float_some_qnan
              (FP_Add mode (float_minus_infinity (:τ # χ))
                 (float_plus_infinity (:τ # χ))))) ∧
        (∀mode.
           float_add mode (float_plus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (clear_flags,float_plus_infinity (:τ # χ))) ∧
        ∀mode.
          float_add mode (float_plus_infinity (:τ # χ))
            (float_minus_infinity (:τ # χ)) =
          (invalidop_flags,
           float_some_qnan
             (FP_Add mode (float_plus_infinity (:τ # χ))
                (float_minus_infinity (:τ # χ))))
   
   [float_add_finite]  Theorem
      
      ⊢ ∀mode x y r1 r2.
          float_value x = Float r1 ∧ float_value y = Float r2 ⇒
          float_add mode x y =
          float_round_with_flags mode
            (if r1 = 0 ∧ r2 = 0 ∧ x.Sign = y.Sign then x.Sign = 1w
             else (mode = roundTowardNegative)) (r1 + r2)
   
   [float_add_finite_minus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_add mode x (float_minus_infinity (:τ # χ)) =
          (clear_flags,float_minus_infinity (:τ # χ))
   
   [float_add_finite_plus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_add mode x (float_plus_infinity (:τ # χ)) =
          (clear_flags,float_plus_infinity (:τ # χ))
   
   [float_add_minus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_add mode (float_minus_infinity (:τ # χ)) x =
          (clear_flags,float_minus_infinity (:τ # χ))
   
   [float_add_nan]  Theorem
      
      ⊢ ∀mode x y.
          float_value x = NaN ∨ float_value y = NaN ⇒
          float_add mode x y =
          (check_for_signalling [x; y],float_some_qnan (FP_Add mode x y))
   
   [float_add_plus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_add mode (float_plus_infinity (:τ # χ)) x =
          (clear_flags,float_plus_infinity (:τ # χ))
   
   [float_case_cong]  Theorem
      
      ⊢ ∀M M' f.
          M = M' ∧
          (∀a0 a1 a2. M' = float a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
          float_CASE M f = float_CASE M' f'
   
   [float_case_eq]  Theorem
      
      ⊢ float_CASE x f = v ⇔ ∃c c0 c1. x = float c c0 c1 ∧ f c c0 c1 = v
   
   [float_cases]  Theorem
      
      ⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_normal x ∨
            float_is_subnormal x ∨ float_is_zero x
   
   [float_cases_finite]  Theorem
      
      ⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_finite x
   
   [float_compare2num_11]  Theorem
      
      ⊢ ∀a a'. float_compare2num a = float_compare2num a' ⇔ a = a'
   
   [float_compare2num_ONTO]  Theorem
      
      ⊢ ∀r. r < 4 ⇔ ∃a. r = float_compare2num a
   
   [float_compare2num_num2float_compare]  Theorem
      
      ⊢ ∀r. r < 4 ⇔ float_compare2num (num2float_compare r) = r
   
   [float_compare2num_thm]  Theorem
      
      ⊢ float_compare2num LT = 0 ∧ float_compare2num EQ = 1 ∧
        float_compare2num GT = 2 ∧ float_compare2num UN = 3
   
   [float_compare_Axiom]  Theorem
      
      ⊢ ∀x0 x1 x2 x3. ∃f. f LT = x0 ∧ f EQ = x1 ∧ f GT = x2 ∧ f UN = x3
   
   [float_compare_EQ_float_compare]  Theorem
      
      ⊢ ∀a a'. a = a' ⇔ float_compare2num a = float_compare2num a'
   
   [float_compare_case_cong]  Theorem
      
      ⊢ ∀M M' v0 v1 v2 v3.
          M = M' ∧ (M' = LT ⇒ v0 = v0') ∧ (M' = EQ ⇒ v1 = v1') ∧
          (M' = GT ⇒ v2 = v2') ∧ (M' = UN ⇒ v3 = v3') ⇒
          (case M of LT => v0 | EQ => v1 | GT => v2 | UN => v3) =
          case M' of LT => v0' | EQ => v1' | GT => v2' | UN => v3'
   
   [float_compare_case_def]  Theorem
      
      ⊢ (∀v0 v1 v2 v3.
           (case LT of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v0) ∧
        (∀v0 v1 v2 v3.
           (case EQ of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v1) ∧
        (∀v0 v1 v2 v3.
           (case GT of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v2) ∧
        ∀v0 v1 v2 v3.
          (case UN of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v3
   
   [float_compare_case_eq]  Theorem
      
      ⊢ (case x of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v ⇔
        x = LT ∧ v0 = v ∨ x = EQ ∧ v1 = v ∨ x = GT ∧ v2 = v ∨
        x = UN ∧ v3 = v
   
   [float_compare_distinct]  Theorem
      
      ⊢ LT ≠ EQ ∧ LT ≠ GT ∧ LT ≠ UN ∧ EQ ≠ GT ∧ EQ ≠ UN ∧ GT ≠ UN
   
   [float_compare_induction]  Theorem
      
      ⊢ ∀P. P EQ ∧ P GT ∧ P LT ∧ P UN ⇒ ∀a. P a
   
   [float_compare_nchotomy]  Theorem
      
      ⊢ ∀a. a = LT ∨ a = EQ ∨ a = GT ∨ a = UN
   
   [float_component_equality]  Theorem
      
      ⊢ ∀f1 f2.
          f1 = f2 ⇔
          f1.Sign = f2.Sign ∧ f1.Exponent = f2.Exponent ∧
          f1.Significand = f2.Significand
   
   [float_components]  Theorem
      
      ⊢ (float_plus_infinity (:τ # χ)).Sign = 0w ∧
        (float_plus_infinity (:τ # χ)).Exponent = UINT_MAXw ∧
        (float_plus_infinity (:τ # χ)).Significand = 0w ∧
        (float_minus_infinity (:τ # χ)).Sign = 1w ∧
        (float_minus_infinity (:τ # χ)).Exponent = UINT_MAXw ∧
        (float_minus_infinity (:τ # χ)).Significand = 0w ∧ POS0.Sign = 0w ∧
        POS0.Exponent = 0w ∧ POS0.Significand = 0w ∧ NEG0.Sign = 1w ∧
        NEG0.Exponent = 0w ∧ NEG0.Significand = 0w ∧
        (float_plus_min (:τ # χ)).Sign = 0w ∧
        (float_plus_min (:τ # χ)).Exponent = 0w ∧
        (float_plus_min (:τ # χ)).Significand = 1w ∧
        (float_minus_min (:τ # χ)).Sign = 1w ∧
        (float_minus_min (:τ # χ)).Exponent = 0w ∧
        (float_minus_min (:τ # χ)).Significand = 1w ∧
        (float_top (:τ # χ)).Sign = 0w ∧
        (float_top (:τ # χ)).Exponent = UINT_MAXw − 1w ∧
        (float_top (:τ # χ)).Significand = UINT_MAXw ∧
        (float_bottom (:τ # χ)).Sign = 1w ∧
        (float_bottom (:τ # χ)).Exponent = UINT_MAXw − 1w ∧
        (float_bottom (:τ # χ)).Significand = UINT_MAXw ∧
        (∀fp_op. (float_some_qnan fp_op).Exponent = UINT_MAXw) ∧
        (∀fp_op. (float_some_qnan fp_op).Significand ≠ 0w) ∧
        (∀x. (float_negate x).Sign = ¬x.Sign) ∧
        (∀x. (float_negate x).Exponent = x.Exponent) ∧
        ∀x. (float_negate x).Significand = x.Significand
   
   [float_distinct]  Theorem
      
      ⊢ float_plus_infinity (:τ # χ) ≠ float_minus_infinity (:τ # χ) ∧
        float_plus_infinity (:τ # χ) ≠ POS0 ∧
        float_plus_infinity (:τ # χ) ≠ NEG0 ∧
        float_plus_infinity (:τ # χ) ≠ float_top (:τ # χ) ∧
        float_plus_infinity (:τ # χ) ≠ float_bottom (:τ # χ) ∧
        float_plus_infinity (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
        float_plus_infinity (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
        (∀fp_op. float_plus_infinity (:τ # χ) ≠ float_some_qnan fp_op) ∧
        float_minus_infinity (:τ # χ) ≠ POS0 ∧
        float_minus_infinity (:τ # χ) ≠ NEG0 ∧
        float_minus_infinity (:τ # χ) ≠ float_top (:τ # χ) ∧
        float_minus_infinity (:τ # χ) ≠ float_bottom (:τ # χ) ∧
        float_minus_infinity (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
        float_minus_infinity (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
        (∀fp_op. float_minus_infinity (:τ # χ) ≠ float_some_qnan fp_op) ∧
        POS0 ≠ NEG0 ∧ POS0 ≠ float_top (:τ # χ) ∧
        POS0 ≠ float_bottom (:τ # χ) ∧ POS0 ≠ float_plus_min (:τ # χ) ∧
        POS0 ≠ float_minus_min (:τ # χ) ∧
        (∀fp_op. POS0 ≠ float_some_qnan fp_op) ∧
        NEG0 ≠ float_top (:τ # χ) ∧ NEG0 ≠ float_bottom (:τ # χ) ∧
        NEG0 ≠ float_plus_min (:τ # χ) ∧ NEG0 ≠ float_minus_min (:τ # χ) ∧
        (∀fp_op. NEG0 ≠ float_some_qnan fp_op) ∧
        float_top (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
        float_top (:τ # χ) ≠ float_bottom (:τ # χ) ∧
        (∀fp_op. float_top (:τ # χ) ≠ float_some_qnan fp_op) ∧
        float_bottom (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
        (∀fp_op. float_bottom (:τ # χ) ≠ float_some_qnan fp_op) ∧
        (∀fp_op. float_plus_min (:τ # χ) ≠ float_some_qnan fp_op) ∧
        float_plus_min (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
        (∀fp_op. float_minus_min (:τ # χ) ≠ float_some_qnan fp_op) ∧
        ∀x. float_negate x ≠ x
   
   [float_distinct_finite]  Theorem
      
      ⊢ ∀x. ¬(float_is_nan x ∧ float_is_infinite x) ∧
            ¬(float_is_nan x ∧ float_is_finite x) ∧
            ¬(float_is_infinite x ∧ float_is_finite x)
   
   [float_div_compute]  Theorem
      
      ⊢ (∀mode x fp_op.
           float_div mode (float_some_qnan fp_op) x =
           (check_for_signalling [x],
            float_some_qnan (FP_Div mode (float_some_qnan fp_op) x))) ∧
        (∀mode x fp_op.
           float_div mode x (float_some_qnan fp_op) =
           (check_for_signalling [x],
            float_some_qnan (FP_Div mode x (float_some_qnan fp_op)))) ∧
        (∀mode.
           float_div mode (float_minus_infinity (:τ # χ))
             (float_minus_infinity (:τ # χ)) =
           (invalidop_flags,
            float_some_qnan
              (FP_Div mode (float_minus_infinity (:τ # χ))
                 (float_minus_infinity (:τ # χ))))) ∧
        (∀mode.
           float_div mode (float_minus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (invalidop_flags,
            float_some_qnan
              (FP_Div mode (float_minus_infinity (:τ # χ))
                 (float_plus_infinity (:τ # χ))))) ∧
        (∀mode.
           float_div mode (float_plus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (invalidop_flags,
            float_some_qnan
              (FP_Div mode (float_plus_infinity (:τ # χ))
                 (float_plus_infinity (:τ # χ))))) ∧
        ∀mode.
          float_div mode (float_plus_infinity (:τ # χ))
            (float_minus_infinity (:τ # χ)) =
          (invalidop_flags,
           float_some_qnan
             (FP_Div mode (float_plus_infinity (:τ # χ))
                (float_minus_infinity (:τ # χ))))
   
   [float_div_finite]  Theorem
      
      ⊢ ∀mode x y r1 r2.
          float_value x = Float r1 ∧ float_value y = Float r2 ⇒
          float_div mode x y =
          if r2 = 0 then
            if r1 = 0 then
              (invalidop_flags,float_some_qnan (FP_Div mode x y))
            else
              (dividezero_flags,
               if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
               else float_minus_infinity (:τ # χ))
          else float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 / r2)
   
   [float_div_finite_minus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_div mode x (float_minus_infinity (:τ # χ)) =
          (clear_flags,if x.Sign = 0w then NEG0 else POS0)
   
   [float_div_finite_plus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_div mode x (float_plus_infinity (:τ # χ)) =
          (clear_flags,if x.Sign = 0w then POS0 else NEG0)
   
   [float_div_minus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_div mode (float_minus_infinity (:τ # χ)) x =
          (clear_flags,
           if x.Sign = 0w then float_minus_infinity (:τ # χ)
           else float_plus_infinity (:τ # χ))
   
   [float_div_nan]  Theorem
      
      ⊢ ∀mode x y.
          float_value x = NaN ∨ float_value y = NaN ⇒
          float_div mode x y =
          (check_for_signalling [x; y],float_some_qnan (FP_Div mode x y))
   
   [float_div_plus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_div mode (float_plus_infinity (:τ # χ)) x =
          (clear_flags,
           if x.Sign = 0w then float_plus_infinity (:τ # χ)
           else float_minus_infinity (:τ # χ))
   
   [float_fn_updates]  Theorem
      
      ⊢ (∀f c c0 c1.
           float c c0 c1 with Sign updated_by f = float (f c) c0 c1) ∧
        (∀f c c0 c1.
           float c c0 c1 with Exponent updated_by f = float c (f c0) c1) ∧
        ∀f c c0 c1.
          float c c0 c1 with Significand updated_by f = float c c0 (f c1)
   
   [float_fupdcanon]  Theorem
      
      ⊢ (∀g f0 f.
           f with <|Exponent updated_by f0; Sign updated_by g|> =
           f with <|Sign updated_by g; Exponent updated_by f0|>) ∧
        (∀g f0 f.
           f with <|Significand updated_by f0; Sign updated_by g|> =
           f with <|Sign updated_by g; Significand updated_by f0|>) ∧
        ∀g f0 f.
          f with <|Significand updated_by f0; Exponent updated_by g|> =
          f with <|Exponent updated_by g; Significand updated_by f0|>
   
   [float_fupdcanon_comp]  Theorem
      
      ⊢ ((∀g f0.
            Exponent_fupd f0 ∘ Sign_fupd g = Sign_fupd g ∘ Exponent_fupd f0) ∧
         ∀h g f0.
           Exponent_fupd f0 ∘ Sign_fupd g ∘ h =
           Sign_fupd g ∘ Exponent_fupd f0 ∘ h) ∧
        ((∀g f0.
            Significand_fupd f0 ∘ Sign_fupd g =
            Sign_fupd g ∘ Significand_fupd f0) ∧
         ∀h g f0.
           Significand_fupd f0 ∘ Sign_fupd g ∘ h =
           Sign_fupd g ∘ Significand_fupd f0 ∘ h) ∧
        (∀g f0.
           Significand_fupd f0 ∘ Exponent_fupd g =
           Exponent_fupd g ∘ Significand_fupd f0) ∧
        ∀h g f0.
          Significand_fupd f0 ∘ Exponent_fupd g ∘ h =
          Exponent_fupd g ∘ Significand_fupd f0 ∘ h
   
   [float_fupdfupds]  Theorem
      
      ⊢ (∀g f0 f.
           f with <|Sign updated_by f0; Sign updated_by g|> =
           f with Sign updated_by f0 ∘ g) ∧
        (∀g f0 f.
           f with <|Exponent updated_by f0; Exponent updated_by g|> =
           f with Exponent updated_by f0 ∘ g) ∧
        ∀g f0 f.
          f with <|Significand updated_by f0; Significand updated_by g|> =
          f with Significand updated_by f0 ∘ g
   
   [float_fupdfupds_comp]  Theorem
      
      ⊢ ((∀g f0. Sign_fupd f0 ∘ Sign_fupd g = Sign_fupd (f0 ∘ g)) ∧
         ∀h g f0. Sign_fupd f0 ∘ Sign_fupd g ∘ h = Sign_fupd (f0 ∘ g) ∘ h) ∧
        ((∀g f0.
            Exponent_fupd f0 ∘ Exponent_fupd g = Exponent_fupd (f0 ∘ g)) ∧
         ∀h g f0.
           Exponent_fupd f0 ∘ Exponent_fupd g ∘ h =
           Exponent_fupd (f0 ∘ g) ∘ h) ∧
        (∀g f0.
           Significand_fupd f0 ∘ Significand_fupd g =
           Significand_fupd (f0 ∘ g)) ∧
        ∀h g f0.
          Significand_fupd f0 ∘ Significand_fupd g ∘ h =
          Significand_fupd (f0 ∘ g) ∘ h
   
   [float_induction]  Theorem
      
      ⊢ ∀P. (∀c c0 c1. P (float c c0 c1)) ⇒ ∀f. P f
   
   [float_infinities]  Theorem
      
      ⊢ ∀x. float_is_infinite x ⇔
            x = float_plus_infinity (:τ # χ) ∨
            x = float_minus_infinity (:τ # χ)
   
   [float_infinities_distinct]  Theorem
      
      ⊢ ∀x. ¬(x = float_plus_infinity (:τ # χ) ∧
             x = float_minus_infinity (:τ # χ))
   
   [float_infinity_negate_abs]  Theorem
      
      ⊢ float_negate (float_plus_infinity (:τ # χ)) =
        float_minus_infinity (:τ # χ) ∧
        float_negate (float_minus_infinity (:τ # χ)) =
        float_plus_infinity (:τ # χ) ∧
        float_abs (float_plus_infinity (:τ # χ)) =
        float_plus_infinity (:τ # χ) ∧
        float_abs (float_minus_infinity (:τ # χ)) =
        float_plus_infinity (:τ # χ)
   
   [float_is_distinct]  Theorem
      
      ⊢ ∀x. ¬(float_is_nan x ∧ float_is_infinite x) ∧
            ¬(float_is_nan x ∧ float_is_normal x) ∧
            ¬(float_is_nan x ∧ float_is_subnormal x) ∧
            ¬(float_is_nan x ∧ float_is_zero x) ∧
            ¬(float_is_infinite x ∧ float_is_normal x) ∧
            ¬(float_is_infinite x ∧ float_is_subnormal x) ∧
            ¬(float_is_infinite x ∧ float_is_zero x) ∧
            ¬(float_is_normal x ∧ float_is_subnormal x) ∧
            ¬(float_is_normal x ∧ float_is_zero x) ∧
            ¬(float_is_subnormal x ∧ float_is_zero x)
   
   [float_is_finite]  Theorem
      
      ⊢ ∀x. float_is_finite x ⇔
            float_is_normal x ∨ float_is_subnormal x ∨ float_is_zero x
   
   [float_is_nan_impl]  Theorem
      
      ⊢ ∀x. float_is_nan x ⇔ ¬float_equal x x
   
   [float_is_zero]  Theorem
      
      ⊢ ∀x. float_is_zero x ⇔ x.Exponent = 0w ∧ x.Significand = 0w
   
   [float_is_zero_impl]  Theorem
      
      ⊢ ∀x. float_is_zero x ⇔ float_equal POS0 x
   
   [float_is_zero_to_real]  Theorem
      
      ⊢ ∀x. float_is_zero x ⇔ float_to_real x = 0
   
   [float_literal_11]  Theorem
      
      ⊢ ∀c11 c01 c1 c12 c02 c2.
          <|Sign := c11; Exponent := c01; Significand := c1|> =
          <|Sign := c12; Exponent := c02; Significand := c2|> ⇔
          c11 = c12 ∧ c01 = c02 ∧ c1 = c2
   
   [float_literal_nchotomy]  Theorem
      
      ⊢ ∀f. ∃c1 c0 c. f = <|Sign := c1; Exponent := c0; Significand := c|>
   
   [float_minus_infinity]  Theorem
      
      ⊢ float_minus_infinity (:τ # χ) =
        <|Sign := 1w; Exponent := UINT_MAXw; Significand := 0w|>
   
   [float_minus_zero]  Theorem
      
      ⊢ NEG0 = <|Sign := 1w; Exponent := 0w; Significand := 0w|>
   
   [float_mul_compute]  Theorem
      
      ⊢ (∀mode x fp_op.
           float_mul mode (float_some_qnan fp_op) x =
           (check_for_signalling [x],
            float_some_qnan (FP_Mul mode (float_some_qnan fp_op) x))) ∧
        (∀mode x fp_op.
           float_mul mode x (float_some_qnan fp_op) =
           (check_for_signalling [x],
            float_some_qnan (FP_Mul mode x (float_some_qnan fp_op)))) ∧
        (∀mode.
           float_mul mode (float_minus_infinity (:τ # χ))
             (float_minus_infinity (:τ # χ)) =
           (clear_flags,float_plus_infinity (:τ # χ))) ∧
        (∀mode.
           float_mul mode (float_minus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (clear_flags,float_minus_infinity (:τ # χ))) ∧
        (∀mode.
           float_mul mode (float_plus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (clear_flags,float_plus_infinity (:τ # χ))) ∧
        ∀mode.
          float_mul mode (float_plus_infinity (:τ # χ))
            (float_minus_infinity (:τ # χ)) =
          (clear_flags,float_minus_infinity (:τ # χ))
   
   [float_mul_finite]  Theorem
      
      ⊢ ∀mode x y r1 r2.
          float_value x = Float r1 ∧ float_value y = Float r2 ⇒
          float_mul mode x y =
          float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 * r2)
   
   [float_mul_finite_minus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_mul mode x (float_minus_infinity (:τ # χ)) =
          if r = 0 then
            (invalidop_flags,
             float_some_qnan
               (FP_Mul mode x (float_minus_infinity (:τ # χ))))
          else
            (clear_flags,
             if x.Sign = 0w then float_minus_infinity (:τ # χ)
             else float_plus_infinity (:τ # χ))
   
   [float_mul_finite_plus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_mul mode x (float_plus_infinity (:τ # χ)) =
          if r = 0 then
            (invalidop_flags,
             float_some_qnan (FP_Mul mode x (float_plus_infinity (:τ # χ))))
          else
            (clear_flags,
             if x.Sign = 0w then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
   
   [float_mul_minus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_mul mode (float_minus_infinity (:τ # χ)) x =
          if r = 0 then
            (invalidop_flags,
             float_some_qnan
               (FP_Mul mode (float_minus_infinity (:τ # χ)) x))
          else
            (clear_flags,
             if x.Sign = 0w then float_minus_infinity (:τ # χ)
             else float_plus_infinity (:τ # χ))
   
   [float_mul_nan]  Theorem
      
      ⊢ ∀mode x y.
          float_value x = NaN ∨ float_value y = NaN ⇒
          float_mul mode x y =
          (check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y))
   
   [float_mul_plus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_mul mode (float_plus_infinity (:τ # χ)) x =
          if r = 0 then
            (invalidop_flags,
             float_some_qnan (FP_Mul mode (float_plus_infinity (:τ # χ)) x))
          else
            (clear_flags,
             if x.Sign = 0w then float_plus_infinity (:τ # χ)
             else float_minus_infinity (:τ # χ))
   
   [float_nchotomy]  Theorem
      
      ⊢ ∀ff. ∃c c0 c1. ff = float c c0 c1
   
   [float_negate_negate]  Theorem
      
      ⊢ ∀x. float_negate (float_negate x) = x
   
   [float_round_bottom]  Theorem
      
      ⊢ ∀mode toneg r.
          round mode r = float_bottom (:τ # χ) ⇒
          float_round mode toneg r = float_bottom (:τ # χ)
   
   [float_round_minus_infinity]  Theorem
      
      ⊢ ∀mode toneg r.
          round mode r = float_minus_infinity (:τ # χ) ⇒
          float_round mode toneg r = float_minus_infinity (:τ # χ)
   
   [float_round_non_zero]  Theorem
      
      ⊢ ∀mode toneg r s e f.
          round mode r = <|Sign := s; Exponent := e; Significand := f|> ∧
          (e ≠ 0w ∨ f ≠ 0w) ⇒
          float_round mode toneg r =
          <|Sign := s; Exponent := e; Significand := f|>
   
   [float_round_plus_infinity]  Theorem
      
      ⊢ ∀mode toneg r.
          round mode r = float_plus_infinity (:τ # χ) ⇒
          float_round mode toneg r = float_plus_infinity (:τ # χ)
   
   [float_round_roundTowardNegative_minus_infinity]  Theorem
      
      ⊢ ∀b y x.
          x < -largest (:τ # χ) ⇒
          float_round roundTowardNegative b x =
          float_minus_infinity (:τ # χ)
   
   [float_round_roundTowardNegative_top]  Theorem
      
      ⊢ ∀b y x.
          largest (:τ # χ) < x ⇒
          float_round roundTowardNegative b x = float_top (:τ # χ)
   
   [float_round_roundTowardPositive_bottom]  Theorem
      
      ⊢ ∀b y x.
          x < -largest (:τ # χ) ⇒
          float_round roundTowardPositive b x = float_bottom (:τ # χ)
   
   [float_round_roundTowardPositive_plus_infinity]  Theorem
      
      ⊢ ∀b y x.
          largest (:τ # χ) < x ⇒
          float_round roundTowardPositive b x =
          float_plus_infinity (:τ # χ)
   
   [float_round_roundTowardZero_bottom]  Theorem
      
      ⊢ ∀b y x.
          x < -largest (:τ # χ) ⇒
          float_round roundTowardZero b x = float_bottom (:τ # χ)
   
   [float_round_roundTowardZero_top]  Theorem
      
      ⊢ ∀b y x.
          largest (:τ # χ) < x ⇒
          float_round roundTowardZero b x = float_top (:τ # χ)
   
   [float_round_to_integral_compute]  Theorem
      
      ⊢ (∀m. float_round_to_integral m (float_minus_infinity (:τ # χ)) =
             float_minus_infinity (:τ # χ)) ∧
        (∀m. float_round_to_integral m (float_plus_infinity (:τ # χ)) =
             float_plus_infinity (:τ # χ)) ∧
        ∀m fp_op.
          float_round_to_integral m (float_some_qnan fp_op) =
          float_some_qnan fp_op
   
   [float_round_top]  Theorem
      
      ⊢ ∀mode toneg r.
          round mode r = float_top (:τ # χ) ⇒
          float_round mode toneg r = float_top (:τ # χ)
   
   [float_sets]  Theorem
      
      ⊢ float_is_zero = {NEG0; POS0} ∧
        float_is_infinite =
        {float_minus_infinity (:τ # χ); float_plus_infinity (:τ # χ)}
   
   [float_sub_compute]  Theorem
      
      ⊢ (∀mode x fp_op.
           float_sub mode (float_some_qnan fp_op) x =
           (check_for_signalling [x],
            float_some_qnan (FP_Sub mode (float_some_qnan fp_op) x))) ∧
        (∀mode x fp_op.
           float_sub mode x (float_some_qnan fp_op) =
           (check_for_signalling [x],
            float_some_qnan (FP_Sub mode x (float_some_qnan fp_op)))) ∧
        (∀mode.
           float_sub mode (float_minus_infinity (:τ # χ))
             (float_minus_infinity (:τ # χ)) =
           (invalidop_flags,
            float_some_qnan
              (FP_Sub mode (float_minus_infinity (:τ # χ))
                 (float_minus_infinity (:τ # χ))))) ∧
        (∀mode.
           float_sub mode (float_minus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (clear_flags,float_minus_infinity (:τ # χ))) ∧
        (∀mode.
           float_sub mode (float_plus_infinity (:τ # χ))
             (float_plus_infinity (:τ # χ)) =
           (invalidop_flags,
            float_some_qnan
              (FP_Sub mode (float_plus_infinity (:τ # χ))
                 (float_plus_infinity (:τ # χ))))) ∧
        ∀mode.
          float_sub mode (float_plus_infinity (:τ # χ))
            (float_minus_infinity (:τ # χ)) =
          (clear_flags,float_plus_infinity (:τ # χ))
   
   [float_sub_finite]  Theorem
      
      ⊢ ∀mode x y r1 r2.
          float_value x = Float r1 ∧ float_value y = Float r2 ⇒
          float_sub mode x y =
          float_round_with_flags mode
            (if r1 = 0 ∧ r2 = 0 ∧ x.Sign ≠ y.Sign then x.Sign = 1w
             else (mode = roundTowardNegative)) (r1 − r2)
   
   [float_sub_finite_minus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_sub mode x (float_minus_infinity (:τ # χ)) =
          (clear_flags,float_plus_infinity (:τ # χ))
   
   [float_sub_finite_plus_infinity]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_sub mode x (float_plus_infinity (:τ # χ)) =
          (clear_flags,float_minus_infinity (:τ # χ))
   
   [float_sub_minus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_sub mode (float_minus_infinity (:τ # χ)) x =
          (clear_flags,float_minus_infinity (:τ # χ))
   
   [float_sub_nan]  Theorem
      
      ⊢ ∀mode x y.
          float_value x = NaN ∨ float_value y = NaN ⇒
          float_sub mode x y =
          (check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y))
   
   [float_sub_plus_infinity_finite]  Theorem
      
      ⊢ ∀mode x r.
          float_value x = Float r ⇒
          float_sub mode (float_plus_infinity (:τ # χ)) x =
          (clear_flags,float_plus_infinity (:τ # χ))
   
   [float_tests]  Theorem
      
      ⊢ (∀s e f.
           float_is_nan <|Sign := s; Exponent := e; Significand := f|> ⇔
           e = -1w ∧ f ≠ 0w) ∧
        (∀s e f.
           float_is_signalling
             <|Sign := s; Exponent := e; Significand := f|> ⇔
           e = -1w ∧ ¬word_msb f ∧ f ≠ 0w) ∧
        (∀s e f.
           float_is_infinite <|Sign := s; Exponent := e; Significand := f|> ⇔
           e = -1w ∧ f = 0w) ∧
        (∀s e f.
           float_is_normal <|Sign := s; Exponent := e; Significand := f|> ⇔
           e ≠ 0w ∧ e ≠ -1w) ∧
        (∀s e f.
           float_is_subnormal
             <|Sign := s; Exponent := e; Significand := f|> ⇔
           e = 0w ∧ f ≠ 0w) ∧
        (∀s e f.
           float_is_zero <|Sign := s; Exponent := e; Significand := f|> ⇔
           e = 0w ∧ f = 0w) ∧
        ∀s e f.
          float_is_finite <|Sign := s; Exponent := e; Significand := f|> ⇔
          e ≠ -1w
   
   [float_to_real]  Theorem
      
      ⊢ ∀s e f.
          float_to_real <|Sign := s; Exponent := e; Significand := f|> =
          (let
             r =
               if e = 0w then
                 2 / &(2 ** bias (:χ)) * (&w2n f / &dimword (:τ))
               else
                 &(2 ** w2n e) / &(2 ** bias (:χ)) *
                 (1 + &w2n f / &dimword (:τ))
           in
             if s = 1w then -r else r)
   
   [float_to_real_EQ0]  Theorem
      
      ⊢ float_to_real f = 0 ⇔ f = POS0 ∨ f = NEG0
   
   [float_to_real_eq]  Theorem
      
      ⊢ ∀x y.
          float_to_real x = float_to_real y ⇔
          x = y ∨ float_is_zero x ∧ float_is_zero y
   
   [float_to_real_negate]  Theorem
      
      ⊢ ∀x. float_to_real (float_negate x) = -float_to_real x
   
   [float_to_real_round0]  Theorem
      
      ⊢ float_to_real (round m 0) = 0
   
   [float_to_real_zeroes]  Theorem
      
      ⊢ float_to_real POS0 = 0 ∧ float_to_real NEG0 = 0
   
   [float_updates_eq_literal]  Theorem
      
      ⊢ ∀f c1 c0 c.
          f with <|Sign := c1; Exponent := c0; Significand := c|> =
          <|Sign := c1; Exponent := c0; Significand := c|>
   
   [float_value_11]  Theorem
      
      ⊢ ∀a a'. Float a = Float a' ⇔ a = a'
   
   [float_value_Axiom]  Theorem
      
      ⊢ ∀f0 f1 f2. ∃fn.
          (∀a. fn (Float a) = f0 a) ∧ fn Infinity = f1 ∧ fn NaN = f2
   
   [float_value_case_cong]  Theorem
      
      ⊢ ∀M M' f v v1.
          M = M' ∧ (∀a. M' = Float a ⇒ f a = f' a) ∧
          (M' = Infinity ⇒ v = v') ∧ (M' = NaN ⇒ v1 = v1') ⇒
          float_value_CASE M f v v1 = float_value_CASE M' f' v' v1'
   
   [float_value_case_eq]  Theorem
      
      ⊢ float_value_CASE x f v v1 = v' ⇔
        (∃r. x = Float r ∧ f r = v') ∨ x = Infinity ∧ v = v' ∨
        x = NaN ∧ v1 = v'
   
   [float_value_distinct]  Theorem
      
      ⊢ (∀a. Float a ≠ Infinity) ∧ (∀a. Float a ≠ NaN) ∧ Infinity ≠ NaN
   
   [float_value_induction]  Theorem
      
      ⊢ ∀P. (∀r. P (Float r)) ∧ P Infinity ∧ P NaN ⇒ ∀f. P f
   
   [float_value_nchotomy]  Theorem
      
      ⊢ ∀ff. (∃r. ff = Float r) ∨ ff = Infinity ∨ ff = NaN
   
   [float_values]  Theorem
      
      ⊢ float_value (float_plus_infinity (:τ # χ)) = Infinity ∧
        float_value (float_minus_infinity (:τ # χ)) = Infinity ∧
        (∀fp_op. float_value (float_some_qnan fp_op) = NaN) ∧
        float_value POS0 = Float 0 ∧ float_value NEG0 = Float 0 ∧
        float_value (float_plus_min (:τ # χ)) =
        Float (2 / 2 pow (bias (:χ) + precision (:τ))) ∧
        float_value (float_minus_min (:τ # χ)) =
        Float (-2 / 2 pow (bias (:χ) + precision (:τ)))
   
   [fp_op_11]  Theorem
      
      ⊢ (∀a0 a1 a0' a1'.
           FP_Sqrt a0 a1 = FP_Sqrt a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
        (∀a0 a1 a2 a0' a1' a2'.
           FP_Add a0 a1 a2 = FP_Add a0' a1' a2' ⇔
           a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
        (∀a0 a1 a2 a0' a1' a2'.
           FP_Sub a0 a1 a2 = FP_Sub a0' a1' a2' ⇔
           a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
        (∀a0 a1 a2 a0' a1' a2'.
           FP_Mul a0 a1 a2 = FP_Mul a0' a1' a2' ⇔
           a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
        (∀a0 a1 a2 a0' a1' a2'.
           FP_Div a0 a1 a2 = FP_Div a0' a1' a2' ⇔
           a0 = a0' ∧ a1 = a1' ∧ a2 = a2') ∧
        (∀a0 a1 a2 a3 a0' a1' a2' a3'.
           FP_MulAdd a0 a1 a2 a3 = FP_MulAdd a0' a1' a2' a3' ⇔
           a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3') ∧
        ∀a0 a1 a2 a3 a0' a1' a2' a3'.
          FP_MulSub a0 a1 a2 a3 = FP_MulSub a0' a1' a2' a3' ⇔
          a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3'
   
   [fp_op_Axiom]  Theorem
      
      ⊢ ∀f0 f1 f2 f3 f4 f5 f6. ∃fn.
          (∀a0 a1. fn (FP_Sqrt a0 a1) = f0 a0 a1) ∧
          (∀a0 a1 a2. fn (FP_Add a0 a1 a2) = f1 a0 a1 a2) ∧
          (∀a0 a1 a2. fn (FP_Sub a0 a1 a2) = f2 a0 a1 a2) ∧
          (∀a0 a1 a2. fn (FP_Mul a0 a1 a2) = f3 a0 a1 a2) ∧
          (∀a0 a1 a2. fn (FP_Div a0 a1 a2) = f4 a0 a1 a2) ∧
          (∀a0 a1 a2 a3. fn (FP_MulAdd a0 a1 a2 a3) = f5 a0 a1 a2 a3) ∧
          ∀a0 a1 a2 a3. fn (FP_MulSub a0 a1 a2 a3) = f6 a0 a1 a2 a3
   
   [fp_op_case_cong]  Theorem
      
      ⊢ ∀M M' f f1 f2 f3 f4 f5 f6.
          M = M' ∧ (∀a0 a1. M' = FP_Sqrt a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
          (∀a0 a1 a2. M' = FP_Add a0 a1 a2 ⇒ f1 a0 a1 a2 = f1' a0 a1 a2) ∧
          (∀a0 a1 a2. M' = FP_Sub a0 a1 a2 ⇒ f2 a0 a1 a2 = f2' a0 a1 a2) ∧
          (∀a0 a1 a2. M' = FP_Mul a0 a1 a2 ⇒ f3 a0 a1 a2 = f3' a0 a1 a2) ∧
          (∀a0 a1 a2. M' = FP_Div a0 a1 a2 ⇒ f4 a0 a1 a2 = f4' a0 a1 a2) ∧
          (∀a0 a1 a2 a3.
             M' = FP_MulAdd a0 a1 a2 a3 ⇒ f5 a0 a1 a2 a3 = f5' a0 a1 a2 a3) ∧
          (∀a0 a1 a2 a3.
             M' = FP_MulSub a0 a1 a2 a3 ⇒ f6 a0 a1 a2 a3 = f6' a0 a1 a2 a3) ⇒
          fp_op_CASE M f f1 f2 f3 f4 f5 f6 =
          fp_op_CASE M' f' f1' f2' f3' f4' f5' f6'
   
   [fp_op_case_eq]  Theorem
      
      ⊢ fp_op_CASE x f f1 f2 f3 f4 f5 f6 = v ⇔
        (∃r f'. x = FP_Sqrt r f' ∧ f r f' = v) ∨
        (∃r f' f0. x = FP_Add r f' f0 ∧ f1 r f' f0 = v) ∨
        (∃r f' f0. x = FP_Sub r f' f0 ∧ f2 r f' f0 = v) ∨
        (∃r f' f0. x = FP_Mul r f' f0 ∧ f3 r f' f0 = v) ∨
        (∃r f' f0. x = FP_Div r f' f0 ∧ f4 r f' f0 = v) ∨
        (∃r f' f0 f1'. x = FP_MulAdd r f' f0 f1' ∧ f5 r f' f0 f1' = v) ∨
        ∃r f' f0 f1'. x = FP_MulSub r f' f0 f1' ∧ f6 r f' f0 f1' = v
   
   [fp_op_distinct]  Theorem
      
      ⊢ (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Add a0' a1' a2) ∧
        (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Sub a0' a1' a2) ∧
        (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Mul a0' a1' a2) ∧
        (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Div a0' a1' a2) ∧
        (∀a3 a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_MulAdd a0' a1' a2 a3) ∧
        (∀a3 a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_MulSub a0' a1' a2 a3) ∧
        (∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Sub a0' a1' a2') ∧
        (∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Mul a0' a1' a2') ∧
        (∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Add a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Add a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
        (∀a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_Mul a0' a1' a2') ∧
        (∀a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Sub a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Sub a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
        (∀a2' a2 a1' a1 a0' a0. FP_Mul a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Mul a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Mul a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Div a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
        (∀a3 a2' a2 a1' a1 a0' a0.
           FP_Div a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
        ∀a3' a3 a2' a2 a1' a1 a0' a0.
          FP_MulAdd a0 a1 a2 a3 ≠ FP_MulSub a0' a1' a2' a3'
   
   [fp_op_induction]  Theorem
      
      ⊢ ∀P. (∀r f. P (FP_Sqrt r f)) ∧ (∀r f f0. P (FP_Add r f f0)) ∧
            (∀r f f0. P (FP_Sub r f f0)) ∧ (∀r f f0. P (FP_Mul r f f0)) ∧
            (∀r f f0. P (FP_Div r f f0)) ∧
            (∀r f f0 f1. P (FP_MulAdd r f f0 f1)) ∧
            (∀r f f0 f1. P (FP_MulSub r f f0 f1)) ⇒
            ∀f. P f
   
   [fp_op_nchotomy]  Theorem
      
      ⊢ ∀ff.
          (∃r f. ff = FP_Sqrt r f) ∨ (∃r f f0. ff = FP_Add r f f0) ∨
          (∃r f f0. ff = FP_Sub r f f0) ∨ (∃r f f0. ff = FP_Mul r f f0) ∨
          (∃r f f0. ff = FP_Div r f f0) ∨
          (∃r f f0 f1. ff = FP_MulAdd r f f0 f1) ∨
          ∃r f f0 f1. ff = FP_MulSub r f f0 f1
   
   [infinity_properties]  Theorem
      
      ⊢ ¬float_is_zero (float_plus_infinity (:τ # χ)) ∧
        ¬float_is_zero (float_minus_infinity (:τ # χ)) ∧
        ¬float_is_finite (float_plus_infinity (:τ # χ)) ∧
        ¬float_is_finite (float_minus_infinity (:τ # χ)) ∧
        ¬float_is_integral (float_plus_infinity (:τ # χ)) ∧
        ¬float_is_integral (float_minus_infinity (:τ # χ)) ∧
        ¬float_is_nan (float_plus_infinity (:τ # χ)) ∧
        ¬float_is_nan (float_minus_infinity (:τ # χ)) ∧
        ¬float_is_normal (float_plus_infinity (:τ # χ)) ∧
        ¬float_is_normal (float_minus_infinity (:τ # χ)) ∧
        ¬float_is_subnormal (float_plus_infinity (:τ # χ)) ∧
        ¬float_is_subnormal (float_minus_infinity (:τ # χ)) ∧
        float_is_infinite (float_plus_infinity (:τ # χ)) ∧
        float_is_infinite (float_minus_infinity (:τ # χ))
   
   [is_closestP_finite_float_exists]  Theorem
      
      ⊢ ∃a. is_closest float_is_finite r a ∧
            ∀b. is_closest float_is_finite r b ∧ P b ⇒ P a
   
   [is_closest_exists]  Theorem
      
      ⊢ s ≠ ∅ ⇒ ∃a. is_closest s r a
   
   [is_closest_finite_AND]  Theorem
      
      ⊢ is_closest float_is_finite r f ∧ Q f ⇒
        is_closest {a | float_is_finite a ∧ Q a} r f
   
   [is_closest_float_is_finite_0]  Theorem
      
      ⊢ is_closest float_is_finite 0 f ⇔ f = POS0 ∨ f = NEG0
   
   [largest]  Theorem
      
      ⊢ largest (:τ # χ) =
        &(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &dimword (:τ)) /
        &(2 ** bias (:χ))
   
   [largest_is_positive]  Theorem
      
      ⊢ 0 ≤ largest (:τ # χ)
   
   [largest_is_top]  Theorem
      
      ⊢ 1 < precision (:χ) ⇒
        largest (:τ # χ) = float_to_real (float_top (:τ # χ))
   
   [largest_lt_threshold]  Theorem
      
      ⊢ largest (:τ # χ) < threshold (:τ # χ)
   
   [le2]  Theorem
      
      ⊢ ∀n m. 2 ≤ n ∧ 2 ≤ m ⇒ 2 ≤ n * m
   
   [less_than_ulp]  Theorem
      
      ⊢ ∀a. abs (float_to_real a) < ulp (:τ # χ) ⇔
            a.Exponent = 0w ∧ a.Significand = 0w
   
   [min_properties]  Theorem
      
      ⊢ ¬float_is_zero (float_plus_min (:τ # χ)) ∧
        float_is_finite (float_plus_min (:τ # χ)) ∧
        (float_is_integral (float_plus_min (:τ # χ)) ⇔
         precision (:χ) = 1 ∧ precision (:τ) = 1) ∧
        ¬float_is_nan (float_plus_min (:τ # χ)) ∧
        ¬float_is_normal (float_plus_min (:τ # χ)) ∧
        float_is_subnormal (float_plus_min (:τ # χ)) ∧
        ¬float_is_infinite (float_plus_min (:τ # χ)) ∧
        ¬float_is_zero (float_minus_min (:τ # χ)) ∧
        float_is_finite (float_minus_min (:τ # χ)) ∧
        (float_is_integral (float_minus_min (:τ # χ)) ⇔
         precision (:χ) = 1 ∧ precision (:τ) = 1) ∧
        ¬float_is_nan (float_minus_min (:τ # χ)) ∧
        ¬float_is_normal (float_minus_min (:τ # χ)) ∧
        float_is_subnormal (float_minus_min (:τ # χ)) ∧
        ¬float_is_infinite (float_minus_min (:τ # χ))
   
   [neg_ulp]  Theorem
      
      ⊢ -ulp (:τ # χ) =
        float_to_real (float_negate (float_plus_min (:τ # χ)))
   
   [num2float_compare_11]  Theorem
      
      ⊢ ∀r r'.
          r < 4 ⇒
          r' < 4 ⇒
          (num2float_compare r = num2float_compare r' ⇔ r = r')
   
   [num2float_compare_ONTO]  Theorem
      
      ⊢ ∀a. ∃r. a = num2float_compare r ∧ r < 4
   
   [num2float_compare_float_compare2num]  Theorem
      
      ⊢ ∀a. num2float_compare (float_compare2num a) = a
   
   [num2float_compare_thm]  Theorem
      
      ⊢ num2float_compare 0 = LT ∧ num2float_compare 1 = EQ ∧
        num2float_compare 2 = GT ∧ num2float_compare 3 = UN
   
   [num2rounding_11]  Theorem
      
      ⊢ ∀r r'. r < 4 ⇒ r' < 4 ⇒ (num2rounding r = num2rounding r' ⇔ r = r')
   
   [num2rounding_ONTO]  Theorem
      
      ⊢ ∀a. ∃r. a = num2rounding r ∧ r < 4
   
   [num2rounding_rounding2num]  Theorem
      
      ⊢ ∀a. num2rounding (rounding2num a) = a
   
   [num2rounding_thm]  Theorem
      
      ⊢ num2rounding 0 = roundTiesToEven ∧
        num2rounding 1 = roundTowardPositive ∧
        num2rounding 2 = roundTowardNegative ∧
        num2rounding 3 = roundTowardZero
   
   [round_roundTiesToEven]  Theorem
      
      ⊢ ∀y x r.
          float_value y = Float r ∧
          (y.Significand = 0w ∧ y.Exponent ≠ 1w ⇒ abs r ≤ abs x) ∧
          2 * abs (r − x) ≤ ULP (y.Exponent,(:τ)) ∧
          (2 * abs (r − x) = ULP (y.Exponent,(:τ)) ⇒
           ¬word_lsb y.Significand) ∧ ulp (:τ # χ) < 2 * abs x ∧
          abs x < threshold (:τ # χ) ⇒
          round roundTiesToEven x = y
   
   [round_roundTiesToEven0]  Theorem
      
      ⊢ ∀y x r.
          float_value y = Float r ∧
          (y.Significand = 0w ∧ y.Exponent ≠ 1w ∧ ¬(abs r ≤ abs x)) ∧
          4 * abs (r − x) ≤ ULP (y.Exponent,(:τ)) ∧
          ulp (:τ # χ) < 2 * abs x ∧ abs x < threshold (:τ # χ) ⇒
          round roundTiesToEven x = y
   
   [round_roundTiesToEven_is_minus_zero]  Theorem
      
      ⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
            float_round roundTiesToEven T x = NEG0
   
   [round_roundTiesToEven_is_plus_zero]  Theorem
      
      ⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
            float_round roundTiesToEven F x = POS0
   
   [round_roundTiesToEven_is_zero]  Theorem
      
      ⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
            round roundTiesToEven x = POS0 ∨ round roundTiesToEven x = NEG0
   
   [round_roundTiesToEven_minus_infinity]  Theorem
      
      ⊢ ∀y x.
          x ≤ -threshold (:τ # χ) ⇒
          round roundTiesToEven x = float_minus_infinity (:τ # χ)
   
   [round_roundTiesToEven_plus_infinity]  Theorem
      
      ⊢ ∀y x.
          threshold (:τ # χ) ≤ x ⇒
          round roundTiesToEven x = float_plus_infinity (:τ # χ)
   
   [round_roundTowardNegative_minus_infinity]  Theorem
      
      ⊢ ∀y x.
          x < -largest (:τ # χ) ⇒
          round roundTowardNegative x = float_minus_infinity (:τ # χ)
   
   [round_roundTowardNegative_top]  Theorem
      
      ⊢ ∀y x.
          largest (:τ # χ) < x ⇒
          round roundTowardNegative x = float_top (:τ # χ)
   
   [round_roundTowardPositive_bottom]  Theorem
      
      ⊢ ∀y x.
          x < -largest (:τ # χ) ⇒
          round roundTowardPositive x = float_bottom (:τ # χ)
   
   [round_roundTowardPositive_plus_infinity]  Theorem
      
      ⊢ ∀y x.
          largest (:τ # χ) < x ⇒
          round roundTowardPositive x = float_plus_infinity (:τ # χ)
   
   [round_roundTowardZero]  Theorem
      
      ⊢ ∀y x r.
          float_value y = Float r ∧ abs (r − x) < ULP (y.Exponent,(:τ)) ∧
          abs r ≤ abs x ∧ ulp (:τ # χ) ≤ abs x ∧ abs x ≤ largest (:τ # χ) ⇒
          round roundTowardZero x = y
   
   [round_roundTowardZero_bottom]  Theorem
      
      ⊢ ∀y x.
          x < -largest (:τ # χ) ⇒
          round roundTowardZero x = float_bottom (:τ # χ)
   
   [round_roundTowardZero_is_minus_zero]  Theorem
      
      ⊢ ∀x. abs x < ulp (:τ # χ) ⇒ float_round roundTowardZero T x = NEG0
   
   [round_roundTowardZero_is_plus_zero]  Theorem
      
      ⊢ ∀x. abs x < ulp (:τ # χ) ⇒ float_round roundTowardZero F x = POS0
   
   [round_roundTowardZero_is_zero]  Theorem
      
      ⊢ ∀x. abs x < ulp (:τ # χ) ⇒
            round roundTowardZero x = POS0 ∨ round roundTowardZero x = NEG0
   
   [round_roundTowardZero_top]  Theorem
      
      ⊢ ∀y x.
          largest (:τ # χ) < x ⇒
          round roundTowardZero x = float_top (:τ # χ)
   
   [rounding2num_11]  Theorem
      
      ⊢ ∀a a'. rounding2num a = rounding2num a' ⇔ a = a'
   
   [rounding2num_ONTO]  Theorem
      
      ⊢ ∀r. r < 4 ⇔ ∃a. r = rounding2num a
   
   [rounding2num_num2rounding]  Theorem
      
      ⊢ ∀r. r < 4 ⇔ rounding2num (num2rounding r) = r
   
   [rounding2num_thm]  Theorem
      
      ⊢ rounding2num roundTiesToEven = 0 ∧
        rounding2num roundTowardPositive = 1 ∧
        rounding2num roundTowardNegative = 2 ∧
        rounding2num roundTowardZero = 3
   
   [rounding_Axiom]  Theorem
      
      ⊢ ∀x0 x1 x2 x3. ∃f.
          f roundTiesToEven = x0 ∧ f roundTowardPositive = x1 ∧
          f roundTowardNegative = x2 ∧ f roundTowardZero = x3
   
   [rounding_EQ_rounding]  Theorem
      
      ⊢ ∀a a'. a = a' ⇔ rounding2num a = rounding2num a'
   
   [rounding_case_cong]  Theorem
      
      ⊢ ∀M M' v0 v1 v2 v3.
          M = M' ∧ (M' = roundTiesToEven ⇒ v0 = v0') ∧
          (M' = roundTowardPositive ⇒ v1 = v1') ∧
          (M' = roundTowardNegative ⇒ v2 = v2') ∧
          (M' = roundTowardZero ⇒ v3 = v3') ⇒
          (case M of
             roundTiesToEven => v0
           | roundTowardPositive => v1
           | roundTowardNegative => v2
           | roundTowardZero => v3) =
          case M' of
            roundTiesToEven => v0'
          | roundTowardPositive => v1'
          | roundTowardNegative => v2'
          | roundTowardZero => v3'
   
   [rounding_case_def]  Theorem
      
      ⊢ (∀v0 v1 v2 v3.
           (case roundTiesToEven of
              roundTiesToEven => v0
            | roundTowardPositive => v1
            | roundTowardNegative => v2
            | roundTowardZero => v3) =
           v0) ∧
        (∀v0 v1 v2 v3.
           (case roundTowardPositive of
              roundTiesToEven => v0
            | roundTowardPositive => v1
            | roundTowardNegative => v2
            | roundTowardZero => v3) =
           v1) ∧
        (∀v0 v1 v2 v3.
           (case roundTowardNegative of
              roundTiesToEven => v0
            | roundTowardPositive => v1
            | roundTowardNegative => v2
            | roundTowardZero => v3) =
           v2) ∧
        ∀v0 v1 v2 v3.
          (case roundTowardZero of
             roundTiesToEven => v0
           | roundTowardPositive => v1
           | roundTowardNegative => v2
           | roundTowardZero => v3) =
          v3
   
   [rounding_case_eq]  Theorem
      
      ⊢ (case x of
           roundTiesToEven => v0
         | roundTowardPositive => v1
         | roundTowardNegative => v2
         | roundTowardZero => v3) =
        v ⇔
        x = roundTiesToEven ∧ v0 = v ∨ x = roundTowardPositive ∧ v1 = v ∨
        x = roundTowardNegative ∧ v2 = v ∨ x = roundTowardZero ∧ v3 = v
   
   [rounding_distinct]  Theorem
      
      ⊢ roundTiesToEven ≠ roundTowardPositive ∧
        roundTiesToEven ≠ roundTowardNegative ∧
        roundTiesToEven ≠ roundTowardZero ∧
        roundTowardPositive ≠ roundTowardNegative ∧
        roundTowardPositive ≠ roundTowardZero ∧
        roundTowardNegative ≠ roundTowardZero
   
   [rounding_induction]  Theorem
      
      ⊢ ∀P. P roundTiesToEven ∧ P roundTowardNegative ∧
            P roundTowardPositive ∧ P roundTowardZero ⇒
            ∀a. P a
   
   [rounding_nchotomy]  Theorem
      
      ⊢ ∀a. a = roundTiesToEven ∨ a = roundTowardPositive ∨
            a = roundTowardNegative ∨ a = roundTowardZero
   
   [sign_not_zero]  Theorem
      
      ⊢ ∀s. -1 pow w2n s ≠ 0
   
   [some_nan_properties]  Theorem
      
      ⊢ ∀fp_op.
          ¬float_is_zero (float_some_qnan fp_op) ∧
          ¬float_is_finite (float_some_qnan fp_op) ∧
          ¬float_is_integral (float_some_qnan fp_op) ∧
          float_is_nan (float_some_qnan fp_op) ∧
          ¬float_is_signalling (float_some_qnan fp_op) ∧
          ¬float_is_normal (float_some_qnan fp_op) ∧
          ¬float_is_subnormal (float_some_qnan fp_op) ∧
          ¬float_is_infinite (float_some_qnan fp_op)
   
   [threshold]  Theorem
      
      ⊢ threshold (:τ # χ) =
        &(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &(2 * dimword (:τ))) /
        &(2 ** bias (:χ))
   
   [threshold_is_positive]  Theorem
      
      ⊢ 0 < threshold (:τ # χ)
   
   [top_properties]  Theorem
      
      ⊢ ¬float_is_zero (float_top (:τ # χ)) ∧
        float_is_finite (float_top (:τ # χ)) ∧
        ¬float_is_nan (float_top (:τ # χ)) ∧
        (float_is_normal (float_top (:τ # χ)) ⇔ precision (:χ) ≠ 1) ∧
        (float_is_subnormal (float_top (:τ # χ)) ⇔ precision (:χ) = 1) ∧
        ¬float_is_infinite (float_top (:τ # χ))
   
   [ulp]  Theorem
      
      ⊢ ulp (:τ # χ) = float_to_real (float_plus_min (:τ # χ))
   
   [ulp_lt_ULP]  Theorem
      
      ⊢ ∀e. ulp (:τ # χ) ≤ ULP (e,(:τ))
   
   [ulp_lt_largest]  Theorem
      
      ⊢ ulp (:τ # χ) < largest (:τ # χ)
   
   [ulp_lt_threshold]  Theorem
      
      ⊢ ulp (:τ # χ) < threshold (:τ # χ)
   
   [ulp_nonzero]  Theorem
      
      ⊢ ulp (:τ # χ) ≠ 0
   
   [ulp_positive]  Theorem
      
      ⊢ 0 < ulp (:τ # χ) ∧ 0 ≤ ulp (:τ # χ) ∧ ¬(ulp (:τ # χ) < 0) ∧
        ¬(ulp (:τ # χ) ≤ 0)
   
   [zero_le_pos_div_twopow]  Theorem
      
      ⊢ ∀m n. 0 ≤ &m / 2 pow n
   
   [zero_le_twopow]  Theorem
      
      ⊢ ∀n. 0 ≤ 2 pow n
   
   [zero_lt_twopow]  Theorem
      
      ⊢ ∀n. 0 < 2 pow n
   
   [zero_neq_twopow]  Theorem
      
      ⊢ ∀n. 2 pow n ≠ 0
   
   [zero_properties]  Theorem
      
      ⊢ float_is_zero POS0 ∧ float_is_zero NEG0 ∧ float_is_finite POS0 ∧
        float_is_finite NEG0 ∧ float_is_integral POS0 ∧
        float_is_integral NEG0 ∧ ¬float_is_nan POS0 ∧ ¬float_is_nan NEG0 ∧
        ¬float_is_normal POS0 ∧ ¬float_is_normal NEG0 ∧
        ¬float_is_subnormal POS0 ∧ ¬float_is_subnormal NEG0 ∧
        ¬float_is_infinite POS0 ∧ ¬float_is_infinite NEG0
   
   [zero_to_real]  Theorem
      
      ⊢ float_to_real POS0 = 0 ∧ float_to_real NEG0 = 0
   
   [zeroes_are_finite_floats]  Theorem
      
      ⊢ float_is_finite POS0 ∧ float_is_finite NEG0
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1