Theory lift_ieee

⊢ ∀x. error (:τ # χ) x = float_to_real (round roundTiesToEven x) − x

⊢ ∀x. normalizes (:τ # χ) x ⇔
      1 < bias (:χ) ∧ (2 pow (bias (:χ) − 1))⁻¹ ≤ abs x ∧
      abs x < threshold (:τ # χ)

⊢ ∀f. sqrtable f ⇔ (f.Sign = 0w) ∨ (f = NEG0)

⊢ ∀x. abs x < threshold (:τ # χ) ∧ abs x < 2 * 1 / 2 pow (bias (:χ) − 1) ∧
      1 < bias (:χ) ⇒
      ∃e. abs (float_to_real (round roundTiesToEven x) − x) ≤ e ∧
          e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ))

⊢ ∀p s x. s ≠ ∅ ⇒ closest_such p s x ∈ s

⊢ ∀p s x. s ≠ ∅ ⇒ is_closest s x (closest_such p s x)

⊢ ∀p s x.
    s ≠ ∅ ⇒
    is_closest s x (closest_such p s x) ∧
    ((∃b. is_closest s x b ∧ p b) ⇒ p (closest_such p s x))

⊢ ∀a x.
    abs x < threshold (:τ # χ) ∧ float_is_finite a ⇒
    abs (error (:τ # χ) x) ≤ abs (float_to_real a − x)

⊢ ∀fracw x.
    0 ≤ x ∧ x < 1 ∧ 0 < fracw ⇒
    ∃n. n < 2 ** fracw ∧ &n / 2 pow fracw ≤ x ∧ x < &SUC n / 2 pow fracw

⊢ ∀fracw x.
    0 ≤ x ∧ x < 1 ∧ 0 < fracw ⇒
    ∃n. n ≤ 2 ** fracw ∧ abs (x − &n / 2 pow fracw) ≤ (2 pow (fracw + 1))⁻¹

⊢ ∀fracw x.
    1 ≤ x ∧ x < 2 ∧ 0 < fracw ⇒
    ∃n. n ≤ 2 ** fracw ∧
        abs (1 + &n / 2 pow fracw − x) ≤ (2 pow (fracw + 1))⁻¹

⊢ ∀a x. float_is_finite a ∧ (float_to_real a = x) ⇒ (error (:τ # χ) x = 0)

⊢ ∀f. float_is_finite f ⇒
      ¬(float_to_real f ≤ -threshold (:α # β)) ∧
      ¬(float_to_real f ≥ threshold (:α # β))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_add roundTiesToEven a b)) ∧
    (float_to_real (SND (float_add roundTiesToEven a b)) =
     float_to_real a + float_to_real b +
     error (:τ # χ) (float_to_real a + float_to_real b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_add roundTiesToEven a b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    normalizes (:τ # χ) (float_to_real a + float_to_real b) ⇒
    float_is_finite (SND (float_add roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
        (float_to_real (SND (float_add roundTiesToEven a b)) =
         (float_to_real a + float_to_real b) * (1 + e))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a + float_to_real b) <
    2 pow 1 / 2 pow (bias (:χ) − 1) ∧
    abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ∧
    1 < bias (:χ) ⇒
    float_is_finite (SND (float_add roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_add roundTiesToEven a b)) =
         float_to_real a + float_to_real b + e)

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
    abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_div roundTiesToEven a b)) ∧
    (float_to_real (SND (float_div roundTiesToEven a b)) =
     float_to_real a / float_to_real b +
     error (:τ # χ) (float_to_real a / float_to_real b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
    abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_div roundTiesToEven a b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
    normalizes (:τ # χ) (float_to_real a / float_to_real b) ⇒
    float_is_finite (SND (float_div roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
        (float_to_real (SND (float_div roundTiesToEven a b)) =
         float_to_real a / float_to_real b * (1 + e))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
    abs (float_to_real a / float_to_real b) <
    2 pow 1 / 2 pow (bias (:χ) − 1) ∧
    abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ∧
    1 < bias (:χ) ⇒
    float_is_finite (SND (float_div roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_div roundTiesToEven a b)) =
         float_to_real a / float_to_real b + e)

⊢ ∀x y.
    float_is_finite x ∧ float_is_finite y ⇒
    (float_equal x y ⇔ (float_to_real x = float_to_real y))

⊢ ∀x. float_equal x x ⇔ ¬float_is_nan x

⊢ FINITE 𝕌(:(τ, χ) float)

⊢ ∀x y.
    float_is_finite x ∧ float_is_finite y ⇒
    (float_greater_equal x y ⇔ float_to_real x ≥ float_to_real y)

⊢ ∀x y.
    float_is_finite x ∧ float_is_finite y ⇒
    (float_greater_than x y ⇔ float_to_real x > float_to_real y)

⊢ ∀x y.
    float_is_finite x ∧ float_is_finite y ⇒
    (float_less_equal x y ⇔ float_to_real x ≤ float_to_real y)

⊢ ∀x y.
    float_is_finite x ∧ float_is_finite y ⇒
    (float_less_than x y ⇔ float_to_real x < float_to_real y)

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_mul roundTiesToEven a b)) ∧
    (float_to_real (SND (float_mul roundTiesToEven a b)) =
     float_to_real a * float_to_real b +
     error (:τ # χ) (float_to_real a * float_to_real b))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    abs (float_to_real a * float_to_real b + float_to_real c) <
    threshold (:τ # χ) ⇒
    float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
    (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
     float_to_real a * float_to_real b + float_to_real c +
     error (:τ # χ) (float_to_real a * float_to_real b + float_to_real c))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    abs (float_to_real a * float_to_real b + float_to_real c) <
    threshold (:τ # χ) ⇒
    float_is_finite (SND (float_mul_add roundTiesToEven a b c))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    normalizes (:τ # χ)
      (float_to_real a * float_to_real b + float_to_real c) ⇒
    float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
    ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
        (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
         (float_to_real a * float_to_real b + float_to_real c) * (1 + e))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    abs (float_to_real a * float_to_real b + float_to_real c) <
    2 pow 1 / 2 pow (bias (:χ) − 1) ∧
    abs (float_to_real a * float_to_real b + float_to_real c) <
    threshold (:τ # χ) ∧ 1 < bias (:χ) ⇒
    float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
    ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
         float_to_real a * float_to_real b + float_to_real c + e)

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_mul roundTiesToEven a b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    normalizes (:τ # χ) (float_to_real a * float_to_real b) ⇒
    float_is_finite (SND (float_mul roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
        (float_to_real (SND (float_mul roundTiesToEven a b)) =
         float_to_real a * float_to_real b * (1 + e))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a * float_to_real b) <
    2 pow 1 / 2 pow (bias (:χ) − 1) ∧
    abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ∧
    1 < bias (:χ) ⇒
    float_is_finite (SND (float_mul roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_mul roundTiesToEven a b)) =
         float_to_real a * float_to_real b + e)

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    abs (float_to_real a * float_to_real b − float_to_real c) <
    threshold (:τ # χ) ⇒
    float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
    (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
     float_to_real a * float_to_real b − float_to_real c +
     error (:τ # χ) (float_to_real a * float_to_real b − float_to_real c))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    abs (float_to_real a * float_to_real b − float_to_real c) <
    threshold (:τ # χ) ⇒
    float_is_finite (SND (float_mul_sub roundTiesToEven a b c))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    normalizes (:τ # χ)
      (float_to_real a * float_to_real b − float_to_real c) ⇒
    float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
    ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
        (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
         (float_to_real a * float_to_real b − float_to_real c) * (1 + e))

⊢ ∀a b c.
    float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
    abs (float_to_real a * float_to_real b − float_to_real c) <
    2 pow 1 / 2 pow (bias (:χ) − 1) ∧
    abs (float_to_real a * float_to_real b − float_to_real c) <
    threshold (:τ # χ) ∧ 1 < bias (:χ) ⇒
    float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
    ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
         float_to_real a * float_to_real b − float_to_real c + e)

⊢ ∀b x.
    abs x < threshold (:τ # χ) ⇒
    float_is_finite (float_round roundTiesToEven b x)

⊢ ∀a. float_is_finite a ∧ sqrtable a ∧
      abs (sqrt (float_to_real a)) < threshold (:τ # χ) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
      (float_to_real (SND (float_sqrt roundTiesToEven a)) =
       sqrt (float_to_real a) + error (:τ # χ) (sqrt (float_to_real a)))

⊢ ∀a. float_is_finite a ∧ sqrtable a ∧
      abs (sqrt (float_to_real a)) < threshold (:τ # χ) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a))

⊢ ∀a. float_is_finite a ∧ sqrtable a ∧
      normalizes (:τ # χ) (sqrt (float_to_real a)) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
      ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          (float_to_real (SND (float_sqrt roundTiesToEven a)) =
           sqrt (float_to_real a) * (1 + e))

⊢ ∀a. float_is_finite a ∧ sqrtable a ∧
      abs (sqrt (float_to_real a)) < 2 pow 1 / 2 pow (bias (:χ) − 1) ∧
      abs (sqrt (float_to_real a)) < threshold (:τ # χ) ∧ 1 < bias (:χ) ⇒
      float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
      ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
          (float_to_real (SND (float_sqrt roundTiesToEven a)) =
           sqrt (float_to_real a) + e)

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_sub roundTiesToEven a b)) ∧
    (float_to_real (SND (float_sub roundTiesToEven a b)) =
     float_to_real a − float_to_real b +
     error (:τ # χ) (float_to_real a − float_to_real b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ⇒
    float_is_finite (SND (float_sub roundTiesToEven a b))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    normalizes (:τ # χ) (float_to_real a − float_to_real b) ⇒
    float_is_finite (SND (float_sub roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
        (float_to_real (SND (float_sub roundTiesToEven a b)) =
         (float_to_real a − float_to_real b) * (1 + e))

⊢ ∀a b.
    float_is_finite a ∧ float_is_finite b ∧
    abs (float_to_real a − float_to_real b) <
    2 pow 1 / 2 pow (bias (:χ) − 1) ∧
    abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ∧
    1 < bias (:χ) ⇒
    float_is_finite (SND (float_sub roundTiesToEven a b)) ∧
    ∃e. abs e ≤ 1 / 2 pow (bias (:χ) + dimindex (:τ)) ∧
        (float_to_real (SND (float_sub roundTiesToEven a b)) =
         float_to_real a − float_to_real b + e)

⊢ ∀x. float_is_finite x ⇒ abs (float_to_real x) ≤ largest (:τ # χ)

⊢ float_to_real (real_to_float roundTiesToEven 0) = 0

⊢ ∀x. float_is_finite x ⇒ abs (float_to_real x) < threshold (:τ # χ)

⊢ ∀p x. float_is_finite (closest_such p {a | float_is_finite a} x)

⊢ FINITE {a | float_is_finite a}

⊢ {a | float_is_finite a} ≠ ∅

⊢ ∀ff P.
    2 * abs ff ≤ ulp (:α # β) ⇒
    (float_to_real (float_round roundTiesToEven P ff) = 0)

⊢ ∀f. float_is_finite f ∧ ¬float_is_zero f ⇒
      (real_to_float roundTiesToEven (float_to_real f) = f)

⊢ ∀x. normalizes (:τ # χ) x ⇒
      ∃e. abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
          (float_to_real (round roundTiesToEven x) = x * (1 + e))

⊢ ∀f. float_is_finite f ∧ ¬float_is_zero f ⇒
      (round roundTiesToEven (float_to_real f) = f)