Theory binary_ieeeProps

⊢ ∀x. mantissa x =
      if x.Exponent = 0w then w2n x.Significand
      else 2 ** precision (:τ) + w2n x.Significand

⊢ ∀f. f.Sign = 0w ∨ f.Sign = 1w

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

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

⊢ f2r f = sign f * &mantissa f * ulpᶠ f

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

⊢ float_value f = Float r ⇒ f2r f = r

⊢ is_closest float_is_finite 0 b ⇔ f2r b = 0

⊢ ¬(largest (:α # β) < 0) ∧ largest (:α # β) ≠ 0 ∧ 0 < largest (:α # β) ∧
  0 ≤ largest (:α # β) ∧ ¬(largest (:α # β) ≤ 0)

⊢ mantissa f < 2 * 2 ** precision (:α)

⊢ r = -(2 pow k * &x) / 2 pow (bias (:χ) + precision (:τ)) ∧ 0 < k ∧
  k < 2 ** precision (:χ) − 1 ∧ x < 2 ** (precision (:τ) + 1) ⇒
  ∃f. float_value f = Float r

⊢ r = 2 pow k * &x / 2 pow (bias (:χ) + precision (:τ)) ∧ 0 < k ∧
  k < 2 ** precision (:χ) − 1 ∧ x < 2 ** (precision (:τ) + 1) ⇒
  ∃f. float_value f = Float r

⊢ abs r = 2 pow k * &x / 2 pow (bias (:χ) + precision (:τ)) ∧ 0 < k ∧
  k < 2 ** precision (:χ) − 1 ∧ x < 2 ** (precision (:τ) + 1) ⇒
  ∃f. float_value f = Float r

⊢ 2 ≤ precision (:β) ∧ float_is_finite f ⇒
  ∃f'. float_is_finite f' ∧ round m (f2r f) = f' ∧ f2r f' = f2r f

⊢ 2 ≤ precision (:β) ∧ float_is_finite f ∧ f2r f ≠ 0 ⇒ round m (f2r f) = f

⊢ 2 ≤ precision (:β) ⇒ round m 0 = POS0 ∨ round m 0 = NEG0

⊢ 2 ≤ precision (:τ) ∧ float_value b = Float rb ∧
  rr = real_of_int i * ulpᶠ b ∧ abs rr ≤ abs rb ⇒
  ∃r. float_value r = Float rr

⊢ ¬(threshold (:α # β) < 0) ∧ threshold (:α # β) ≠ 0 ∧
  0 < threshold (:α # β) ∧ 0 ≤ threshold (:α # β) ∧
  ¬(threshold (:α # β) ≤ 0)

⊢ float_is_finite f ∧ 2 ≤ precision (:τ) ∧ abs r = &n * ulpᶠ f ∧
  n ≤ 2 ** precision (:χ) ⇒
  ∃f'. float_value f' = Float r