Package hol-floating-point: HOL floating point theories

Information

namehol-floating-point
version1.1
descriptionHOL floating point theories
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksumbadaaa151d79d4d7f6fc3966e93133726b89c39d
requiresbase
hol-base
hol-words
hol-integer
hol-real
showData.Bool
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Type Operators

Defined Constants

Theorems

binary_ieee.LT = binary_ieee.num2float_compare 0

binary_ieee.roundTiesToEven = binary_ieee.num2rounding 0

binary_ieee.EQ = binary_ieee.num2float_compare 1

binary_ieee.GT = binary_ieee.num2float_compare (arithmetic.BIT2 0)

binary_ieee.roundTowardNegative =
  binary_ieee.num2rounding (arithmetic.BIT2 0)

binary_ieee.roundTowardPositive = binary_ieee.num2rounding 1

machine_ieee.fp16_bottom =
  machine_ieee.float_to_fp16 (binary_ieee.float_bottom bool.the_value)

machine_ieee.fp16_negInf =
  machine_ieee.float_to_fp16
    (binary_ieee.float_minus_infinity bool.the_value)

machine_ieee.fp16_negMin =
  machine_ieee.float_to_fp16 (binary_ieee.float_minus_min bool.the_value)

machine_ieee.fp16_negZero =
  machine_ieee.float_to_fp16 (binary_ieee.float_minus_zero bool.the_value)

machine_ieee.fp16_posInf =
  machine_ieee.float_to_fp16
    (binary_ieee.float_plus_infinity bool.the_value)

machine_ieee.fp16_posMin =
  machine_ieee.float_to_fp16 (binary_ieee.float_plus_min bool.the_value)

machine_ieee.fp16_posZero =
  machine_ieee.float_to_fp16 (binary_ieee.float_plus_zero bool.the_value)

machine_ieee.fp16_top =
  machine_ieee.float_to_fp16 (binary_ieee.float_top bool.the_value)

machine_ieee.fp32_bottom =
  machine_ieee.float_to_fp32 (binary_ieee.float_bottom bool.the_value)

machine_ieee.fp32_negInf =
  machine_ieee.float_to_fp32
    (binary_ieee.float_minus_infinity bool.the_value)

machine_ieee.fp32_negMin =
  machine_ieee.float_to_fp32 (binary_ieee.float_minus_min bool.the_value)

machine_ieee.fp32_negZero =
  machine_ieee.float_to_fp32 (binary_ieee.float_minus_zero bool.the_value)

machine_ieee.fp32_posInf =
  machine_ieee.float_to_fp32
    (binary_ieee.float_plus_infinity bool.the_value)

machine_ieee.fp32_posMin =
  machine_ieee.float_to_fp32 (binary_ieee.float_plus_min bool.the_value)

machine_ieee.fp32_posZero =
  machine_ieee.float_to_fp32 (binary_ieee.float_plus_zero bool.the_value)

machine_ieee.fp32_top =
  machine_ieee.float_to_fp32 (binary_ieee.float_top bool.the_value)

machine_ieee.fp16_isFinite =
  binary_ieee.float_is_finite machine_ieee.fp16_to_float

machine_ieee.fp16_isInfinite =
  binary_ieee.float_is_infinite machine_ieee.fp16_to_float

machine_ieee.fp16_isIntegral =
  binary_ieee.float_is_integral machine_ieee.fp16_to_float

machine_ieee.fp16_isNan =
  binary_ieee.float_is_nan machine_ieee.fp16_to_float

machine_ieee.fp16_isNormal =
  binary_ieee.float_is_normal machine_ieee.fp16_to_float

machine_ieee.fp16_isSubnormal =
  binary_ieee.float_is_subnormal machine_ieee.fp16_to_float

machine_ieee.fp16_isZero =
  binary_ieee.float_is_zero machine_ieee.fp16_to_float

machine_ieee.fp16_to_real =
  binary_ieee.float_value machine_ieee.fp16_to_float

machine_ieee.fp64_bottom =
  machine_ieee.float_to_fp64 (binary_ieee.float_bottom bool.the_value)

machine_ieee.fp64_negInf =
  machine_ieee.float_to_fp64
    (binary_ieee.float_minus_infinity bool.the_value)

machine_ieee.fp64_negMin =
  machine_ieee.float_to_fp64 (binary_ieee.float_minus_min bool.the_value)

machine_ieee.fp64_negZero =
  machine_ieee.float_to_fp64 (binary_ieee.float_minus_zero bool.the_value)

machine_ieee.fp64_posInf =
  machine_ieee.float_to_fp64
    (binary_ieee.float_plus_infinity bool.the_value)

machine_ieee.fp64_posMin =
  machine_ieee.float_to_fp64 (binary_ieee.float_plus_min bool.the_value)

machine_ieee.fp64_posZero =
  machine_ieee.float_to_fp64 (binary_ieee.float_plus_zero bool.the_value)

machine_ieee.fp64_top =
  machine_ieee.float_to_fp64 (binary_ieee.float_top bool.the_value)

machine_ieee.fp32_isFinite =
  binary_ieee.float_is_finite machine_ieee.fp32_to_float

machine_ieee.fp32_isInfinite =
  binary_ieee.float_is_infinite machine_ieee.fp32_to_float

machine_ieee.fp32_isIntegral =
  binary_ieee.float_is_integral machine_ieee.fp32_to_float

machine_ieee.fp32_isNan =
  binary_ieee.float_is_nan machine_ieee.fp32_to_float

machine_ieee.fp32_isNormal =
  binary_ieee.float_is_normal machine_ieee.fp32_to_float

machine_ieee.fp32_isSubnormal =
  binary_ieee.float_is_subnormal machine_ieee.fp32_to_float

machine_ieee.fp32_isZero =
  binary_ieee.float_is_zero machine_ieee.fp32_to_float

machine_ieee.fp32_to_real =
  binary_ieee.float_value machine_ieee.fp32_to_float

binary_ieee.closest = binary_ieee.closest_such (const )

machine_ieee.fp64_isFinite =
  binary_ieee.float_is_finite machine_ieee.fp64_to_float

machine_ieee.fp64_isInfinite =
  binary_ieee.float_is_infinite machine_ieee.fp64_to_float

machine_ieee.fp64_isIntegral =
  binary_ieee.float_is_integral machine_ieee.fp64_to_float

machine_ieee.fp64_isNan =
  binary_ieee.float_is_nan machine_ieee.fp64_to_float

machine_ieee.fp64_isNormal =
  binary_ieee.float_is_normal machine_ieee.fp64_to_float

machine_ieee.fp64_isSubnormal =
  binary_ieee.float_is_subnormal machine_ieee.fp64_to_float

machine_ieee.fp64_isZero =
  binary_ieee.float_is_zero machine_ieee.fp64_to_float

machine_ieee.fp64_to_real =
  binary_ieee.float_value machine_ieee.fp64_to_float

Number.Real.< (binary_ieee.ulp bool.the_value)
    (binary_ieee.largest bool.the_value)

Number.Real.< (binary_ieee.ulp bool.the_value)
    (binary_ieee.threshold bool.the_value)

Number.Real.< 0 (binary_ieee.threshold bool.the_value)

Number.Real.≤ 0 (binary_ieee.largest bool.the_value)

x. binary_ieee.float_compare_size x = 0

x. binary_ieee.rounding_size x = 0

binary_ieee.UN = binary_ieee.num2float_compare 3

binary_ieee.roundTowardZero = binary_ieee.num2rounding 3

machine_ieee.fp64_to_fp32 =
  machine_ieee.convert machine_ieee.fp64_to_float
    machine_ieee.float_to_fp32 machine_ieee.real_to_fp32

binary_ieee.ulp bool.the_value =
  binary_ieee.float_to_real (binary_ieee.float_plus_min bool.the_value)

binary_ieee.float_bottom bool.the_value =
  binary_ieee.float_negate (binary_ieee.float_top bool.the_value)

binary_ieee.float_minus_infinity bool.the_value =
  binary_ieee.float_negate (binary_ieee.float_plus_infinity bool.the_value)

binary_ieee.float_minus_min bool.the_value =
  binary_ieee.float_negate (binary_ieee.float_plus_min bool.the_value)

binary_ieee.float_minus_zero bool.the_value =
  binary_ieee.float_negate (binary_ieee.float_plus_zero bool.the_value)

a. binary_ieee.num2float_compare (binary_ieee.float_compare2num a) = a

a. binary_ieee.num2rounding (binary_ieee.rounding2num a) = a

x. binary_ieee.float_negate (binary_ieee.float_negate x) = x

x. machine_ieee.float_to_fp16 (machine_ieee.fp16_to_float x) = x

x. machine_ieee.fp16_to_float (machine_ieee.float_to_fp16 x) = x

x. machine_ieee.float_to_fp32 (machine_ieee.fp32_to_float x) = x

x. machine_ieee.float_to_fp64 (machine_ieee.fp64_to_float x) = x

x. machine_ieee.fp32_to_float (machine_ieee.float_to_fp32 x) = x

x. machine_ieee.fp64_to_float (machine_ieee.float_to_fp64 x) = x

binary_ieee.float_some_nan bool.the_value =
  select a. binary_ieee.float_is_nan a

x. y. x = machine_ieee.float_to_fp16 y

x. y. x = machine_ieee.fp16_to_float y

x. y. x = machine_ieee.float_to_fp32 y

x. y. x = machine_ieee.float_to_fp64 y

x. y. x = machine_ieee.fp32_to_float y

x. y. x = machine_ieee.fp64_to_float y

machine_ieee.fp16_abs =
  machine_ieee.float_to_fp16
  (binary_ieee.float_abs machine_ieee.fp16_to_float)

machine_ieee.fp16_abs1985 =
  machine_ieee.float_to_fp16
  (binary_ieee.float_abs1985 machine_ieee.fp16_to_float)

machine_ieee.fp16_negate =
  machine_ieee.float_to_fp16
  (binary_ieee.float_negate machine_ieee.fp16_to_float)

machine_ieee.fp16_negate1985 =
  machine_ieee.float_to_fp16
  (binary_ieee.float_negate1985 machine_ieee.fp16_to_float)

machine_ieee.fp32_abs =
  machine_ieee.float_to_fp32
  (binary_ieee.float_abs machine_ieee.fp32_to_float)

machine_ieee.fp32_abs1985 =
  machine_ieee.float_to_fp32
  (binary_ieee.float_abs1985 machine_ieee.fp32_to_float)

machine_ieee.fp32_negate =
  machine_ieee.float_to_fp32
  (binary_ieee.float_negate machine_ieee.fp32_to_float)

machine_ieee.fp32_negate1985 =
  machine_ieee.float_to_fp32
  (binary_ieee.float_negate1985 machine_ieee.fp32_to_float)

machine_ieee.fp32_to_fp64 =
  machine_ieee.convert machine_ieee.fp32_to_float
    machine_ieee.float_to_fp64 machine_ieee.real_to_fp64
    binary_ieee.roundTiesToEven

machine_ieee.fp64_abs =
  machine_ieee.float_to_fp64
  (binary_ieee.float_abs machine_ieee.fp64_to_float)

machine_ieee.fp64_abs1985 =
  machine_ieee.float_to_fp64
  (binary_ieee.float_abs1985 machine_ieee.fp64_to_float)

machine_ieee.fp64_negate =
  machine_ieee.float_to_fp64
  (binary_ieee.float_negate machine_ieee.fp64_to_float)

machine_ieee.fp64_negate1985 =
  machine_ieee.float_to_fp64
  (binary_ieee.float_negate1985 machine_ieee.fp64_to_float)

a.
    machine_ieee.fp16_isFinite (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_finite a

a.
    machine_ieee.fp16_isInfinite (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_infinite a

a.
    machine_ieee.fp16_isIntegral (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_integral a

a.
    machine_ieee.fp16_isNan (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_nan a

a.
    machine_ieee.fp16_isNormal (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_normal a

a.
    machine_ieee.fp16_isSubnormal (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_subnormal a

a.
    machine_ieee.fp16_isZero (machine_ieee.float_to_fp16 a)
    binary_ieee.float_is_zero a

a.
    machine_ieee.fp16_to_real (machine_ieee.float_to_fp16 a) =
    binary_ieee.float_value a

a.
    machine_ieee.fp32_isFinite (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_finite a

a.
    machine_ieee.fp32_isInfinite (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_infinite a

a.
    machine_ieee.fp32_isIntegral (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_integral a

a.
    machine_ieee.fp32_isNan (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_nan a

a.
    machine_ieee.fp32_isNormal (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_normal a

a.
    machine_ieee.fp32_isSubnormal (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_subnormal a

a.
    machine_ieee.fp32_isZero (machine_ieee.float_to_fp32 a)
    binary_ieee.float_is_zero a

a.
    machine_ieee.fp32_to_real (machine_ieee.float_to_fp32 a) =
    binary_ieee.float_value a

a.
    machine_ieee.fp64_isFinite (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_finite a

a.
    machine_ieee.fp64_isInfinite (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_infinite a

a.
    machine_ieee.fp64_isIntegral (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_integral a

a.
    machine_ieee.fp64_isNan (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_nan a

a.
    machine_ieee.fp64_isNormal (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_normal a

a.
    machine_ieee.fp64_isSubnormal (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_subnormal a

a.
    machine_ieee.fp64_isZero (machine_ieee.float_to_fp64 a)
    binary_ieee.float_is_zero a

a.
    machine_ieee.fp64_to_real (machine_ieee.float_to_fp64 a) =
    binary_ieee.float_value a

binary_ieee.ulp bool.the_value =
  binary_ieee.ULP (words.n2w 0, bool.the_value)

Number.Real.~ (binary_ieee.ulp bool.the_value) =
  binary_ieee.float_to_real
    (binary_ieee.float_negate (binary_ieee.float_plus_min bool.the_value))

mode.
    machine_ieee.real_to_fp16 mode =
    machine_ieee.float_to_fp16 binary_ieee.real_to_float mode

mode.
    machine_ieee.real_to_fp32 mode =
    machine_ieee.float_to_fp32 binary_ieee.real_to_float mode

mode.
    machine_ieee.fp16_to_int mode =
    binary_ieee.float_to_int mode machine_ieee.fp16_to_float

mode.
    machine_ieee.real_to_fp64 mode =
    machine_ieee.float_to_fp64 binary_ieee.real_to_float mode

mode.
    machine_ieee.fp32_to_int mode =
    binary_ieee.float_to_int mode machine_ieee.fp32_to_float

mode.
    machine_ieee.fp64_to_int mode =
    binary_ieee.float_to_int mode machine_ieee.fp64_to_float

x.
    binary_ieee.float_to_real (binary_ieee.float_negate x) =
    Number.Real.~ (binary_ieee.float_to_real x)

e.
    Number.Real.≤ (binary_ieee.ulp bool.the_value)
      (binary_ieee.ULP (e, bool.the_value))

a.
    machine_ieee.fp16_abs (machine_ieee.float_to_fp16 a) =
    machine_ieee.float_to_fp16 (binary_ieee.float_abs a)

a.
    machine_ieee.fp16_abs1985 (machine_ieee.float_to_fp16 a) =
    machine_ieee.float_to_fp16 (binary_ieee.float_abs1985 a)

a.
    machine_ieee.fp16_negate (machine_ieee.float_to_fp16 a) =
    machine_ieee.float_to_fp16 (binary_ieee.float_negate a)

a.
    machine_ieee.fp16_negate1985 (machine_ieee.float_to_fp16 a) =
    machine_ieee.float_to_fp16 (binary_ieee.float_negate1985 a)

a.
    machine_ieee.fp32_abs (machine_ieee.float_to_fp32 a) =
    machine_ieee.float_to_fp32 (binary_ieee.float_abs a)

a.
    machine_ieee.fp32_abs1985 (machine_ieee.float_to_fp32 a) =
    machine_ieee.float_to_fp32 (binary_ieee.float_abs1985 a)

a.
    machine_ieee.fp32_negate (machine_ieee.float_to_fp32 a) =
    machine_ieee.float_to_fp32 (binary_ieee.float_negate a)

a.
    machine_ieee.fp32_negate1985 (machine_ieee.float_to_fp32 a) =
    machine_ieee.float_to_fp32 (binary_ieee.float_negate1985 a)

a.
    machine_ieee.fp64_abs (machine_ieee.float_to_fp64 a) =
    machine_ieee.float_to_fp64 (binary_ieee.float_abs a)

a.
    machine_ieee.fp64_abs1985 (machine_ieee.float_to_fp64 a) =
    machine_ieee.float_to_fp64 (binary_ieee.float_abs1985 a)

a.
    machine_ieee.fp64_negate (machine_ieee.float_to_fp64 a) =
    machine_ieee.float_to_fp64 (binary_ieee.float_negate a)

a.
    machine_ieee.fp64_negate1985 (machine_ieee.float_to_fp64 a) =
    machine_ieee.float_to_fp64 (binary_ieee.float_negate1985 a)

rep. bool.TYPE_DEFINITION (λn. n < arithmetic.BIT2 1) rep

rep. bool.TYPE_DEFINITION (λn. n < arithmetic.BIT2 1) rep

m.
    binary_ieee.real_to_float m =
    binary_ieee.float_round m (m = binary_ieee.roundTowardNegative)

n.
    Number.Real.< 0
      (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0)) n)

n.
    Number.Real.≤ 0
      (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0)) n)

a.
    machine_ieee.fp16_isFinite (words.n2w a)
    binary_ieee.float_is_finite (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp16_isInfinite (words.n2w a)
    binary_ieee.float_is_infinite
      (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp16_isIntegral (words.n2w a)
    binary_ieee.float_is_integral
      (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp16_isNan (words.n2w a)
    binary_ieee.float_is_nan (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp16_isNormal (words.n2w a)
    binary_ieee.float_is_normal (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp16_isSubnormal (words.n2w a)
    binary_ieee.float_is_subnormal
      (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp16_isZero (words.n2w a)
    binary_ieee.float_is_zero (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp32_isFinite (words.n2w a)
    binary_ieee.float_is_finite (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp32_isInfinite (words.n2w a)
    binary_ieee.float_is_infinite
      (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp32_isIntegral (words.n2w a)
    binary_ieee.float_is_integral
      (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp32_isNan (words.n2w a)
    binary_ieee.float_is_nan (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp32_isNormal (words.n2w a)
    binary_ieee.float_is_normal (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp32_isSubnormal (words.n2w a)
    binary_ieee.float_is_subnormal
      (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp32_isZero (words.n2w a)
    binary_ieee.float_is_zero (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp64_isFinite (words.n2w a)
    binary_ieee.float_is_finite (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp64_isInfinite (words.n2w a)
    binary_ieee.float_is_infinite
      (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp64_isIntegral (words.n2w a)
    binary_ieee.float_is_integral
      (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp64_isNan (words.n2w a)
    binary_ieee.float_is_nan (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp64_isNormal (words.n2w a)
    binary_ieee.float_is_normal (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp64_isSubnormal (words.n2w a)
    binary_ieee.float_is_subnormal
      (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp64_isZero (words.n2w a)
    binary_ieee.float_is_zero (machine_ieee.fp64_to_float (words.n2w a))

a.
    machine_ieee.fp16_to_real (words.n2w a) =
    binary_ieee.float_value (machine_ieee.fp16_to_float (words.n2w a))

a.
    machine_ieee.fp32_to_real (words.n2w a) =
    binary_ieee.float_value (machine_ieee.fp32_to_float (words.n2w a))

a.
    machine_ieee.fp64_to_real (words.n2w a) =
    binary_ieee.float_value (machine_ieee.fp64_to_float (words.n2w a))

x. binary_ieee.float_is_zero x binary_ieee.float_to_real x = 0

x.
    binary_ieee.float_abs x =
    binary_ieee.float_Sign_fupd (const (words.n2w 0)) x

mode.
    machine_ieee.fp16_roundToIntegral mode =
    machine_ieee.float_to_fp16
    (binary_ieee.float_round_to_integral mode machine_ieee.fp16_to_float)

mode.
    machine_ieee.fp16_sqrt mode =
    machine_ieee.float_to_fp16
    (binary_ieee.float_sqrt mode machine_ieee.fp16_to_float)

mode.
    machine_ieee.fp32_roundToIntegral mode =
    machine_ieee.float_to_fp32
    (binary_ieee.float_round_to_integral mode machine_ieee.fp32_to_float)

mode.
    machine_ieee.fp32_sqrt mode =
    machine_ieee.float_to_fp32
    (binary_ieee.float_sqrt mode machine_ieee.fp32_to_float)

mode.
    machine_ieee.fp64_roundToIntegral mode =
    machine_ieee.float_to_fp64
    (binary_ieee.float_round_to_integral mode machine_ieee.fp64_to_float)

mode.
    machine_ieee.fp64_sqrt mode =
    machine_ieee.float_to_fp64
    (binary_ieee.float_sqrt mode machine_ieee.fp64_to_float)

n. ¬(Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0)) n = 0)

a.
    machine_ieee.fp16_abs (words.n2w a) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_abs (machine_ieee.fp16_to_float (words.n2w a)))

a.
    machine_ieee.fp16_abs1985 (words.n2w a) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_abs1985
         (machine_ieee.fp16_to_float (words.n2w a)))

a.
    machine_ieee.fp16_negate (words.n2w a) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_negate (machine_ieee.fp16_to_float (words.n2w a)))

a.
    machine_ieee.fp16_negate1985 (words.n2w a) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_negate1985
         (machine_ieee.fp16_to_float (words.n2w a)))

a.
    machine_ieee.fp32_abs (words.n2w a) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_abs (machine_ieee.fp32_to_float (words.n2w a)))

a.
    machine_ieee.fp32_abs1985 (words.n2w a) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_abs1985
         (machine_ieee.fp32_to_float (words.n2w a)))

a.
    machine_ieee.fp32_negate (words.n2w a) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_negate (machine_ieee.fp32_to_float (words.n2w a)))

a.
    machine_ieee.fp32_negate1985 (words.n2w a) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_negate1985
         (machine_ieee.fp32_to_float (words.n2w a)))

a.
    machine_ieee.fp64_abs (words.n2w a) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_abs (machine_ieee.fp64_to_float (words.n2w a)))

a.
    machine_ieee.fp64_abs1985 (words.n2w a) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_abs1985
         (machine_ieee.fp64_to_float (words.n2w a)))

a.
    machine_ieee.fp64_negate (words.n2w a) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_negate (machine_ieee.fp64_to_float (words.n2w a)))

a.
    machine_ieee.fp64_negate1985 (words.n2w a) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_negate1985
         (machine_ieee.fp64_to_float (words.n2w a)))

x.
    binary_ieee.float_abs1985 x =
    if binary_ieee.float_is_finite x then binary_ieee.float_abs x else x

x.
    binary_ieee.float_negate x =
    binary_ieee.float_Sign_fupd
      (const (words.word_1comp (binary_ieee.float_Sign x))) x

x.
    binary_ieee.float_negate1985 x =
    if binary_ieee.float_is_finite x then binary_ieee.float_negate x else x

mode a.
    machine_ieee.int_to_fp16 mode a =
    machine_ieee.real_to_fp16 mode (intreal.real_of_int a)

mode a.
    machine_ieee.int_to_fp32 mode a =
    machine_ieee.real_to_fp32 mode (intreal.real_of_int a)

mode a.
    machine_ieee.int_to_fp64 mode a =
    machine_ieee.real_to_fp64 mode (intreal.real_of_int a)

mode a.
    machine_ieee.fp16_to_int mode (machine_ieee.float_to_fp16 a) =
    binary_ieee.float_to_int mode a

mode a.
    machine_ieee.fp32_to_int mode (machine_ieee.float_to_fp32 a) =
    binary_ieee.float_to_int mode a

mode a.
    machine_ieee.fp64_to_int mode (machine_ieee.float_to_fp64 a) =
    binary_ieee.float_to_int mode a

x.
    binary_ieee.float_is_finite x
    binary_ieee.float_value_CASE (binary_ieee.float_value x) (λv1. )

x.
    binary_ieee.float_is_infinite x
    binary_ieee.float_value_CASE (binary_ieee.float_value x) (λv1. )

x.
    binary_ieee.float_is_nan x
    binary_ieee.float_value_CASE (binary_ieee.float_value x) (λv1. )

c c0 c1.
    binary_ieee.float_Significand (binary_ieee.recordtype.float c c0 c1) =
    c1

c c0 c1.
    binary_ieee.float_Exponent (binary_ieee.recordtype.float c c0 c1) = c0

c c0 c1.
    binary_ieee.float_Sign (binary_ieee.recordtype.float c c0 c1) = c

a a'.
    a = a'
    binary_ieee.float_compare2num a = binary_ieee.float_compare2num a'

a a'.
    binary_ieee.float_compare2num a = binary_ieee.float_compare2num a'
    a = a'

a a'. a = a' binary_ieee.rounding2num a = binary_ieee.rounding2num a'

a a'. binary_ieee.rounding2num a = binary_ieee.rounding2num a' a = a'

mode a.
    machine_ieee.fp16_roundToIntegral mode (machine_ieee.float_to_fp16 a) =
    machine_ieee.float_to_fp16 (binary_ieee.float_round_to_integral mode a)

mode a.
    machine_ieee.fp16_sqrt mode (machine_ieee.float_to_fp16 a) =
    machine_ieee.float_to_fp16 (binary_ieee.float_sqrt mode a)

mode a.
    machine_ieee.fp32_roundToIntegral mode (machine_ieee.float_to_fp32 a) =
    machine_ieee.float_to_fp32 (binary_ieee.float_round_to_integral mode a)

mode a.
    machine_ieee.fp32_sqrt mode (machine_ieee.float_to_fp32 a) =
    machine_ieee.float_to_fp32 (binary_ieee.float_sqrt mode a)

mode a.
    machine_ieee.fp64_roundToIntegral mode (machine_ieee.float_to_fp64 a) =
    machine_ieee.float_to_fp64 (binary_ieee.float_round_to_integral mode a)

mode a.
    machine_ieee.fp64_sqrt mode (machine_ieee.float_to_fp64 a) =
    machine_ieee.float_to_fp64 (binary_ieee.float_sqrt mode a)

a a'. binary_ieee.Float a = binary_ieee.Float a' a = a'

x y.
    binary_ieee.float_equal x y
    binary_ieee.float_compare x y = binary_ieee.EQ

x y.
    binary_ieee.float_greater_than x y
    binary_ieee.float_compare x y = binary_ieee.GT

x y.
    binary_ieee.float_less_than x y
    binary_ieee.float_compare x y = binary_ieee.LT

ff. c c0 c1. ff = binary_ieee.recordtype.float c c0 c1

a b.
    machine_ieee.fp16_equal a b
    binary_ieee.float_equal (machine_ieee.fp16_to_float a)
      (machine_ieee.fp16_to_float b)

a b.
    machine_ieee.fp16_greaterEqual a b
    binary_ieee.float_greater_equal (machine_ieee.fp16_to_float a)
      (machine_ieee.fp16_to_float b)

a b.
    machine_ieee.fp16_greaterThan a b
    binary_ieee.float_greater_than (machine_ieee.fp16_to_float a)
      (machine_ieee.fp16_to_float b)

a b.
    machine_ieee.fp16_lessEqual a b
    binary_ieee.float_less_equal (machine_ieee.fp16_to_float a)
      (machine_ieee.fp16_to_float b)

a b.
    machine_ieee.fp16_lessThan a b
    binary_ieee.float_less_than (machine_ieee.fp16_to_float a)
      (machine_ieee.fp16_to_float b)

a b.
    machine_ieee.fp16_compare a b =
    binary_ieee.float_compare (machine_ieee.fp16_to_float a)
      (machine_ieee.fp16_to_float b)

x y. machine_ieee.fp16_to_float x = machine_ieee.fp16_to_float y x = y

x y. machine_ieee.float_to_fp16 x = machine_ieee.float_to_fp16 y x = y

b a.
    machine_ieee.fp16_equal (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) binary_ieee.float_equal a b

b a.
    machine_ieee.fp16_greaterEqual (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) binary_ieee.float_greater_equal a b

b a.
    machine_ieee.fp16_greaterThan (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) binary_ieee.float_greater_than a b

b a.
    machine_ieee.fp16_lessEqual (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) binary_ieee.float_less_equal a b

b a.
    machine_ieee.fp16_lessThan (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) binary_ieee.float_less_than a b

b a.
    machine_ieee.fp16_compare (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) = binary_ieee.float_compare a b

a b.
    machine_ieee.fp32_equal a b
    binary_ieee.float_equal (machine_ieee.fp32_to_float a)
      (machine_ieee.fp32_to_float b)

a b.
    machine_ieee.fp32_greaterEqual a b
    binary_ieee.float_greater_equal (machine_ieee.fp32_to_float a)
      (machine_ieee.fp32_to_float b)

a b.
    machine_ieee.fp32_greaterThan a b
    binary_ieee.float_greater_than (machine_ieee.fp32_to_float a)
      (machine_ieee.fp32_to_float b)

a b.
    machine_ieee.fp32_lessEqual a b
    binary_ieee.float_less_equal (machine_ieee.fp32_to_float a)
      (machine_ieee.fp32_to_float b)

a b.
    machine_ieee.fp32_lessThan a b
    binary_ieee.float_less_than (machine_ieee.fp32_to_float a)
      (machine_ieee.fp32_to_float b)

a b.
    machine_ieee.fp32_compare a b =
    binary_ieee.float_compare (machine_ieee.fp32_to_float a)
      (machine_ieee.fp32_to_float b)

x y. machine_ieee.fp32_to_float x = machine_ieee.fp32_to_float y x = y

a b.
    machine_ieee.fp64_equal a b
    binary_ieee.float_equal (machine_ieee.fp64_to_float a)
      (machine_ieee.fp64_to_float b)

a b.
    machine_ieee.fp64_greaterEqual a b
    binary_ieee.float_greater_equal (machine_ieee.fp64_to_float a)
      (machine_ieee.fp64_to_float b)

a b.
    machine_ieee.fp64_greaterThan a b
    binary_ieee.float_greater_than (machine_ieee.fp64_to_float a)
      (machine_ieee.fp64_to_float b)

a b.
    machine_ieee.fp64_lessEqual a b
    binary_ieee.float_less_equal (machine_ieee.fp64_to_float a)
      (machine_ieee.fp64_to_float b)

a b.
    machine_ieee.fp64_lessThan a b
    binary_ieee.float_less_than (machine_ieee.fp64_to_float a)
      (machine_ieee.fp64_to_float b)

a b.
    machine_ieee.fp64_compare a b =
    binary_ieee.float_compare (machine_ieee.fp64_to_float a)
      (machine_ieee.fp64_to_float b)

x y. machine_ieee.fp64_to_float x = machine_ieee.fp64_to_float y x = y

x y. machine_ieee.float_to_fp32 x = machine_ieee.float_to_fp32 y x = y

b a.
    machine_ieee.fp32_equal (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) binary_ieee.float_equal a b

b a.
    machine_ieee.fp32_greaterEqual (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) binary_ieee.float_greater_equal a b

b a.
    machine_ieee.fp32_greaterThan (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) binary_ieee.float_greater_than a b

b a.
    machine_ieee.fp32_lessEqual (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) binary_ieee.float_less_equal a b

b a.
    machine_ieee.fp32_lessThan (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) binary_ieee.float_less_than a b

b a.
    machine_ieee.fp32_compare (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) = binary_ieee.float_compare a b

x y. machine_ieee.float_to_fp64 x = machine_ieee.float_to_fp64 y x = y

b a.
    machine_ieee.fp64_equal (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) binary_ieee.float_equal a b

b a.
    machine_ieee.fp64_greaterEqual (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) binary_ieee.float_greater_equal a b

b a.
    machine_ieee.fp64_greaterThan (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) binary_ieee.float_greater_than a b

b a.
    machine_ieee.fp64_lessEqual (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) binary_ieee.float_less_equal a b

b a.
    machine_ieee.fp64_lessThan (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) binary_ieee.float_less_than a b

b a.
    machine_ieee.fp64_compare (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) = binary_ieee.float_compare a b

r.
    r < arithmetic.BIT2 1
    binary_ieee.float_compare2num (binary_ieee.num2float_compare r) = r

r.
    r < arithmetic.BIT2 1
    binary_ieee.rounding2num (binary_ieee.num2rounding r) = r

s. ¬(Number.Real.↑ (Number.Real.~ 1) (words.w2n s) = 0)

x.
    machine_ieee.float_to_fp16 x =
    words.word_concat (binary_ieee.float_Sign x)
      (words.word_concat (binary_ieee.float_Exponent x)
         (binary_ieee.float_Significand x))

x.
    machine_ieee.float_to_fp32 x =
    words.word_concat (binary_ieee.float_Sign x)
      (words.word_concat (binary_ieee.float_Exponent x)
         (binary_ieee.float_Significand x))

x.
    machine_ieee.float_to_fp64 x =
    words.word_concat (binary_ieee.float_Sign x)
      (words.word_concat (binary_ieee.float_Exponent x)
         (binary_ieee.float_Significand x))

a. r. a = binary_ieee.num2float_compare r r < arithmetic.BIT2 1

mode a.
    machine_ieee.fp16_to_int mode (words.n2w a) =
    binary_ieee.float_to_int mode
      (machine_ieee.fp16_to_float (words.n2w a))

mode a.
    machine_ieee.fp32_to_int mode (words.n2w a) =
    binary_ieee.float_to_int mode
      (machine_ieee.fp32_to_float (words.n2w a))

mode a.
    machine_ieee.fp64_to_int mode (words.n2w a) =
    binary_ieee.float_to_int mode
      (machine_ieee.fp64_to_float (words.n2w a))

a. r. a = binary_ieee.num2rounding r r < arithmetic.BIT2 1

r. r < arithmetic.BIT2 1 a. r = binary_ieee.float_compare2num a

r. r < arithmetic.BIT2 1 a. r = binary_ieee.rounding2num a

binary_ieee.float_to_real (binary_ieee.float_plus_zero bool.the_value) =
  0
  binary_ieee.float_to_real (binary_ieee.float_minus_zero bool.the_value) =
  0

b. arithmetic.BIT2 0 < arithmetic.BIT2 0 b 1 < b

b. arithmetic.BIT2 0 arithmetic.BIT2 0 b 1 b

mode a.
    machine_ieee.fp16_roundToIntegral mode (words.n2w a) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_round_to_integral mode
         (machine_ieee.fp16_to_float (words.n2w a)))

mode a.
    machine_ieee.fp16_sqrt mode (words.n2w a) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_sqrt mode
         (machine_ieee.fp16_to_float (words.n2w a)))

mode a.
    machine_ieee.fp32_roundToIntegral mode (words.n2w a) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_round_to_integral mode
         (machine_ieee.fp32_to_float (words.n2w a)))

mode a.
    machine_ieee.fp32_sqrt mode (words.n2w a) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_sqrt mode
         (machine_ieee.fp32_to_float (words.n2w a)))

mode a.
    machine_ieee.fp64_roundToIntegral mode (words.n2w a) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_round_to_integral mode
         (machine_ieee.fp64_to_float (words.n2w a)))

mode a.
    machine_ieee.fp64_sqrt mode (words.n2w a) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_sqrt mode
         (machine_ieee.fp64_to_float (words.n2w a)))

m n.
    Number.Real.≤ 0
      (real./ (Number.Real.fromNatural m)
         (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0)) n))

y x.
    Number.Real.< (binary_ieee.largest bool.the_value) x
    binary_ieee.round binary_ieee.roundTowardNegative x =
    binary_ieee.float_top bool.the_value

y x.
    Number.Real.< (binary_ieee.largest bool.the_value) x
    binary_ieee.round binary_ieee.roundTowardPositive x =
    binary_ieee.float_plus_infinity bool.the_value

y x.
    Number.Real.< (binary_ieee.largest bool.the_value) x
    binary_ieee.round binary_ieee.roundTowardZero x =
    binary_ieee.float_top bool.the_value

y x.
    Number.Real.≤ (binary_ieee.threshold bool.the_value) x
    binary_ieee.round binary_ieee.roundTiesToEven x =
    binary_ieee.float_plus_infinity bool.the_value

x.
    binary_ieee.float_is_zero x
    binary_ieee.float_value_CASE (binary_ieee.float_value x) (λr. r = 0)
      

x.
    Number.Real.< (Number.Real.abs x) (binary_ieee.ulp bool.the_value)
    binary_ieee.float_round binary_ieee.roundTowardZero x =
    binary_ieee.float_plus_zero bool.the_value

x.
    Number.Real.< (Number.Real.abs x) (binary_ieee.ulp bool.the_value)
    binary_ieee.float_round binary_ieee.roundTowardZero x =
    binary_ieee.float_minus_zero bool.the_value

ff.
    (r. ff = binary_ieee.Float r) ff = binary_ieee.Infinity
    ff = binary_ieee.NaN

y x.
    Number.Real.< x (Number.Real.~ (binary_ieee.largest bool.the_value))
    binary_ieee.round binary_ieee.roundTowardNegative x =
    binary_ieee.float_minus_infinity bool.the_value

y x.
    Number.Real.< x (Number.Real.~ (binary_ieee.largest bool.the_value))
    binary_ieee.round binary_ieee.roundTowardPositive x =
    binary_ieee.float_bottom bool.the_value

y x.
    Number.Real.< x (Number.Real.~ (binary_ieee.largest bool.the_value))
    binary_ieee.round binary_ieee.roundTowardZero x =
    binary_ieee.float_bottom bool.the_value

y x.
    Number.Real.≤ x
      (Number.Real.~ (binary_ieee.threshold bool.the_value))
    binary_ieee.round binary_ieee.roundTiesToEven x =
    binary_ieee.float_minus_infinity bool.the_value

x y.
    binary_ieee.float_greater_equal x y
    binary_ieee.float_compare_CASE (binary_ieee.float_compare x y)

x y.
    binary_ieee.float_less_equal x y
    binary_ieee.float_compare_CASE (binary_ieee.float_compare x y)

P. (e. P (e, bool.the_value)) v v1. P (v, v1)

binary_ieee.float_plus_infinity bool.the_value =
  binary_ieee.float_Sign_fupd (const (words.n2w 0))
    (binary_ieee.float_Exponent_fupd (const words.word_T)
       (binary_ieee.float_Significand_fupd (const (words.n2w 0)) bool.ARB))

mode x.
    binary_ieee.float_round_to_integral mode x =
    binary_ieee.float_value_CASE (binary_ieee.float_value x)
      (λr. binary_ieee.integral_round mode r) x x

x.
    binary_ieee.float_is_zero x
    binary_ieee.float_Exponent x = words.n2w 0
    binary_ieee.float_Significand x = words.n2w 0

P. (c c0 c1. P (binary_ieee.recordtype.float c c0 c1)) ff. P ff

b a.
    machine_ieee.fp16_equal (words.n2w a) (words.n2w b)
    binary_ieee.float_equal (machine_ieee.fp16_to_float (words.n2w a))
      (machine_ieee.fp16_to_float (words.n2w b))

b a.
    machine_ieee.fp16_greaterEqual (words.n2w a) (words.n2w b)
    binary_ieee.float_greater_equal
      (machine_ieee.fp16_to_float (words.n2w a))
      (machine_ieee.fp16_to_float (words.n2w b))

b a.
    machine_ieee.fp16_greaterThan (words.n2w a) (words.n2w b)
    binary_ieee.float_greater_than
      (machine_ieee.fp16_to_float (words.n2w a))
      (machine_ieee.fp16_to_float (words.n2w b))

b a.
    machine_ieee.fp16_lessEqual (words.n2w a) (words.n2w b)
    binary_ieee.float_less_equal (machine_ieee.fp16_to_float (words.n2w a))
      (machine_ieee.fp16_to_float (words.n2w b))

b a.
    machine_ieee.fp16_lessThan (words.n2w a) (words.n2w b)
    binary_ieee.float_less_than (machine_ieee.fp16_to_float (words.n2w a))
      (machine_ieee.fp16_to_float (words.n2w b))

b a.
    machine_ieee.fp32_equal (words.n2w a) (words.n2w b)
    binary_ieee.float_equal (machine_ieee.fp32_to_float (words.n2w a))
      (machine_ieee.fp32_to_float (words.n2w b))

b a.
    machine_ieee.fp32_greaterEqual (words.n2w a) (words.n2w b)
    binary_ieee.float_greater_equal
      (machine_ieee.fp32_to_float (words.n2w a))
      (machine_ieee.fp32_to_float (words.n2w b))

b a.
    machine_ieee.fp32_greaterThan (words.n2w a) (words.n2w b)
    binary_ieee.float_greater_than
      (machine_ieee.fp32_to_float (words.n2w a))
      (machine_ieee.fp32_to_float (words.n2w b))

b a.
    machine_ieee.fp32_lessEqual (words.n2w a) (words.n2w b)
    binary_ieee.float_less_equal (machine_ieee.fp32_to_float (words.n2w a))
      (machine_ieee.fp32_to_float (words.n2w b))

b a.
    machine_ieee.fp32_lessThan (words.n2w a) (words.n2w b)
    binary_ieee.float_less_than (machine_ieee.fp32_to_float (words.n2w a))
      (machine_ieee.fp32_to_float (words.n2w b))

b a.
    machine_ieee.fp64_equal (words.n2w a) (words.n2w b)
    binary_ieee.float_equal (machine_ieee.fp64_to_float (words.n2w a))
      (machine_ieee.fp64_to_float (words.n2w b))

b a.
    machine_ieee.fp64_greaterEqual (words.n2w a) (words.n2w b)
    binary_ieee.float_greater_equal
      (machine_ieee.fp64_to_float (words.n2w a))
      (machine_ieee.fp64_to_float (words.n2w b))

b a.
    machine_ieee.fp64_greaterThan (words.n2w a) (words.n2w b)
    binary_ieee.float_greater_than
      (machine_ieee.fp64_to_float (words.n2w a))
      (machine_ieee.fp64_to_float (words.n2w b))

b a.
    machine_ieee.fp64_lessEqual (words.n2w a) (words.n2w b)
    binary_ieee.float_less_equal (machine_ieee.fp64_to_float (words.n2w a))
      (machine_ieee.fp64_to_float (words.n2w b))

b a.
    machine_ieee.fp64_lessThan (words.n2w a) (words.n2w b)
    binary_ieee.float_less_than (machine_ieee.fp64_to_float (words.n2w a))
      (machine_ieee.fp64_to_float (words.n2w b))

b a.
    machine_ieee.fp16_compare (words.n2w a) (words.n2w b) =
    binary_ieee.float_compare (machine_ieee.fp16_to_float (words.n2w a))
      (machine_ieee.fp16_to_float (words.n2w b))

b a.
    machine_ieee.fp32_compare (words.n2w a) (words.n2w b) =
    binary_ieee.float_compare (machine_ieee.fp32_to_float (words.n2w a))
      (machine_ieee.fp32_to_float (words.n2w b))

b a.
    machine_ieee.fp64_compare (words.n2w a) (words.n2w b) =
    binary_ieee.float_compare (machine_ieee.fp64_to_float (words.n2w a))
      (machine_ieee.fp64_to_float (words.n2w b))

binary_ieee.float_minus_infinity bool.the_value =
  binary_ieee.float_Sign_fupd (const (words.n2w 1))
    (binary_ieee.float_Exponent_fupd (const words.word_T)
       (binary_ieee.float_Significand_fupd (const (words.n2w 0)) bool.ARB))

binary_ieee.float_plus_zero bool.the_value =
  binary_ieee.float_Sign_fupd (const (words.n2w 0))
    (binary_ieee.float_Exponent_fupd (const (words.n2w 0))
       (binary_ieee.float_Significand_fupd (const (words.n2w 0)) bool.ARB))

b y x.
    Number.Real.< (binary_ieee.largest bool.the_value) x
    binary_ieee.float_round binary_ieee.roundTowardNegative b x =
    binary_ieee.float_top bool.the_value

b y x.
    Number.Real.< (binary_ieee.largest bool.the_value) x
    binary_ieee.float_round binary_ieee.roundTowardPositive b x =
    binary_ieee.float_plus_infinity bool.the_value

b y x.
    Number.Real.< (binary_ieee.largest bool.the_value) x
    binary_ieee.float_round binary_ieee.roundTowardZero b x =
    binary_ieee.float_top bool.the_value

a.
    a = binary_ieee.LT a = binary_ieee.EQ a = binary_ieee.GT
    a = binary_ieee.UN

mode a b.
    machine_ieee.fp16_add mode a b =
    machine_ieee.float_to_fp16
      (binary_ieee.float_add mode (machine_ieee.fp16_to_float a)
         (machine_ieee.fp16_to_float b))

mode a b.
    machine_ieee.fp16_div mode a b =
    machine_ieee.float_to_fp16
      (binary_ieee.float_div mode (machine_ieee.fp16_to_float a)
         (machine_ieee.fp16_to_float b))

mode a b.
    machine_ieee.fp16_mul mode a b =
    machine_ieee.float_to_fp16
      (binary_ieee.float_mul mode (machine_ieee.fp16_to_float a)
         (machine_ieee.fp16_to_float b))

mode a b.
    machine_ieee.fp16_sub mode a b =
    machine_ieee.float_to_fp16
      (binary_ieee.float_sub mode (machine_ieee.fp16_to_float a)
         (machine_ieee.fp16_to_float b))

mode b a.
    machine_ieee.fp16_add mode (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) =
    machine_ieee.float_to_fp16 (binary_ieee.float_add mode a b)

mode b a.
    machine_ieee.fp16_div mode (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) =
    machine_ieee.float_to_fp16 (binary_ieee.float_div mode a b)

mode b a.
    machine_ieee.fp16_mul mode (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) =
    machine_ieee.float_to_fp16 (binary_ieee.float_mul mode a b)

mode b a.
    machine_ieee.fp16_sub mode (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) =
    machine_ieee.float_to_fp16 (binary_ieee.float_sub mode a b)

mode a b.
    machine_ieee.fp32_add mode a b =
    machine_ieee.float_to_fp32
      (binary_ieee.float_add mode (machine_ieee.fp32_to_float a)
         (machine_ieee.fp32_to_float b))

mode a b.
    machine_ieee.fp32_div mode a b =
    machine_ieee.float_to_fp32
      (binary_ieee.float_div mode (machine_ieee.fp32_to_float a)
         (machine_ieee.fp32_to_float b))

mode a b.
    machine_ieee.fp32_mul mode a b =
    machine_ieee.float_to_fp32
      (binary_ieee.float_mul mode (machine_ieee.fp32_to_float a)
         (machine_ieee.fp32_to_float b))

mode a b.
    machine_ieee.fp32_sub mode a b =
    machine_ieee.float_to_fp32
      (binary_ieee.float_sub mode (machine_ieee.fp32_to_float a)
         (machine_ieee.fp32_to_float b))

mode a b.
    machine_ieee.fp64_add mode a b =
    machine_ieee.float_to_fp64
      (binary_ieee.float_add mode (machine_ieee.fp64_to_float a)
         (machine_ieee.fp64_to_float b))

mode a b.
    machine_ieee.fp64_div mode a b =
    machine_ieee.float_to_fp64
      (binary_ieee.float_div mode (machine_ieee.fp64_to_float a)
         (machine_ieee.fp64_to_float b))

mode a b.
    machine_ieee.fp64_mul mode a b =
    machine_ieee.float_to_fp64
      (binary_ieee.float_mul mode (machine_ieee.fp64_to_float a)
         (machine_ieee.fp64_to_float b))

mode a b.
    machine_ieee.fp64_sub mode a b =
    machine_ieee.float_to_fp64
      (binary_ieee.float_sub mode (machine_ieee.fp64_to_float a)
         (machine_ieee.fp64_to_float b))

mode b a.
    machine_ieee.fp32_add mode (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) =
    machine_ieee.float_to_fp32 (binary_ieee.float_add mode a b)

mode b a.
    machine_ieee.fp32_div mode (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) =
    machine_ieee.float_to_fp32 (binary_ieee.float_div mode a b)

mode b a.
    machine_ieee.fp32_mul mode (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) =
    machine_ieee.float_to_fp32 (binary_ieee.float_mul mode a b)

mode b a.
    machine_ieee.fp32_sub mode (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) =
    machine_ieee.float_to_fp32 (binary_ieee.float_sub mode a b)

mode b a.
    machine_ieee.fp64_add mode (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) =
    machine_ieee.float_to_fp64 (binary_ieee.float_add mode a b)

mode b a.
    machine_ieee.fp64_div mode (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) =
    machine_ieee.float_to_fp64 (binary_ieee.float_div mode a b)

mode b a.
    machine_ieee.fp64_mul mode (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) =
    machine_ieee.float_to_fp64 (binary_ieee.float_mul mode a b)

mode b a.
    machine_ieee.fp64_sub mode (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) =
    machine_ieee.float_to_fp64 (binary_ieee.float_sub mode a b)

a.
    a = binary_ieee.roundTiesToEven a = binary_ieee.roundTowardPositive
    a = binary_ieee.roundTowardNegative a = binary_ieee.roundTowardZero

P.
    (r. P (binary_ieee.Float r)) P binary_ieee.Infinity
    P binary_ieee.NaN ff. P ff

x.
    binary_ieee.float_is_integral x
    binary_ieee.float_value_CASE (binary_ieee.float_value x)
      (λr. n. Number.Real.abs r = Number.Real.fromNatural n)

x.
    binary_ieee.float_is_normal x
    ¬(binary_ieee.float_Exponent x = words.n2w 0)
    ¬(binary_ieee.float_Exponent x = words.word_T)

x.
    binary_ieee.float_is_subnormal x
    binary_ieee.float_Exponent x = words.n2w 0
    ¬(binary_ieee.float_Significand x = words.n2w 0)

P.
    P binary_ieee.EQ P binary_ieee.GT P binary_ieee.LT
    P binary_ieee.UN a. P a

P.
    P binary_ieee.roundTiesToEven P binary_ieee.roundTowardNegative
    P binary_ieee.roundTowardPositive P binary_ieee.roundTowardZero
    a. P a

a0 a1 a2 f.
    binary_ieee.float_CASE (binary_ieee.recordtype.float a0 a1 a2) f =
    f a0 a1 a2

binary_ieee.float_minus_zero bool.the_value =
  binary_ieee.float_Sign_fupd (const (words.n2w 1))
    (binary_ieee.float_Exponent_fupd (const (words.n2w 0))
       (binary_ieee.float_Significand_fupd (const (words.n2w 0)) bool.ARB))

binary_ieee.float_plus_min bool.the_value =
  binary_ieee.float_Sign_fupd (const (words.n2w 0))
    (binary_ieee.float_Exponent_fupd (const (words.n2w 0))
       (binary_ieee.float_Significand_fupd (const (words.n2w 1)) bool.ARB))

b y x.
    Number.Real.< x (Number.Real.~ (binary_ieee.largest bool.the_value))
    binary_ieee.float_round binary_ieee.roundTowardNegative b x =
    binary_ieee.float_minus_infinity bool.the_value

b y x.
    Number.Real.< x (Number.Real.~ (binary_ieee.largest bool.the_value))
    binary_ieee.float_round binary_ieee.roundTowardPositive b x =
    binary_ieee.float_bottom bool.the_value

b y x.
    Number.Real.< x (Number.Real.~ (binary_ieee.largest bool.the_value))
    binary_ieee.float_round binary_ieee.roundTowardZero b x =
    binary_ieee.float_bottom bool.the_value

f f1 a0 a1 a2.
    binary_ieee.float_size f f1 (binary_ieee.recordtype.float a0 a1 a2) = 1

f.
    fn. a0 a1 a2. fn (binary_ieee.recordtype.float a0 a1 a2) = f a0 a1 a2

(a. binary_ieee.float_value_size (binary_ieee.Float a) = 1)
  binary_ieee.float_value_size binary_ieee.Infinity = 0
  binary_ieee.float_value_size binary_ieee.NaN = 0

x y.
    binary_ieee.float_to_real x = binary_ieee.float_to_real y
    x = y binary_ieee.float_is_zero x binary_ieee.float_is_zero y

f.
    c1 c0 c.
      f =
      binary_ieee.float_Sign_fupd (const c1)
        (binary_ieee.float_Exponent_fupd (const c0)
           (binary_ieee.float_Significand_fupd (const c) bool.ARB))

f c c0 c1.
    binary_ieee.float_Significand_fupd f
      (binary_ieee.recordtype.float c c0 c1) =
    binary_ieee.recordtype.float c c0 (f c1)

f c c0 c1.
    binary_ieee.float_Exponent_fupd f
      (binary_ieee.recordtype.float c c0 c1) =
    binary_ieee.recordtype.float c (f c0) c1

f c c0 c1.
    binary_ieee.float_Sign_fupd f (binary_ieee.recordtype.float c c0 c1) =
    binary_ieee.recordtype.float (f c) c0 c1

binary_ieee.float_top bool.the_value =
  binary_ieee.float_Sign_fupd (const (words.n2w 0))
    (binary_ieee.float_Exponent_fupd
       (const (words.word_sub words.word_T (words.n2w 1)))
       (binary_ieee.float_Significand_fupd (const words.word_T) bool.ARB))

mode toneg r.
    binary_ieee.round mode r = binary_ieee.float_bottom bool.the_value
    binary_ieee.float_round mode toneg r =
    binary_ieee.float_bottom bool.the_value

mode toneg r.
    binary_ieee.round mode r =
    binary_ieee.float_minus_infinity bool.the_value
    binary_ieee.float_round mode toneg r =
    binary_ieee.float_minus_infinity bool.the_value

mode toneg r.
    binary_ieee.round mode r =
    binary_ieee.float_plus_infinity bool.the_value
    binary_ieee.float_round mode toneg r =
    binary_ieee.float_plus_infinity bool.the_value

mode toneg r.
    binary_ieee.round mode r = binary_ieee.float_top bool.the_value
    binary_ieee.float_round mode toneg r =
    binary_ieee.float_top bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_add mode x
      (binary_ieee.float_minus_infinity bool.the_value) =
    binary_ieee.float_minus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_add mode x
      (binary_ieee.float_plus_infinity bool.the_value) =
    binary_ieee.float_plus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_sub mode x
      (binary_ieee.float_minus_infinity bool.the_value) =
    binary_ieee.float_plus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_sub mode x
      (binary_ieee.float_plus_infinity bool.the_value) =
    binary_ieee.float_minus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_add mode
      (binary_ieee.float_minus_infinity bool.the_value) x =
    binary_ieee.float_minus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_add mode
      (binary_ieee.float_plus_infinity bool.the_value) x =
    binary_ieee.float_plus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_sub mode
      (binary_ieee.float_minus_infinity bool.the_value) x =
    binary_ieee.float_minus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_sub mode
      (binary_ieee.float_plus_infinity bool.the_value) x =
    binary_ieee.float_plus_infinity bool.the_value

x.
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs x)) (binary_ieee.ulp bool.the_value)
    binary_ieee.float_round binary_ieee.roundTiesToEven x =
    binary_ieee.float_plus_zero bool.the_value

x.
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs x)) (binary_ieee.ulp bool.the_value)
    binary_ieee.float_round binary_ieee.roundTiesToEven x =
    binary_ieee.float_minus_zero bool.the_value

a b. Number.Real.< 0 b (real./ a b = 0 a = 0)

(a. ¬(binary_ieee.Float a = binary_ieee.Infinity))
  (a. ¬(binary_ieee.Float a = binary_ieee.NaN))
  ¬(binary_ieee.Infinity = binary_ieee.NaN)

binary_ieee.float_is_zero =
  pred_set.INSERT (binary_ieee.float_minus_zero bool.the_value)
    (pred_set.INSERT (binary_ieee.float_plus_zero bool.the_value)
       pred_set.EMPTY)
  binary_ieee.float_is_infinite =
  pred_set.INSERT (binary_ieee.float_minus_infinity bool.the_value)
    (pred_set.INSERT (binary_ieee.float_plus_infinity bool.the_value)
       pred_set.EMPTY)

a.
    Number.Real.< (Number.Real.abs (binary_ieee.float_to_real a))
      (binary_ieee.ulp bool.the_value)
    binary_ieee.float_Exponent a = words.n2w 0
    binary_ieee.float_Significand a = words.n2w 0

mode b a.
    machine_ieee.fp16_add mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_add mode
         (machine_ieee.fp16_to_float (words.n2w a))
         (machine_ieee.fp16_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp16_div mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_div mode
         (machine_ieee.fp16_to_float (words.n2w a))
         (machine_ieee.fp16_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp16_mul mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_mul mode
         (machine_ieee.fp16_to_float (words.n2w a))
         (machine_ieee.fp16_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp16_sub mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_sub mode
         (machine_ieee.fp16_to_float (words.n2w a))
         (machine_ieee.fp16_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp32_add mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_add mode
         (machine_ieee.fp32_to_float (words.n2w a))
         (machine_ieee.fp32_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp32_div mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_div mode
         (machine_ieee.fp32_to_float (words.n2w a))
         (machine_ieee.fp32_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp32_mul mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_mul mode
         (machine_ieee.fp32_to_float (words.n2w a))
         (machine_ieee.fp32_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp32_sub mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_sub mode
         (machine_ieee.fp32_to_float (words.n2w a))
         (machine_ieee.fp32_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp64_add mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_add mode
         (machine_ieee.fp64_to_float (words.n2w a))
         (machine_ieee.fp64_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp64_div mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_div mode
         (machine_ieee.fp64_to_float (words.n2w a))
         (machine_ieee.fp64_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp64_mul mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_mul mode
         (machine_ieee.fp64_to_float (words.n2w a))
         (machine_ieee.fp64_to_float (words.n2w b)))

mode b a.
    machine_ieee.fp64_sub mode (words.n2w a) (words.n2w b) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_sub mode
         (machine_ieee.fp64_to_float (words.n2w a))
         (machine_ieee.fp64_to_float (words.n2w b)))

x.
    Number.Real.< (Number.Real.abs x) (binary_ieee.ulp bool.the_value)
    binary_ieee.round binary_ieee.roundTowardZero x =
    binary_ieee.float_plus_zero bool.the_value
    binary_ieee.round binary_ieee.roundTowardZero x =
    binary_ieee.float_minus_zero bool.the_value

x.
    binary_ieee.float_value x =
    if binary_ieee.float_Exponent x = words.word_T then
      if binary_ieee.float_Significand x = words.n2w 0 then
        binary_ieee.Infinity
      else binary_ieee.NaN
    else binary_ieee.Float (binary_ieee.float_to_real x)

mode a b c.
    machine_ieee.fp16_mul_add mode a b c =
    machine_ieee.float_to_fp16
      (binary_ieee.float_mul_add mode (machine_ieee.fp16_to_float a)
         (machine_ieee.fp16_to_float b) (machine_ieee.fp16_to_float c))

mode a b c.
    machine_ieee.fp16_mul_sub mode a b c =
    machine_ieee.float_to_fp16
      (binary_ieee.float_mul_sub mode (machine_ieee.fp16_to_float a)
         (machine_ieee.fp16_to_float b) (machine_ieee.fp16_to_float c))

mode c b a.
    machine_ieee.fp16_mul_add mode (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) (machine_ieee.float_to_fp16 c) =
    machine_ieee.float_to_fp16 (binary_ieee.float_mul_add mode a b c)

mode c b a.
    machine_ieee.fp16_mul_sub mode (machine_ieee.float_to_fp16 a)
      (machine_ieee.float_to_fp16 b) (machine_ieee.float_to_fp16 c) =
    machine_ieee.float_to_fp16 (binary_ieee.float_mul_sub mode a b c)

mode a b c.
    machine_ieee.fp32_mul_add mode a b c =
    machine_ieee.float_to_fp32
      (binary_ieee.float_mul_add mode (machine_ieee.fp32_to_float a)
         (machine_ieee.fp32_to_float b) (machine_ieee.fp32_to_float c))

mode a b c.
    machine_ieee.fp32_mul_sub mode a b c =
    machine_ieee.float_to_fp32
      (binary_ieee.float_mul_sub mode (machine_ieee.fp32_to_float a)
         (machine_ieee.fp32_to_float b) (machine_ieee.fp32_to_float c))

mode a b c.
    machine_ieee.fp64_mul_add mode a b c =
    machine_ieee.float_to_fp64
      (binary_ieee.float_mul_add mode (machine_ieee.fp64_to_float a)
         (machine_ieee.fp64_to_float b) (machine_ieee.fp64_to_float c))

mode a b c.
    machine_ieee.fp64_mul_sub mode a b c =
    machine_ieee.float_to_fp64
      (binary_ieee.float_mul_sub mode (machine_ieee.fp64_to_float a)
         (machine_ieee.fp64_to_float b) (machine_ieee.fp64_to_float c))

mode c b a.
    machine_ieee.fp32_mul_add mode (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) (machine_ieee.float_to_fp32 c) =
    machine_ieee.float_to_fp32 (binary_ieee.float_mul_add mode a b c)

mode c b a.
    machine_ieee.fp32_mul_sub mode (machine_ieee.float_to_fp32 a)
      (machine_ieee.float_to_fp32 b) (machine_ieee.float_to_fp32 c) =
    machine_ieee.float_to_fp32 (binary_ieee.float_mul_sub mode a b c)

mode c b a.
    machine_ieee.fp64_mul_add mode (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) (machine_ieee.float_to_fp64 c) =
    machine_ieee.float_to_fp64 (binary_ieee.float_mul_add mode a b c)

mode c b a.
    machine_ieee.fp64_mul_sub mode (machine_ieee.float_to_fp64 a)
      (machine_ieee.float_to_fp64 b) (machine_ieee.float_to_fp64 c) =
    machine_ieee.float_to_fp64 (binary_ieee.float_mul_sub mode a b c)

mode x y.
    binary_ieee.float_value x = binary_ieee.NaN
    binary_ieee.float_value y = binary_ieee.NaN
    binary_ieee.float_add mode x y =
    binary_ieee.float_some_nan bool.the_value

mode x y.
    binary_ieee.float_value x = binary_ieee.NaN
    binary_ieee.float_value y = binary_ieee.NaN
    binary_ieee.float_div mode x y =
    binary_ieee.float_some_nan bool.the_value

mode x y.
    binary_ieee.float_value x = binary_ieee.NaN
    binary_ieee.float_value y = binary_ieee.NaN
    binary_ieee.float_mul mode x y =
    binary_ieee.float_some_nan bool.the_value

mode x y.
    binary_ieee.float_value x = binary_ieee.NaN
    binary_ieee.float_value y = binary_ieee.NaN
    binary_ieee.float_sub mode x y =
    binary_ieee.float_some_nan bool.the_value

P.
    (f. P f)
    c1 c0 c.
      P
        (binary_ieee.float_Sign_fupd (const c1)
           (binary_ieee.float_Exponent_fupd (const c0)
              (binary_ieee.float_Significand_fupd (const c) bool.ARB)))

P.
    (f. P f)
    c1 c0 c.
      P
        (binary_ieee.float_Sign_fupd (const c1)
           (binary_ieee.float_Exponent_fupd (const c0)
              (binary_ieee.float_Significand_fupd (const c) bool.ARB)))

(a.
     binary_ieee.num2float_compare (binary_ieee.float_compare2num a) = a)
  r.
    (let n r in n < arithmetic.BIT2 1)
    binary_ieee.float_compare2num (binary_ieee.num2float_compare r) = r

(a. binary_ieee.num2rounding (binary_ieee.rounding2num a) = a)
  r.
    (let n r in n < arithmetic.BIT2 1)
    binary_ieee.rounding2num (binary_ieee.num2rounding r) = r

n m.
    Number.Real.≤ (Number.Real.fromNatural (arithmetic.BIT2 0)) n
    Number.Real.≤ (Number.Real.fromNatural (arithmetic.BIT2 0)) m
    Number.Real.≤ (Number.Real.fromNatural (arithmetic.BIT2 0))
      (Number.Real.* n m)

e1 e2.
    ¬(e2 = words.n2w 0)
    (Number.Real.≤ (binary_ieee.ULP (e1, bool.the_value))
       (binary_ieee.ULP (e2, bool.the_value)) words.word_ls e1 e2)

binary_ieee.num2float_compare 0 = binary_ieee.LT
  binary_ieee.num2float_compare 1 = binary_ieee.EQ
  binary_ieee.num2float_compare (arithmetic.BIT2 0) = binary_ieee.GT
  binary_ieee.num2float_compare 3 = binary_ieee.UN

binary_ieee.num2rounding 0 = binary_ieee.roundTiesToEven
  binary_ieee.num2rounding 1 = binary_ieee.roundTowardPositive
  binary_ieee.num2rounding (arithmetic.BIT2 0) =
  binary_ieee.roundTowardNegative
  binary_ieee.num2rounding 3 = binary_ieee.roundTowardZero

binary_ieee.float_compare2num binary_ieee.LT = 0
  binary_ieee.float_compare2num binary_ieee.EQ = 1
  binary_ieee.float_compare2num binary_ieee.GT = arithmetic.BIT2 0
  binary_ieee.float_compare2num binary_ieee.UN = 3

binary_ieee.rounding2num binary_ieee.roundTiesToEven = 0
  binary_ieee.rounding2num binary_ieee.roundTowardPositive = 1
  binary_ieee.rounding2num binary_ieee.roundTowardNegative =
  arithmetic.BIT2 0
  binary_ieee.rounding2num binary_ieee.roundTowardZero = 3

f0 f1 f2.
    fn.
      (a. fn (binary_ieee.Float a) = f0 a)
      fn binary_ieee.Infinity = f1 fn binary_ieee.NaN = f2

mode toneg r.
    binary_ieee.float_round mode toneg r =
    bool.LET
      (λx.
         if binary_ieee.float_is_zero x then
           if toneg then binary_ieee.float_minus_zero bool.the_value
           else binary_ieee.float_plus_zero bool.the_value
         else x) (binary_ieee.round mode r)

r r'.
    r < arithmetic.BIT2 1 r' < arithmetic.BIT2 1
    (binary_ieee.num2float_compare r = binary_ieee.num2float_compare r'
     r = r')

r r'.
    r < arithmetic.BIT2 1 r' < arithmetic.BIT2 1
    (binary_ieee.num2rounding r = binary_ieee.num2rounding r' r = r')

f1 f2.
    f1 = f2
    binary_ieee.float_Sign f1 = binary_ieee.float_Sign f2
    binary_ieee.float_Exponent f1 = binary_ieee.float_Exponent f2
    binary_ieee.float_Significand f1 = binary_ieee.float_Significand f2

x.
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs x)) (binary_ieee.ulp bool.the_value)
    binary_ieee.round binary_ieee.roundTiesToEven x =
    binary_ieee.float_plus_zero bool.the_value
    binary_ieee.round binary_ieee.roundTiesToEven x =
    binary_ieee.float_minus_zero bool.the_value

x0 x1 x2 x3.
    f.
      f binary_ieee.LT = x0 f binary_ieee.EQ = x1
      f binary_ieee.GT = x2 f binary_ieee.UN = x3

x0 x1 x2 x3.
    f.
      f binary_ieee.roundTiesToEven = x0
      f binary_ieee.roundTowardPositive = x1
      f binary_ieee.roundTowardNegative = x2
      f binary_ieee.roundTowardZero = x3

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_div mode x
      (binary_ieee.float_minus_infinity bool.the_value) =
    if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_minus_zero bool.the_value
    else binary_ieee.float_plus_zero bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_div mode x
      (binary_ieee.float_plus_infinity bool.the_value) =
    if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_plus_zero bool.the_value
    else binary_ieee.float_minus_zero bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_div mode
      (binary_ieee.float_minus_infinity bool.the_value) x =
    if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_minus_infinity bool.the_value
    else binary_ieee.float_plus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_div mode
      (binary_ieee.float_plus_infinity bool.the_value) x =
    if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_plus_infinity bool.the_value
    else binary_ieee.float_minus_infinity bool.the_value

mode c b a.
    machine_ieee.fp16_mul_add mode (words.n2w a) (words.n2w b)
      (words.n2w c) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_mul_add mode
         (machine_ieee.fp16_to_float (words.n2w a))
         (machine_ieee.fp16_to_float (words.n2w b))
         (machine_ieee.fp16_to_float (words.n2w c)))

mode c b a.
    machine_ieee.fp16_mul_sub mode (words.n2w a) (words.n2w b)
      (words.n2w c) =
    machine_ieee.float_to_fp16
      (binary_ieee.float_mul_sub mode
         (machine_ieee.fp16_to_float (words.n2w a))
         (machine_ieee.fp16_to_float (words.n2w b))
         (machine_ieee.fp16_to_float (words.n2w c)))

mode c b a.
    machine_ieee.fp32_mul_add mode (words.n2w a) (words.n2w b)
      (words.n2w c) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_mul_add mode
         (machine_ieee.fp32_to_float (words.n2w a))
         (machine_ieee.fp32_to_float (words.n2w b))
         (machine_ieee.fp32_to_float (words.n2w c)))

mode c b a.
    machine_ieee.fp32_mul_sub mode (words.n2w a) (words.n2w b)
      (words.n2w c) =
    machine_ieee.float_to_fp32
      (binary_ieee.float_mul_sub mode
         (machine_ieee.fp32_to_float (words.n2w a))
         (machine_ieee.fp32_to_float (words.n2w b))
         (machine_ieee.fp32_to_float (words.n2w c)))

mode c b a.
    machine_ieee.fp64_mul_add mode (words.n2w a) (words.n2w b)
      (words.n2w c) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_mul_add mode
         (machine_ieee.fp64_to_float (words.n2w a))
         (machine_ieee.fp64_to_float (words.n2w b))
         (machine_ieee.fp64_to_float (words.n2w c)))

mode c b a.
    machine_ieee.fp64_mul_sub mode (words.n2w a) (words.n2w b)
      (words.n2w c) =
    machine_ieee.float_to_fp64
      (binary_ieee.float_mul_sub mode
         (machine_ieee.fp64_to_float (words.n2w a))
         (machine_ieee.fp64_to_float (words.n2w b))
         (machine_ieee.fp64_to_float (words.n2w c)))

x y.
    ¬(binary_ieee.float_to_real x = binary_ieee.float_to_real y)
    ¬binary_ieee.exponent_boundary y x
    Number.Real.≤
      (binary_ieee.ULP (binary_ieee.float_Exponent x, bool.the_value))
      (Number.Real.abs
         (Number.Real.- (binary_ieee.float_to_real x)
            (binary_ieee.float_to_real y)))

f c1 c0 c.
    binary_ieee.float_Sign_fupd (const c1)
      (binary_ieee.float_Exponent_fupd (const c0)
         (binary_ieee.float_Significand_fupd (const c) f)) =
    binary_ieee.float_Sign_fupd (const c1)
      (binary_ieee.float_Exponent_fupd (const c0)
         (binary_ieee.float_Significand_fupd (const c) bool.ARB))

binary_ieee.float_negate
    (binary_ieee.float_plus_infinity bool.the_value) =
  binary_ieee.float_minus_infinity bool.the_value
  binary_ieee.float_negate
    (binary_ieee.float_minus_infinity bool.the_value) =
  binary_ieee.float_plus_infinity bool.the_value
  binary_ieee.float_abs (binary_ieee.float_plus_infinity bool.the_value) =
  binary_ieee.float_plus_infinity bool.the_value
  binary_ieee.float_abs (binary_ieee.float_minus_infinity bool.the_value) =
  binary_ieee.float_plus_infinity bool.the_value

mode x.
    binary_ieee.float_sqrt mode x =
    if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_value_CASE (binary_ieee.float_value x)
        (λr. binary_ieee.float_round mode (transc.sqrt r))
        (binary_ieee.float_plus_infinity bool.the_value)
        (binary_ieee.float_some_nan bool.the_value)
    else binary_ieee.float_some_nan bool.the_value

p s x.
    binary_ieee.closest_such p s x =
    select a.
      binary_ieee.is_closest s x a
      b. binary_ieee.is_closest s x b p b p a

(m.
     binary_ieee.float_round_to_integral m
       (binary_ieee.float_minus_infinity bool.the_value) =
     binary_ieee.float_minus_infinity bool.the_value)
  (m.
     binary_ieee.float_round_to_integral m
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_plus_infinity bool.the_value)
  m.
    binary_ieee.float_round_to_integral m
      (binary_ieee.float_some_nan bool.the_value) =
    binary_ieee.float_some_nan bool.the_value

binary_ieee.ULP (e, bool.the_value) =
  real./
    (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
       (if e = words.n2w 0 then 1 else words.w2n e))
    (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
       (words.INT_MAX bool.the_value + fcp.dimindex bool.the_value))

¬(binary_ieee.LT = binary_ieee.EQ) ¬(binary_ieee.LT = binary_ieee.GT)
  ¬(binary_ieee.LT = binary_ieee.UN) ¬(binary_ieee.EQ = binary_ieee.GT)
  ¬(binary_ieee.EQ = binary_ieee.UN) ¬(binary_ieee.GT = binary_ieee.UN)

¬(binary_ieee.roundTiesToEven = binary_ieee.roundTowardPositive)
  ¬(binary_ieee.roundTiesToEven = binary_ieee.roundTowardNegative)
  ¬(binary_ieee.roundTiesToEven = binary_ieee.roundTowardZero)
  ¬(binary_ieee.roundTowardPositive = binary_ieee.roundTowardNegative)
  ¬(binary_ieee.roundTowardPositive = binary_ieee.roundTowardZero)
  ¬(binary_ieee.roundTowardNegative = binary_ieee.roundTowardZero)

a0 a1 a2 a0' a1' a2'.
    binary_ieee.recordtype.float a0 a1 a2 =
    binary_ieee.recordtype.float a0' a1' a2'
    a0 = a0' a1 = a1' a2 = a2'

s x a.
    binary_ieee.is_closest s x a
    bool.IN a s
    b.
      bool.IN b s
      Number.Real.≤
        (Number.Real.abs (Number.Real.- (binary_ieee.float_to_real a) x))
        (Number.Real.abs (Number.Real.- (binary_ieee.float_to_real b) x))

binary_ieee.largest bool.the_value =
  Number.Real.*
    (real./
       (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
          (arithmetic.- (words.UINT_MAX bool.the_value) 1))
       (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
          (words.INT_MAX bool.the_value)))
    (Number.Real.- (Number.Real.fromNatural (arithmetic.BIT2 0))
       (realax.inv
          (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
             (fcp.dimindex bool.the_value))))

binary_ieee.largest bool.the_value =
  real./
    (Number.Real.*
       (Number.Real.fromNatural
          (arithmetic.BIT2 0
           arithmetic.- (words.UINT_MAX bool.the_value) 1))
       (Number.Real.- (Number.Real.fromNatural (arithmetic.BIT2 0))
          (real./ 1
             (Number.Real.fromNatural (words.dimword bool.the_value)))))
    (Number.Real.fromNatural
       (arithmetic.BIT2 0 words.INT_MAX bool.the_value))

binary_ieee.threshold bool.the_value =
  Number.Real.*
    (real./
       (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
          (arithmetic.- (words.UINT_MAX bool.the_value) 1))
       (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
          (words.INT_MAX bool.the_value)))
    (Number.Real.- (Number.Real.fromNatural (arithmetic.BIT2 0))
       (realax.inv
          (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
             (suc (fcp.dimindex bool.the_value)))))

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'float'.
           (a0'.
              (a0 a1 a2.
                 a0' =
                 (let a0 a0 in
                  λa1 a2.
                    ind_type.CONSTR 0 (a0, a1, a2) (λn. ind_type.BOTTOM))
                   a1 a2) 'float' a0') 'float' a0') rep

¬binary_ieee.float_is_zero (binary_ieee.float_some_nan bool.the_value)
  ¬binary_ieee.float_is_finite
      (binary_ieee.float_some_nan bool.the_value)
  ¬binary_ieee.float_is_integral
      (binary_ieee.float_some_nan bool.the_value)
  binary_ieee.float_is_nan (binary_ieee.float_some_nan bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_some_nan bool.the_value)
  ¬binary_ieee.float_is_subnormal
      (binary_ieee.float_some_nan bool.the_value)
  ¬binary_ieee.float_is_infinite
      (binary_ieee.float_some_nan bool.the_value)

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_mul mode x
      (binary_ieee.float_minus_infinity bool.the_value) =
    if r = 0 then binary_ieee.float_some_nan bool.the_value
    else if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_minus_infinity bool.the_value
    else binary_ieee.float_plus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_mul mode x
      (binary_ieee.float_plus_infinity bool.the_value) =
    if r = 0 then binary_ieee.float_some_nan bool.the_value
    else if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_plus_infinity bool.the_value
    else binary_ieee.float_minus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_mul mode
      (binary_ieee.float_minus_infinity bool.the_value) x =
    if r = 0 then binary_ieee.float_some_nan bool.the_value
    else if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_minus_infinity bool.the_value
    else binary_ieee.float_plus_infinity bool.the_value

mode x r.
    binary_ieee.float_value x = binary_ieee.Float r
    binary_ieee.float_mul mode
      (binary_ieee.float_plus_infinity bool.the_value) x =
    if r = 0 then binary_ieee.float_some_nan bool.the_value
    else if binary_ieee.float_Sign x = words.n2w 0 then
      binary_ieee.float_plus_infinity bool.the_value
    else binary_ieee.float_minus_infinity bool.the_value

binary_ieee.threshold bool.the_value =
  real./
    (Number.Real.*
       (Number.Real.fromNatural
          (arithmetic.BIT2 0
           arithmetic.- (words.UINT_MAX bool.the_value) 1))
       (Number.Real.- (Number.Real.fromNatural (arithmetic.BIT2 0))
          (real./ 1
             (Number.Real.fromNatural
                (arithmetic.BIT2 0 * words.dimword bool.the_value)))))
    (Number.Real.fromNatural
       (arithmetic.BIT2 0 words.INT_MAX bool.the_value))

binary_ieee.ULP =
  relation.WFREC (select R. wellFounded R)
    (λULP a.
       pair.pair_CASE a
         (λe v1.
            id
              (real./
                 (Number.Real.↑
                    (Number.Real.fromNatural (arithmetic.BIT2 0))
                    (if e = words.n2w 0 then 1 else words.w2n e))
                 (Number.Real.↑
                    (Number.Real.fromNatural (arithmetic.BIT2 0))
                    (words.INT_MAX bool.the_value +
                     fcp.dimindex bool.the_value)))))

mode x y r1 r2.
    binary_ieee.float_value x = binary_ieee.Float r1
    binary_ieee.float_value y = binary_ieee.Float r2
    binary_ieee.float_mul mode x y =
    binary_ieee.float_round mode
      (¬(binary_ieee.float_Sign x = binary_ieee.float_Sign y))
      (Number.Real.* r1 r2)

x v0 v1 v2 v3.
    binary_ieee.float_compare_CASE x v0 v1 v2 v3 =
    let m binary_ieee.float_compare2num x in
    if m < 1 then v0
    else if m < arithmetic.BIT2 0 then v1
    else if m = arithmetic.BIT2 0 then v2
    else v3

x v0 v1 v2 v3.
    binary_ieee.rounding_CASE x v0 v1 v2 v3 =
    let m binary_ieee.rounding2num x in
    if m < 1 then v0
    else if m < arithmetic.BIT2 0 then v1
    else if m = arithmetic.BIT2 0 then v2
    else v3

(c c0 c1.
     binary_ieee.float_Sign (binary_ieee.recordtype.float c c0 c1) = c)
  (c c0 c1.
     binary_ieee.float_Exponent (binary_ieee.recordtype.float c c0 c1) =
     c0)
  c c0 c1.
    binary_ieee.float_Significand (binary_ieee.recordtype.float c c0 c1) =
    c1

M M' f.
    M = M'
    (a0 a1 a2.
       M' = binary_ieee.recordtype.float a0 a1 a2
       f a0 a1 a2 = f' a0 a1 a2)
    binary_ieee.float_CASE M f = binary_ieee.float_CASE M' f'

n.
    machine_ieee.fp16_to_float (words.n2w n) =
    bool.LET
      (pair.UNCURRY
         (λq f.
            bool.LET
              (pair.UNCURRY
                 (λs e.
                    binary_ieee.float_Sign_fupd
                      (const (words.n2w (s mod arithmetic.BIT2 0)))
                      (binary_ieee.float_Exponent_fupd
                         (const (words.n2w e))
                         (binary_ieee.float_Significand_fupd
                            (const (words.n2w f)) bool.ARB))))
              (bit.DIVMOD_2EXP (bit1 (arithmetic.BIT2 0)) q)))
      (bit.DIVMOD_2EXP (arithmetic.BIT2 (arithmetic.BIT2 1)) n)

to_float from_float from_real m w.
    machine_ieee.convert to_float from_float from_real m w =
    bool.LET
      (λf.
         binary_ieee.float_value_CASE (binary_ieee.float_value f)
           (λr. from_real m r)
           (from_float
              (if binary_ieee.float_Sign f = words.n2w 0 then
                 binary_ieee.float_plus_infinity bool.the_value
               else binary_ieee.float_minus_infinity bool.the_value))
           (from_float (binary_ieee.float_some_nan bool.the_value)))
      (to_float w)

(b c d.
     Number.Real.abs
       (Number.Real.*
          (Number.Real.* (Number.Real.↑ (Number.Real.~ 1) (words.w2n b)) c)
          d) = Number.Real.abs (Number.Real.* c d))
  b c.
    Number.Real.abs
      (Number.Real.* (Number.Real.↑ (Number.Real.~ 1) (words.w2n b)) c) =
    Number.Real.abs c

¬binary_ieee.float_is_zero (binary_ieee.float_bottom bool.the_value)
  binary_ieee.float_is_finite (binary_ieee.float_bottom bool.the_value)
  ¬binary_ieee.float_is_nan (binary_ieee.float_bottom bool.the_value)
  (binary_ieee.float_is_normal (binary_ieee.float_bottom bool.the_value)
   ¬(fcp.dimindex bool.the_value = 1))
  (binary_ieee.float_is_subnormal
     (binary_ieee.float_bottom bool.the_value)
   fcp.dimindex bool.the_value = 1)
  ¬binary_ieee.float_is_infinite (binary_ieee.float_bottom bool.the_value)

¬binary_ieee.float_is_zero (binary_ieee.float_top bool.the_value)
  binary_ieee.float_is_finite (binary_ieee.float_top bool.the_value)
  ¬binary_ieee.float_is_nan (binary_ieee.float_top bool.the_value)
  (binary_ieee.float_is_normal (binary_ieee.float_top bool.the_value)
   ¬(fcp.dimindex bool.the_value = 1))
  (binary_ieee.float_is_subnormal (binary_ieee.float_top bool.the_value)
   fcp.dimindex bool.the_value = 1)
  ¬binary_ieee.float_is_infinite (binary_ieee.float_top bool.the_value)

(a f v v1.
     binary_ieee.float_value_CASE (binary_ieee.Float a) f v v1 = f a)
  (f v v1. binary_ieee.float_value_CASE binary_ieee.Infinity f v v1 = v)
  f v v1. binary_ieee.float_value_CASE binary_ieee.NaN f v v1 = v1

n.
    machine_ieee.fp32_to_float (words.n2w n) =
    bool.LET
      (pair.UNCURRY
         (λq f.
            bool.LET
              (pair.UNCURRY
                 (λs e.
                    binary_ieee.float_Sign_fupd
                      (const (words.n2w (s mod arithmetic.BIT2 0)))
                      (binary_ieee.float_Exponent_fupd
                         (const (words.n2w e))
                         (binary_ieee.float_Significand_fupd
                            (const (words.n2w f)) bool.ARB))))
              (bit.DIVMOD_2EXP (arithmetic.BIT2 3) q)))
      (bit.DIVMOD_2EXP (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))) n)

w.
    machine_ieee.fp16_to_float w =
    binary_ieee.float_Sign_fupd (const (words.word_extract 15 15 w))
      (binary_ieee.float_Exponent_fupd
         (const
            (words.word_extract
               (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))
               (arithmetic.BIT2 (arithmetic.BIT2 1)) w))
         (binary_ieee.float_Significand_fupd
            (const (words.word_extract (bit1 (arithmetic.BIT2 1)) 0 w))
            bool.ARB))

rep.
    bool.TYPE_DEFINITION
      (λa0.
         'float_value'.
           (a0.
              (a.
                 a0 =
                 let a a in ind_type.CONSTR 0 a (λn. ind_type.BOTTOM))
              a0 = ind_type.CONSTR (suc 0) bool.ARB (λn. ind_type.BOTTOM)
              a0 =
              ind_type.CONSTR (suc (suc 0)) bool.ARB
                (λn. ind_type.BOTTOM) 'float_value' a0)
           'float_value' a0) rep

n.
    machine_ieee.fp64_to_float (words.n2w n) =
    bool.LET
      (pair.UNCURRY
         (λq f.
            bool.LET
              (pair.UNCURRY
                 (λs e.
                    binary_ieee.float_Sign_fupd
                      (const (words.n2w (s mod arithmetic.BIT2 0)))
                      (binary_ieee.float_Exponent_fupd
                         (const (words.n2w e))
                         (binary_ieee.float_Significand_fupd
                            (const (words.n2w f)) bool.ARB))))
              (bit.DIVMOD_2EXP (bit1 (bit1 (arithmetic.BIT2 0))) q)))
      (bit.DIVMOD_2EXP
         (arithmetic.BIT2
            (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))) n)

c11 c01 c1 c12 c02 c2.
    binary_ieee.float_Sign_fupd (const c11)
      (binary_ieee.float_Exponent_fupd (const c01)
         (binary_ieee.float_Significand_fupd (const c1) bool.ARB)) =
    binary_ieee.float_Sign_fupd (const c12)
      (binary_ieee.float_Exponent_fupd (const c02)
         (binary_ieee.float_Significand_fupd (const c2) bool.ARB))
    c11 = c12 c01 = c02 c1 = c2

y x r.
    binary_ieee.float_value y = binary_ieee.Float r
    Number.Real.< (Number.Real.abs (Number.Real.- r x))
      (binary_ieee.ULP (binary_ieee.float_Exponent y, bool.the_value))
    Number.Real.≤ (Number.Real.abs r) (Number.Real.abs x)
    Number.Real.≤ (binary_ieee.ulp bool.the_value) (Number.Real.abs x)
    Number.Real.≤ (Number.Real.abs x)
      (binary_ieee.largest bool.the_value)
    binary_ieee.round binary_ieee.roundTowardZero x = y

y x.
    binary_ieee.exponent_boundary y x
    binary_ieee.float_Sign x = binary_ieee.float_Sign y
    words.w2n (binary_ieee.float_Exponent x) =
    words.w2n (binary_ieee.float_Exponent y) + 1
    ¬(binary_ieee.float_Exponent x = words.n2w 1)
    binary_ieee.float_Significand y = words.word_2comp (words.n2w 1)
    binary_ieee.float_Significand x = words.n2w 0

w.
    machine_ieee.fp32_to_float w =
    binary_ieee.float_Sign_fupd (const (words.word_extract 31 31 w))
      (binary_ieee.float_Exponent_fupd
         (const
            (words.word_extract
               (arithmetic.BIT2
                  (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))))
               (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))) w))
         (binary_ieee.float_Significand_fupd
            (const
               (words.word_extract
                  (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 1))) 0
                  w)) bool.ARB))

a b x.
    ¬binary_ieee.exponent_boundary b a
    Number.Real.<
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs (Number.Real.- (binary_ieee.float_to_real a) x)))
      (binary_ieee.ULP (binary_ieee.float_Exponent a, bool.the_value))
    Number.Real.<
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs (Number.Real.- (binary_ieee.float_to_real b) x)))
      (binary_ieee.ULP (binary_ieee.float_Exponent a, bool.the_value))
    ¬binary_ieee.float_is_zero a b = a

(g f0 f.
     binary_ieee.float_Exponent_fupd f0 (binary_ieee.float_Sign_fupd g f) =
     binary_ieee.float_Sign_fupd g
       (binary_ieee.float_Exponent_fupd f0 f))
  (g f0 f.
     binary_ieee.float_Significand_fupd f0
       (binary_ieee.float_Sign_fupd g f) =
     binary_ieee.float_Sign_fupd g
       (binary_ieee.float_Significand_fupd f0 f))
  g f0 f.
    binary_ieee.float_Significand_fupd f0
      (binary_ieee.float_Exponent_fupd g f) =
    binary_ieee.float_Exponent_fupd g
      (binary_ieee.float_Significand_fupd f0 f)

(g f0 f.
     binary_ieee.float_Sign_fupd f0 (binary_ieee.float_Sign_fupd g f) =
     binary_ieee.float_Sign_fupd (f0 g) f)
  (g f0 f.
     binary_ieee.float_Exponent_fupd f0
       (binary_ieee.float_Exponent_fupd g f) =
     binary_ieee.float_Exponent_fupd (f0 g) f)
  g f0 f.
    binary_ieee.float_Significand_fupd f0
      (binary_ieee.float_Significand_fupd g f) =
    binary_ieee.float_Significand_fupd (f0 g) f

a b x.
    ¬binary_ieee.exponent_boundary b a
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 1))
         (Number.Real.abs (Number.Real.- (binary_ieee.float_to_real a) x)))
      (binary_ieee.ULP (binary_ieee.float_Exponent a, bool.the_value))
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 1))
         (Number.Real.abs (Number.Real.- (binary_ieee.float_to_real b) x)))
      (binary_ieee.ULP (binary_ieee.float_Exponent a, bool.the_value))
    ¬binary_ieee.float_is_zero a b = a

w.
    machine_ieee.fp64_to_float w =
    binary_ieee.float_Sign_fupd (const (words.word_extract 63 63 w))
      (binary_ieee.float_Exponent_fupd
         (const
            (words.word_extract
               (arithmetic.BIT2
                  (arithmetic.BIT2
                     (arithmetic.BIT2
                        (arithmetic.BIT2 (arithmetic.BIT2 0)))))
               (arithmetic.BIT2
                  (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))) w))
         (binary_ieee.float_Significand_fupd
            (const
               (words.word_extract
                  (bit1
                     (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))) 0
                  w)) bool.ARB))

M M' f v v1.
    M = M' (a. M' = binary_ieee.Float a f a = f' a)
    (M' = binary_ieee.Infinity v = v')
    (M' = binary_ieee.NaN v1 = v1')
    binary_ieee.float_value_CASE M f v v1 =
    binary_ieee.float_value_CASE M' f' v' v1'

mode toneg r s e f.
    binary_ieee.round mode r =
    binary_ieee.float_Sign_fupd (const s)
      (binary_ieee.float_Exponent_fupd (const e)
         (binary_ieee.float_Significand_fupd (const f) bool.ARB))
    (¬(e = words.n2w 0) ¬(f = words.n2w 0))
    binary_ieee.float_round mode toneg r =
    binary_ieee.float_Sign_fupd (const s)
      (binary_ieee.float_Exponent_fupd (const e)
         (binary_ieee.float_Significand_fupd (const f) bool.ARB))

mode x y r1 r2.
    binary_ieee.float_value x = binary_ieee.Float r1
    binary_ieee.float_value y = binary_ieee.Float r2
    binary_ieee.float_add mode x y =
    binary_ieee.float_round mode
      (if r1 = 0 r2 = 0
          binary_ieee.float_Sign x = binary_ieee.float_Sign y
       then binary_ieee.float_Sign x = words.n2w 1
       else mode = binary_ieee.roundTowardNegative) (Number.Real.+ r1 r2)

a b x.
    ¬binary_ieee.exponent_boundary b a
    Number.Real.<
      (Number.Real.abs (Number.Real.- x (binary_ieee.float_to_real a)))
      (binary_ieee.ULP (binary_ieee.float_Exponent a, bool.the_value))
    Number.Real.<
      (Number.Real.abs (Number.Real.- x (binary_ieee.float_to_real b)))
      (binary_ieee.ULP (binary_ieee.float_Exponent a, bool.the_value))
    Number.Real.≤ (Number.Real.abs (binary_ieee.float_to_real a))
      (Number.Real.abs x)
    Number.Real.≤ (Number.Real.abs (binary_ieee.float_to_real b))
      (Number.Real.abs x) ¬binary_ieee.float_is_zero a b = a

mode x y r1 r2.
    binary_ieee.float_value x = binary_ieee.Float r1
    binary_ieee.float_value y = binary_ieee.Float r2
    binary_ieee.float_sub mode x y =
    binary_ieee.float_round mode
      (if r1 = 0 r2 = 0
          ¬(binary_ieee.float_Sign x = binary_ieee.float_Sign y)
       then binary_ieee.float_Sign x = words.n2w 1
       else mode = binary_ieee.roundTowardNegative) (Number.Real.- r1 r2)

(f c c0 c1.
     binary_ieee.float_Sign_fupd f (binary_ieee.recordtype.float c c0 c1) =
     binary_ieee.recordtype.float (f c) c0 c1)
  (f c c0 c1.
     binary_ieee.float_Exponent_fupd f
       (binary_ieee.recordtype.float c c0 c1) =
     binary_ieee.recordtype.float c (f c0) c1)
  f c c0 c1.
    binary_ieee.float_Significand_fupd f
      (binary_ieee.recordtype.float c c0 c1) =
    binary_ieee.recordtype.float c c0 (f c1)

mode x y r1 r2.
    binary_ieee.float_value x = binary_ieee.Float r1
    binary_ieee.float_value y = binary_ieee.Float r2
    binary_ieee.float_div mode x y =
    if r2 = 0 then
      if r1 = 0 then binary_ieee.float_some_nan bool.the_value
      else if binary_ieee.float_Sign x = binary_ieee.float_Sign y then
        binary_ieee.float_plus_infinity bool.the_value
      else binary_ieee.float_minus_infinity bool.the_value
    else
      binary_ieee.float_round mode
        (¬(binary_ieee.float_Sign x = binary_ieee.float_Sign y))
        (real./ r1 r2)

M M' v0 v1 v2 v3.
    M = M' (M' = binary_ieee.LT v0 = v0')
    (M' = binary_ieee.EQ v1 = v1') (M' = binary_ieee.GT v2 = v2')
    (M' = binary_ieee.UN v3 = v3')
    binary_ieee.float_compare_CASE M v0 v1 v2 v3 =
    binary_ieee.float_compare_CASE M' v0' v1' v2' v3'

M M' v0 v1 v2 v3.
    M = M' (M' = binary_ieee.roundTiesToEven v0 = v0')
    (M' = binary_ieee.roundTowardPositive v1 = v1')
    (M' = binary_ieee.roundTowardNegative v2 = v2')
    (M' = binary_ieee.roundTowardZero v3 = v3')
    binary_ieee.rounding_CASE M v0 v1 v2 v3 =
    binary_ieee.rounding_CASE M' v0' v1' v2' v3'

(v0 v1 v2 v3.
     binary_ieee.float_compare_CASE binary_ieee.LT v0 v1 v2 v3 = v0)
  (v0 v1 v2 v3.
     binary_ieee.float_compare_CASE binary_ieee.EQ v0 v1 v2 v3 = v1)
  (v0 v1 v2 v3.
     binary_ieee.float_compare_CASE binary_ieee.GT v0 v1 v2 v3 = v2)
  v0 v1 v2 v3.
    binary_ieee.float_compare_CASE binary_ieee.UN v0 v1 v2 v3 = v3

(v0 v1 v2 v3.
     binary_ieee.rounding_CASE binary_ieee.roundTiesToEven v0 v1 v2 v3 =
     v0)
  (v0 v1 v2 v3.
     binary_ieee.rounding_CASE binary_ieee.roundTowardPositive v0 v1 v2
       v3 = v1)
  (v0 v1 v2 v3.
     binary_ieee.rounding_CASE binary_ieee.roundTowardNegative v0 v1 v2
       v3 = v2)
  v0 v1 v2 v3.
    binary_ieee.rounding_CASE binary_ieee.roundTowardZero v0 v1 v2 v3 = v3

binary_ieee.float_is_zero (binary_ieee.float_plus_zero bool.the_value)
  binary_ieee.float_is_zero (binary_ieee.float_minus_zero bool.the_value)
  binary_ieee.float_is_finite
    (binary_ieee.float_plus_zero bool.the_value)
  binary_ieee.float_is_finite
    (binary_ieee.float_minus_zero bool.the_value)
  binary_ieee.float_is_integral
    (binary_ieee.float_plus_zero bool.the_value)
  binary_ieee.float_is_integral
    (binary_ieee.float_minus_zero bool.the_value)
  ¬binary_ieee.float_is_nan (binary_ieee.float_plus_zero bool.the_value)
  ¬binary_ieee.float_is_nan (binary_ieee.float_minus_zero bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_plus_zero bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_minus_zero bool.the_value)
  ¬binary_ieee.float_is_subnormal
      (binary_ieee.float_plus_zero bool.the_value)
  ¬binary_ieee.float_is_subnormal
      (binary_ieee.float_minus_zero bool.the_value)
  ¬binary_ieee.float_is_infinite
      (binary_ieee.float_plus_zero bool.the_value)
  ¬binary_ieee.float_is_infinite
      (binary_ieee.float_minus_zero bool.the_value)

¬binary_ieee.float_is_zero
      (binary_ieee.float_plus_infinity bool.the_value)
  ¬binary_ieee.float_is_zero
      (binary_ieee.float_minus_infinity bool.the_value)
  ¬binary_ieee.float_is_finite
      (binary_ieee.float_plus_infinity bool.the_value)
  ¬binary_ieee.float_is_finite
      (binary_ieee.float_minus_infinity bool.the_value)
  ¬binary_ieee.float_is_integral
      (binary_ieee.float_plus_infinity bool.the_value)
  ¬binary_ieee.float_is_integral
      (binary_ieee.float_minus_infinity bool.the_value)
  ¬binary_ieee.float_is_nan
      (binary_ieee.float_plus_infinity bool.the_value)
  ¬binary_ieee.float_is_nan
      (binary_ieee.float_minus_infinity bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_plus_infinity bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_minus_infinity bool.the_value)
  ¬binary_ieee.float_is_subnormal
      (binary_ieee.float_plus_infinity bool.the_value)
  ¬binary_ieee.float_is_subnormal
      (binary_ieee.float_minus_infinity bool.the_value)
  binary_ieee.float_is_infinite
    (binary_ieee.float_plus_infinity bool.the_value)
  binary_ieee.float_is_infinite
    (binary_ieee.float_minus_infinity bool.the_value)

mode x.
    binary_ieee.float_to_int mode x =
    binary_ieee.float_value_CASE (binary_ieee.float_value x)
      (λr.
         Data.Option.some
           (binary_ieee.rounding_CASE mode
              (bool.LET
                 (λf.
                    bool.LET
                      (λdf.
                         if Number.Real.< df
                              (real./ 1
                                 (Number.Real.fromNatural
                                    (arithmetic.BIT2 0)))
                            df =
                            real./ 1
                              (Number.Real.fromNatural
                                 (arithmetic.BIT2 0))
                            even (integer.Num (integer.ABS f))
                         then f
                         else intreal.INT_CEILING r)
                      (Number.Real.abs
                         (Number.Real.- r (intreal.real_of_int f))))
                 (intreal.INT_FLOOR r)) (intreal.INT_CEILING r)
              (intreal.INT_FLOOR r)
              (if binary_ieee.float_Sign x = words.n2w 1 then
                 intreal.INT_CEILING r
               else intreal.INT_FLOOR r))) Data.Option.none
      Data.Option.none

y x r.
    binary_ieee.float_value y = binary_ieee.Float r
    (binary_ieee.float_Significand y = words.n2w 0
     ¬(binary_ieee.float_Exponent y = words.n2w 1)
     ¬Number.Real.≤ (Number.Real.abs r) (Number.Real.abs x))
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 1))
         (Number.Real.abs (Number.Real.- r x)))
      (binary_ieee.ULP (binary_ieee.float_Exponent y, bool.the_value))
    Number.Real.< (binary_ieee.ulp bool.the_value)
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs x))
    Number.Real.< (Number.Real.abs x)
      (binary_ieee.threshold bool.the_value)
    binary_ieee.round binary_ieee.roundTiesToEven x = y

(mode x.
     binary_ieee.float_add mode (binary_ieee.float_some_nan bool.the_value)
       x = binary_ieee.float_some_nan bool.the_value)
  (mode x.
     binary_ieee.float_add mode x
       (binary_ieee.float_some_nan bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_add mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_minus_infinity bool.the_value) =
     binary_ieee.float_minus_infinity bool.the_value)
  (mode.
     binary_ieee.float_add mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_add mode
       (binary_ieee.float_plus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_plus_infinity bool.the_value)
  mode.
    binary_ieee.float_add mode
      (binary_ieee.float_plus_infinity bool.the_value)
      (binary_ieee.float_minus_infinity bool.the_value) =
    binary_ieee.float_some_nan bool.the_value

(mode x.
     binary_ieee.float_div mode (binary_ieee.float_some_nan bool.the_value)
       x = binary_ieee.float_some_nan bool.the_value)
  (mode x.
     binary_ieee.float_div mode x
       (binary_ieee.float_some_nan bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_div mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_minus_infinity bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_div mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_div mode
       (binary_ieee.float_plus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  mode.
    binary_ieee.float_div mode
      (binary_ieee.float_plus_infinity bool.the_value)
      (binary_ieee.float_minus_infinity bool.the_value) =
    binary_ieee.float_some_nan bool.the_value

(mode x.
     binary_ieee.float_mul mode (binary_ieee.float_some_nan bool.the_value)
       x = binary_ieee.float_some_nan bool.the_value)
  (mode x.
     binary_ieee.float_mul mode x
       (binary_ieee.float_some_nan bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_mul mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_minus_infinity bool.the_value) =
     binary_ieee.float_plus_infinity bool.the_value)
  (mode.
     binary_ieee.float_mul mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_minus_infinity bool.the_value)
  (mode.
     binary_ieee.float_mul mode
       (binary_ieee.float_plus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_plus_infinity bool.the_value)
  mode.
    binary_ieee.float_mul mode
      (binary_ieee.float_plus_infinity bool.the_value)
      (binary_ieee.float_minus_infinity bool.the_value) =
    binary_ieee.float_minus_infinity bool.the_value

(mode x.
     binary_ieee.float_sub mode (binary_ieee.float_some_nan bool.the_value)
       x = binary_ieee.float_some_nan bool.the_value)
  (mode x.
     binary_ieee.float_sub mode x
       (binary_ieee.float_some_nan bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_sub mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_minus_infinity bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  (mode.
     binary_ieee.float_sub mode
       (binary_ieee.float_minus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_minus_infinity bool.the_value)
  (mode.
     binary_ieee.float_sub mode
       (binary_ieee.float_plus_infinity bool.the_value)
       (binary_ieee.float_plus_infinity bool.the_value) =
     binary_ieee.float_some_nan bool.the_value)
  mode.
    binary_ieee.float_sub mode
      (binary_ieee.float_plus_infinity bool.the_value)
      (binary_ieee.float_minus_infinity bool.the_value) =
    binary_ieee.float_plus_infinity bool.the_value

x y.
    binary_ieee.float_compare x y =
    pair.pair_CASE (binary_ieee.float_value x, binary_ieee.float_value y)
      (λv v1.
         binary_ieee.float_value_CASE v
           (λr1.
              binary_ieee.float_value_CASE v1
                (λr2.
                   if Number.Real.< r1 r2 then binary_ieee.LT
                   else if r1 = r2 then binary_ieee.EQ
                   else binary_ieee.GT)
                (if binary_ieee.float_Sign y = words.n2w 1 then
                   binary_ieee.GT
                 else binary_ieee.LT) binary_ieee.UN)
           (binary_ieee.float_value_CASE v1
              (λv7.
                 if binary_ieee.float_Sign x = words.n2w 1 then
                   binary_ieee.LT
                 else binary_ieee.GT)
              (if binary_ieee.float_Sign x = binary_ieee.float_Sign y then
                 binary_ieee.EQ
               else if binary_ieee.float_Sign x = words.n2w 1 then
                 binary_ieee.LT
               else binary_ieee.GT) binary_ieee.UN) binary_ieee.UN)

mode x y.
    binary_ieee.float_add mode x y =
    pair.pair_CASE (binary_ieee.float_value x, binary_ieee.float_value y)
      (λv v1.
         binary_ieee.float_value_CASE v
           (λr1.
              binary_ieee.float_value_CASE v1
                (λr2.
                   binary_ieee.float_round mode
                     (if r1 = 0 r2 = 0
                         binary_ieee.float_Sign x =
                         binary_ieee.float_Sign y
                      then binary_ieee.float_Sign x = words.n2w 1
                      else mode = binary_ieee.roundTowardNegative)
                     (Number.Real.+ r1 r2)) y
                (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_value_CASE v1 (λv7. x)
              (if binary_ieee.float_Sign x = binary_ieee.float_Sign y then
                 x
               else binary_ieee.float_some_nan bool.the_value)
              (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_some_nan bool.the_value))

binary_ieee.float_value
    (binary_ieee.float_plus_infinity bool.the_value) =
  binary_ieee.Infinity
  binary_ieee.float_value
    (binary_ieee.float_minus_infinity bool.the_value) =
  binary_ieee.Infinity
  binary_ieee.float_value (binary_ieee.float_some_nan bool.the_value) =
  binary_ieee.NaN
  binary_ieee.float_value (binary_ieee.float_plus_zero bool.the_value) =
  binary_ieee.Float 0
  binary_ieee.float_value (binary_ieee.float_minus_zero bool.the_value) =
  binary_ieee.Float 0
  binary_ieee.float_value (binary_ieee.float_plus_min bool.the_value) =
  binary_ieee.Float
    (real./ (Number.Real.fromNatural (arithmetic.BIT2 0))
       (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
          (words.INT_MAX bool.the_value + fcp.dimindex bool.the_value)))
  binary_ieee.float_value (binary_ieee.float_minus_min bool.the_value) =
  binary_ieee.Float
    (real./ (Number.Real.~ (Number.Real.fromNatural (arithmetic.BIT2 0)))
       (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
          (words.INT_MAX bool.the_value + fcp.dimindex bool.the_value)))

mode x y.
    binary_ieee.float_sub mode x y =
    pair.pair_CASE (binary_ieee.float_value x, binary_ieee.float_value y)
      (λv v1.
         binary_ieee.float_value_CASE v
           (λr1.
              binary_ieee.float_value_CASE v1
                (λr2.
                   binary_ieee.float_round mode
                     (if r1 = 0 r2 = 0
                         ¬(binary_ieee.float_Sign x =
                            binary_ieee.float_Sign y)
                      then binary_ieee.float_Sign x = words.n2w 1
                      else mode = binary_ieee.roundTowardNegative)
                     (Number.Real.- r1 r2)) (binary_ieee.float_negate y)
                (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_value_CASE v1 (λv7. x)
              (if binary_ieee.float_Sign x = binary_ieee.float_Sign y then
                 binary_ieee.float_some_nan bool.the_value
               else x) (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_some_nan bool.the_value))

s e f.
    binary_ieee.float_to_real
      (binary_ieee.float_Sign_fupd (const s)
         (binary_ieee.float_Exponent_fupd (const e)
            (binary_ieee.float_Significand_fupd (const f) bool.ARB))) =
    bool.LET (λr. if s = words.n2w 1 then Number.Real.~ r else r)
      (if e = words.n2w 0 then
         Number.Real.*
           (real./ (Number.Real.fromNatural (arithmetic.BIT2 0))
              (Number.Real.fromNatural
                 (arithmetic.BIT2 0 words.INT_MAX bool.the_value)))
           (real./ (Number.Real.fromNatural (words.w2n f))
              (Number.Real.fromNatural (words.dimword bool.the_value)))
       else
         Number.Real.*
           (real./
              (Number.Real.fromNatural (arithmetic.BIT2 0 words.w2n e))
              (Number.Real.fromNatural
                 (arithmetic.BIT2 0 words.INT_MAX bool.the_value)))
           (Number.Real.+ 1
              (real./ (Number.Real.fromNatural (words.w2n f))
                 (Number.Real.fromNatural
                    (words.dimword bool.the_value)))))

x.
    binary_ieee.float_to_real x =
    if binary_ieee.float_Exponent x = words.n2w 0 then
      Number.Real.*
        (Number.Real.*
           (Number.Real.↑ (Number.Real.~ 1)
              (words.w2n (binary_ieee.float_Sign x)))
           (real./ (Number.Real.fromNatural (arithmetic.BIT2 0))
              (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
                 (words.INT_MAX bool.the_value))))
        (real./
           (Number.Real.fromNatural
              (words.w2n (binary_ieee.float_Significand x)))
           (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
              (fcp.dimindex bool.the_value)))
    else
      Number.Real.*
        (Number.Real.*
           (Number.Real.↑ (Number.Real.~ 1)
              (words.w2n (binary_ieee.float_Sign x)))
           (real./
              (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
                 (words.w2n (binary_ieee.float_Exponent x)))
              (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
                 (words.INT_MAX bool.the_value))))
        (Number.Real.+ 1
           (real./
              (Number.Real.fromNatural
                 (words.w2n (binary_ieee.float_Significand x)))
              (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0))
                 (fcp.dimindex bool.the_value))))

mode x y.
    binary_ieee.float_div mode x y =
    pair.pair_CASE (binary_ieee.float_value x, binary_ieee.float_value y)
      (λv v1.
         binary_ieee.float_value_CASE v
           (λr1.
              binary_ieee.float_value_CASE v1
                (λr2.
                   if r2 = 0 then
                     if r1 = 0 then
                       binary_ieee.float_some_nan bool.the_value
                     else if binary_ieee.float_Sign x =
                             binary_ieee.float_Sign y
                     then binary_ieee.float_plus_infinity bool.the_value
                     else binary_ieee.float_minus_infinity bool.the_value
                   else
                     binary_ieee.float_round mode
                       (¬(binary_ieee.float_Sign x =
                           binary_ieee.float_Sign y)) (real./ r1 r2))
                (if binary_ieee.float_Sign x = binary_ieee.float_Sign y
                 then binary_ieee.float_plus_zero bool.the_value
                 else binary_ieee.float_minus_zero bool.the_value)
                (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_value_CASE v1
              (λv7.
                 if binary_ieee.float_Sign x = binary_ieee.float_Sign y
                 then binary_ieee.float_plus_infinity bool.the_value
                 else binary_ieee.float_minus_infinity bool.the_value)
              (binary_ieee.float_some_nan bool.the_value)
              (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_some_nan bool.the_value))

mode x y.
    binary_ieee.float_mul mode x y =
    pair.pair_CASE (binary_ieee.float_value x, binary_ieee.float_value y)
      (λv v1.
         binary_ieee.float_value_CASE v
           (λr'.
              binary_ieee.float_value_CASE v1
                (λr2.
                   binary_ieee.float_round mode
                     (¬(binary_ieee.float_Sign x =
                         binary_ieee.float_Sign y)) (Number.Real.* r' r2))
                (if r' = 0 then binary_ieee.float_some_nan bool.the_value
                 else if binary_ieee.float_Sign x =
                         binary_ieee.float_Sign y
                 then binary_ieee.float_plus_infinity bool.the_value
                 else binary_ieee.float_minus_infinity bool.the_value)
                (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_value_CASE v1
              (λr.
                 if r = 0 then binary_ieee.float_some_nan bool.the_value
                 else if binary_ieee.float_Sign x =
                         binary_ieee.float_Sign y
                 then binary_ieee.float_plus_infinity bool.the_value
                 else binary_ieee.float_minus_infinity bool.the_value)
              (if binary_ieee.float_Sign x = binary_ieee.float_Sign y then
                 binary_ieee.float_plus_infinity bool.the_value
               else binary_ieee.float_minus_infinity bool.the_value)
              (binary_ieee.float_some_nan bool.the_value))
           (binary_ieee.float_some_nan bool.the_value))

y x r.
    binary_ieee.float_value y = binary_ieee.Float r
    (binary_ieee.float_Significand y = words.n2w 0
     ¬(binary_ieee.float_Exponent y = words.n2w 1)
     Number.Real.≤ (Number.Real.abs r) (Number.Real.abs x))
    Number.Real.≤
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs (Number.Real.- r x)))
      (binary_ieee.ULP (binary_ieee.float_Exponent y, bool.the_value))
    (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
       (Number.Real.abs (Number.Real.- r x)) =
     binary_ieee.ULP (binary_ieee.float_Exponent y, bool.the_value)
     ¬words.word_lsb (binary_ieee.float_Significand y))
    Number.Real.< (binary_ieee.ulp bool.the_value)
      (Number.Real.* (Number.Real.fromNatural (arithmetic.BIT2 0))
         (Number.Real.abs x))
    Number.Real.< (Number.Real.abs x)
      (binary_ieee.threshold bool.the_value)
    binary_ieee.round binary_ieee.roundTiesToEven x = y

¬binary_ieee.float_is_zero (binary_ieee.float_plus_min bool.the_value)
  binary_ieee.float_is_finite (binary_ieee.float_plus_min bool.the_value)
  (binary_ieee.float_is_integral
     (binary_ieee.float_plus_min bool.the_value)
   fcp.dimindex bool.the_value = 1 fcp.dimindex bool.the_value = 1)
  ¬binary_ieee.float_is_nan (binary_ieee.float_plus_min bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_plus_min bool.the_value)
  binary_ieee.float_is_subnormal
    (binary_ieee.float_plus_min bool.the_value)
  ¬binary_ieee.float_is_infinite
      (binary_ieee.float_plus_min bool.the_value)
  ¬binary_ieee.float_is_zero (binary_ieee.float_minus_min bool.the_value)
  binary_ieee.float_is_finite
    (binary_ieee.float_minus_min bool.the_value)
  (binary_ieee.float_is_integral
     (binary_ieee.float_minus_min bool.the_value)
   fcp.dimindex bool.the_value = 1 fcp.dimindex bool.the_value = 1)
  ¬binary_ieee.float_is_nan (binary_ieee.float_minus_min bool.the_value)
  ¬binary_ieee.float_is_normal
      (binary_ieee.float_minus_min bool.the_value)
  binary_ieee.float_is_subnormal
    (binary_ieee.float_minus_min bool.the_value)
  ¬binary_ieee.float_is_infinite
      (binary_ieee.float_minus_min bool.the_value)

((g f0.
      binary_ieee.float_Sign_fupd f0 binary_ieee.float_Sign_fupd g =
      binary_ieee.float_Sign_fupd (f0 g))
   h g f0.
     binary_ieee.float_Sign_fupd f0 (binary_ieee.float_Sign_fupd g h) =
     binary_ieee.float_Sign_fupd (f0 g) h)
  ((g f0.
      binary_ieee.float_Exponent_fupd f0
      binary_ieee.float_Exponent_fupd g =
      binary_ieee.float_Exponent_fupd (f0 g))
   h g f0.
     binary_ieee.float_Exponent_fupd f0
     (binary_ieee.float_Exponent_fupd g h) =
     binary_ieee.float_Exponent_fupd (f0 g) h)
  (g f0.
     binary_ieee.float_Significand_fupd f0
     binary_ieee.float_Significand_fupd g =
     binary_ieee.float_Significand_fupd (f0 g))
  h g f0.
    binary_ieee.float_Significand_fupd f0
    (binary_ieee.float_Significand_fupd g h) =
    binary_ieee.float_Significand_fupd (f0 g) h

(f0 f.
     binary_ieee.float_Sign (binary_ieee.float_Exponent_fupd f0 f) =
     binary_ieee.float_Sign f)
  (f0 f.
     binary_ieee.float_Sign (binary_ieee.float_Significand_fupd f0 f) =
     binary_ieee.float_Sign f)
  (f0 f.
     binary_ieee.float_Exponent (binary_ieee.float_Sign_fupd f0 f) =
     binary_ieee.float_Exponent f)
  (f0 f.
     binary_ieee.float_Exponent (binary_ieee.float_Significand_fupd f0 f) =
     binary_ieee.float_Exponent f)
  (f0 f.
     binary_ieee.float_Significand (binary_ieee.float_Sign_fupd f0 f) =
     binary_ieee.float_Significand f)
  (f0 f.
     binary_ieee.float_Significand (binary_ieee.float_Exponent_fupd f0 f) =
     binary_ieee.float_Significand f)
  (f0 f.
     binary_ieee.float_Sign (binary_ieee.float_Sign_fupd f0 f) =
     f0 (binary_ieee.float_Sign f))
  (f0 f.
     binary_ieee.float_Exponent (binary_ieee.float_Exponent_fupd f0 f) =
     f0 (binary_ieee.float_Exponent f))
  f0 f.
    binary_ieee.float_Significand
      (binary_ieee.float_Significand_fupd f0 f) =
    f0 (binary_ieee.float_Significand f)

((g f0.
      binary_ieee.float_Exponent_fupd f0 binary_ieee.float_Sign_fupd g =
      binary_ieee.float_Sign_fupd g binary_ieee.float_Exponent_fupd f0)
   h g f0.
     binary_ieee.float_Exponent_fupd f0
     (binary_ieee.float_Sign_fupd g h) =
     binary_ieee.float_Sign_fupd g
     (binary_ieee.float_Exponent_fupd f0 h))
  ((g f0.
      binary_ieee.float_Significand_fupd f0
      binary_ieee.float_Sign_fupd g =
      binary_ieee.float_Sign_fupd g
      binary_ieee.float_Significand_fupd f0)
   h g f0.
     binary_ieee.float_Significand_fupd f0
     (binary_ieee.float_Sign_fupd g h) =
     binary_ieee.float_Sign_fupd g
     (binary_ieee.float_Significand_fupd f0 h))
  (g f0.
     binary_ieee.float_Significand_fupd f0
     binary_ieee.float_Exponent_fupd g =
     binary_ieee.float_Exponent_fupd g
     binary_ieee.float_Significand_fupd f0)
  h g f0.
    binary_ieee.float_Significand_fupd f0
    (binary_ieee.float_Exponent_fupd g h) =
    binary_ieee.float_Exponent_fupd g
    (binary_ieee.float_Significand_fupd f0 h)

mode x.
    binary_ieee.round mode x =
    binary_ieee.rounding_CASE mode
      (bool.LET
         (λt.
            if Number.Real.≤ x (Number.Real.~ t) then
              binary_ieee.float_minus_infinity bool.the_value
            else if Number.Real.≥ x t then
              binary_ieee.float_plus_infinity bool.the_value
            else
              binary_ieee.closest_such
                (λa. ¬words.word_lsb (binary_ieee.float_Significand a))
                binary_ieee.float_is_finite x)
         (binary_ieee.threshold bool.the_value))
      (bool.LET
         (λt.
            if Number.Real.< x (Number.Real.~ t) then
              binary_ieee.float_bottom bool.the_value
            else if Number.Real.> x t then
              binary_ieee.float_plus_infinity bool.the_value
            else
              binary_ieee.closest
                (pred_set.GSPEC
                   (λa.
                      (a,
                       binary_ieee.float_is_finite a
                       Number.Real.≥ (binary_ieee.float_to_real a) x))) x)
         (binary_ieee.largest bool.the_value))
      (bool.LET
         (λt.
            if Number.Real.< x (Number.Real.~ t) then
              binary_ieee.float_minus_infinity bool.the_value
            else if Number.Real.> x t then
              binary_ieee.float_top bool.the_value
            else
              binary_ieee.closest
                (pred_set.GSPEC
                   (λa.
                      (a,
                       binary_ieee.float_is_finite a
                       Number.Real.≤ (binary_ieee.float_to_real a) x))) x)
         (binary_ieee.largest bool.the_value))
      (bool.LET
         (λt.
            if Number.Real.< x (Number.Real.~ t) then
              binary_ieee.float_bottom bool.the_value
            else if Number.Real.> x t then
              binary_ieee.float_top bool.the_value
            else
              binary_ieee.closest
                (pred_set.GSPEC
                   (λa.
                      (a,
                       binary_ieee.float_is_finite a
                       Number.Real.≤
                         (Number.Real.abs (binary_ieee.float_to_real a))
                         (Number.Real.abs x)))) x)
         (binary_ieee.largest bool.the_value))

mode x.
    binary_ieee.integral_round mode x =
    binary_ieee.rounding_CASE mode
      (bool.LET
         (λt.
            if Number.Real.≤ x (Number.Real.~ t) then
              binary_ieee.float_minus_infinity bool.the_value
            else if Number.Real.≥ x t then
              binary_ieee.float_plus_infinity bool.the_value
            else
              binary_ieee.closest_such
                (λa.
                   n.
                     even n
                     Number.Real.abs (binary_ieee.float_to_real a) =
                     Number.Real.fromNatural n)
                binary_ieee.float_is_integral x)
         (binary_ieee.threshold bool.the_value))
      (bool.LET
         (λt.
            if Number.Real.< x (Number.Real.~ t) then
              binary_ieee.float_bottom bool.the_value
            else if Number.Real.> x t then
              binary_ieee.float_plus_infinity bool.the_value
            else
              binary_ieee.closest
                (pred_set.GSPEC
                   (λa.
                      (a,
                       binary_ieee.float_is_integral a
                       Number.Real.≥ (binary_ieee.float_to_real a) x))) x)
         (binary_ieee.largest bool.the_value))
      (bool.LET
         (λt.
            if Number.Real.< x (Number.Real.~ t) then
              binary_ieee.float_minus_infinity bool.the_value
            else if Number.Real.> x t then
              binary_ieee.float_top bool.the_value
            else
              binary_ieee.closest
                (pred_set.GSPEC
                   (λa.
                      (a,
                       binary_ieee.float_is_integral a
                       Number.Real.≤ (binary_ieee.float_to_real a) x))) x)
         (binary_ieee.largest bool.the_value))
      (bool.LET
         (λt.
            if Number.Real.< x (Number.Real.~ t) then
              binary_ieee.float_bottom bool.the_value
            else if Number.Real.> x t then
              binary_ieee.float_top bool.the_value
            else
              binary_ieee.closest
                (pred_set.GSPEC
                   (λa.
                      (a,
                       binary_ieee.float_is_integral a
                       Number.Real.≤
                         (Number.Real.abs (binary_ieee.float_to_real a))
                         (Number.Real.abs x)))) x)
         (binary_ieee.largest bool.the_value))

mode x y z.
    binary_ieee.float_mul_sub mode x y z =
    bool.LET
      (λsignP.
         bool.LET
           (λinfP.
              if binary_ieee.float_is_nan x binary_ieee.float_is_nan y
                 binary_ieee.float_is_nan z
                 binary_ieee.float_is_infinite x
                 binary_ieee.float_is_zero y
                 binary_ieee.float_is_zero x
                 binary_ieee.float_is_infinite y
                 binary_ieee.float_is_infinite z infP
                 binary_ieee.float_Sign z = signP
              then binary_ieee.float_some_nan bool.the_value
              else if binary_ieee.float_is_infinite z
                      binary_ieee.float_Sign z = words.n2w 1
                      infP signP = words.n2w 0
              then binary_ieee.float_plus_infinity bool.the_value
              else if binary_ieee.float_is_infinite z
                      binary_ieee.float_Sign z = words.n2w 0
                      infP signP = words.n2w 1
              then binary_ieee.float_minus_infinity bool.the_value
              else if binary_ieee.float_is_zero z
                      (binary_ieee.float_is_zero x
                       binary_ieee.float_is_zero y)
                      ¬(binary_ieee.float_Sign x = signP)
              then
                if binary_ieee.float_Sign x = words.n2w 0 then
                  binary_ieee.float_minus_zero bool.the_value
                else binary_ieee.float_plus_zero bool.the_value
              else
                binary_ieee.real_to_float mode
                  (Number.Real.-
                     (Number.Real.* (binary_ieee.float_to_real x)
                        (binary_ieee.float_to_real y))
                     (binary_ieee.float_to_real z)))
           (binary_ieee.float_is_infinite x
            binary_ieee.float_is_infinite y))
      (words.word_xor (binary_ieee.float_Sign x)
         (binary_ieee.float_Sign y))

mode x y z.
    binary_ieee.float_mul_add mode x y z =
    bool.LET
      (λsignP.
         bool.LET
           (λinfP.
              if binary_ieee.float_is_nan x binary_ieee.float_is_nan y
                 binary_ieee.float_is_nan z
                 binary_ieee.float_is_infinite x
                 binary_ieee.float_is_zero y
                 binary_ieee.float_is_zero x
                 binary_ieee.float_is_infinite y
                 binary_ieee.float_is_infinite z infP
                 ¬(binary_ieee.float_Sign z = signP)
              then binary_ieee.float_some_nan bool.the_value
              else if binary_ieee.float_is_infinite z
                      binary_ieee.float_Sign z = words.n2w 0
                      infP signP = words.n2w 0
              then binary_ieee.float_plus_infinity bool.the_value
              else if binary_ieee.float_is_infinite z
                      binary_ieee.float_Sign z = words.n2w 1
                      infP signP = words.n2w 1
              then binary_ieee.float_minus_infinity bool.the_value
              else if binary_ieee.float_is_zero z
                      (binary_ieee.float_is_zero x
                       binary_ieee.float_is_zero y)
                      binary_ieee.float_Sign x = signP
              then
                if binary_ieee.float_Sign x = words.n2w 1 then
                  binary_ieee.float_minus_zero bool.the_value
                else binary_ieee.float_plus_zero bool.the_value
              else
                binary_ieee.real_to_float mode
                  (Number.Real.+
                     (Number.Real.* (binary_ieee.float_to_real x)
                        (binary_ieee.float_to_real y))
                     (binary_ieee.float_to_real z)))
           (binary_ieee.float_is_infinite x
            binary_ieee.float_is_infinite y))
      (words.word_xor (binary_ieee.float_Sign x)
         (binary_ieee.float_Sign y))

(s e f.
     binary_ieee.float_is_nan
       (binary_ieee.float_Sign_fupd (const s)
          (binary_ieee.float_Exponent_fupd (const e)
             (binary_ieee.float_Significand_fupd (const f) bool.ARB)))
     e = words.word_2comp (words.n2w 1) ¬(f = words.n2w 0))
  (s e f.
     binary_ieee.float_is_infinite
       (binary_ieee.float_Sign_fupd (const s)
          (binary_ieee.float_Exponent_fupd (const e)
             (binary_ieee.float_Significand_fupd (const f) bool.ARB)))
     e = words.word_2comp (words.n2w 1) f = words.n2w 0)
  (s e f.
     binary_ieee.float_is_normal
       (binary_ieee.float_Sign_fupd (const s)
          (binary_ieee.float_Exponent_fupd (const e)
             (binary_ieee.float_Significand_fupd (const f) bool.ARB)))
     ¬(e = words.n2w 0) ¬(e = words.word_2comp (words.n2w 1)))
  (s e f.
     binary_ieee.float_is_subnormal
       (binary_ieee.float_Sign_fupd (const s)
          (binary_ieee.float_Exponent_fupd (const e)
             (binary_ieee.float_Significand_fupd (const f) bool.ARB)))
     e = words.n2w 0 ¬(f = words.n2w 0))
  (s e f.
     binary_ieee.float_is_zero
       (binary_ieee.float_Sign_fupd (const s)
          (binary_ieee.float_Exponent_fupd (const e)
             (binary_ieee.float_Significand_fupd (const f) bool.ARB)))
     e = words.n2w 0 f = words.n2w 0)
  s e f.
    binary_ieee.float_is_finite
      (binary_ieee.float_Sign_fupd (const s)
         (binary_ieee.float_Exponent_fupd (const e)
            (binary_ieee.float_Significand_fupd (const f) bool.ARB)))
    ¬(e = words.word_2comp (words.n2w 1))

binary_ieee.float_Sign (binary_ieee.float_plus_infinity bool.the_value) =
  words.n2w 0
  binary_ieee.float_Exponent
    (binary_ieee.float_plus_infinity bool.the_value) = words.word_T
  binary_ieee.float_Significand
    (binary_ieee.float_plus_infinity bool.the_value) = words.n2w 0
  binary_ieee.float_Sign
    (binary_ieee.float_minus_infinity bool.the_value) = words.n2w 1
  binary_ieee.float_Exponent
    (binary_ieee.float_minus_infinity bool.the_value) = words.word_T
  binary_ieee.float_Significand
    (binary_ieee.float_minus_infinity bool.the_value) = words.n2w 0
  binary_ieee.float_Sign (binary_ieee.float_plus_zero bool.the_value) =
  words.n2w 0
  binary_ieee.float_Exponent (binary_ieee.float_plus_zero bool.the_value) =
  words.n2w 0
  binary_ieee.float_Significand
    (binary_ieee.float_plus_zero bool.the_value) = words.n2w 0
  binary_ieee.float_Sign (binary_ieee.float_minus_zero bool.the_value) =
  words.n2w 1
  binary_ieee.float_Exponent
    (binary_ieee.float_minus_zero bool.the_value) = words.n2w 0
  binary_ieee.float_Significand
    (binary_ieee.float_minus_zero bool.the_value) = words.n2w 0
  binary_ieee.float_Sign (binary_ieee.float_plus_min bool.the_value) =
  words.n2w 0
  binary_ieee.float_Exponent (binary_ieee.float_plus_min bool.the_value) =
  words.n2w 0
  binary_ieee.float_Significand
    (binary_ieee.float_plus_min bool.the_value) = words.n2w 1
  binary_ieee.float_Sign (binary_ieee.float_minus_min bool.the_value) =
  words.n2w 1
  binary_ieee.float_Exponent (binary_ieee.float_minus_min bool.the_value) =
  words.n2w 0
  binary_ieee.float_Significand
    (binary_ieee.float_minus_min bool.the_value) = words.n2w 1
  binary_ieee.float_Sign (binary_ieee.float_top bool.the_value) =
  words.n2w 0
  binary_ieee.float_Exponent (binary_ieee.float_top bool.the_value) =
  words.word_sub words.word_T (words.n2w 1)
  binary_ieee.float_Significand (binary_ieee.float_top bool.the_value) =
  words.word_T
  binary_ieee.float_Sign (binary_ieee.float_bottom bool.the_value) =
  words.n2w 1
  binary_ieee.float_Exponent (binary_ieee.float_bottom bool.the_value) =
  words.word_sub words.word_T (words.n2w 1)
  binary_ieee.float_Significand (binary_ieee.float_bottom bool.the_value) =
  words.word_T
  binary_ieee.float_Exponent (binary_ieee.float_some_nan bool.the_value) =
  words.word_T
  ¬(binary_ieee.float_Significand
       (binary_ieee.float_some_nan bool.the_value) = words.n2w 0)
  (x.
     binary_ieee.float_Sign (binary_ieee.float_negate x) =
     words.word_1comp (binary_ieee.float_Sign x))
  (x.
     binary_ieee.float_Exponent (binary_ieee.float_negate x) =
     binary_ieee.float_Exponent x)
  x.
    binary_ieee.float_Significand (binary_ieee.float_negate x) =
    binary_ieee.float_Significand x

¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_minus_infinity bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_plus_zero bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_minus_zero bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_top bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_bottom bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_plus_min bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_minus_min bool.the_value)
  ¬(binary_ieee.float_plus_infinity bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_plus_zero bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_minus_zero bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_top bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_bottom bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_plus_min bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_minus_min bool.the_value)
  ¬(binary_ieee.float_minus_infinity bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_plus_zero bool.the_value =
     binary_ieee.float_minus_zero bool.the_value)
  ¬(binary_ieee.float_plus_zero bool.the_value =
     binary_ieee.float_top bool.the_value)
  ¬(binary_ieee.float_plus_zero bool.the_value =
     binary_ieee.float_bottom bool.the_value)
  ¬(binary_ieee.float_plus_zero bool.the_value =
     binary_ieee.float_plus_min bool.the_value)
  ¬(binary_ieee.float_plus_zero bool.the_value =
     binary_ieee.float_minus_min bool.the_value)
  ¬(binary_ieee.float_plus_zero bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_minus_zero bool.the_value =
     binary_ieee.float_top bool.the_value)
  ¬(binary_ieee.float_minus_zero bool.the_value =
     binary_ieee.float_bottom bool.the_value)
  ¬(binary_ieee.float_minus_zero bool.the_value =
     binary_ieee.float_plus_min bool.the_value)
  ¬(binary_ieee.float_minus_zero bool.the_value =
     binary_ieee.float_minus_min bool.the_value)
  ¬(binary_ieee.float_minus_zero bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_top bool.the_value =
     binary_ieee.float_minus_min bool.the_value)
  ¬(binary_ieee.float_top bool.the_value =
     binary_ieee.float_bottom bool.the_value)
  ¬(binary_ieee.float_top bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_bottom bool.the_value =
     binary_ieee.float_plus_min bool.the_value)
  ¬(binary_ieee.float_bottom bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_plus_min bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  ¬(binary_ieee.float_plus_min bool.the_value =
     binary_ieee.float_minus_min bool.the_value)
  ¬(binary_ieee.float_minus_min bool.the_value =
     binary_ieee.float_some_nan bool.the_value)
  x. ¬(binary_ieee.float_negate x = x)

External Type Operators

External Constants

Assumptions

pred_set.FINITE pred_set.UNIV

wellFounded empty

0 = 0

0 < fcp.dimindex bool.the_value

0 < words.dimword bool.the_value

x. x = x

t. t

n. 0 n

m. m m

x. Number.Real.≤ x x

q. q

words.word_lsb (words.word_2comp (words.n2w 1))

words.word_T = words.n2w (words.UINT_MAX bool.the_value)

pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV

fcp.dimindex bool.the_value = 1

words.dimword bool.the_value = arithmetic.BIT2 0

1 < words.dimword bool.the_value

1 fcp.dimindex bool.the_value

arithmetic.DIV2 (bit1 x) = x

words.w2n (words.n2w 0) = 0

words.word_1comp (words.n2w 0) = words.word_T

¬¬p p

x. ¬bool.IN x pred_set.EMPTY

x. id x = x

t. t ¬t

x. marker.Abbrev x x

n. ¬(n < n)

n. 0 < suc n

x. ¬Number.Real.< x x

w. words.word_ls (words.n2w 0) w

(¬) = λt. t

() = λP. P ((select) P)

a. x. x = a

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

Number.Real.abs 0 = 0

words.word_2comp (words.n2w 1) = words.word_T

¬(p q) p

x. x = x

n. ¬(suc n = 0)

n. Number.Real.≤ 0 (Number.Real.fromNatural n)

c. arithmetic.- c c = 0

n. min n n = n

x. Number.Real.≤ 0 (Number.Real.abs x)

x. Number.Real.~ (Number.Real.~ x) = x

w. words.w2n w < words.dimword bool.the_value

a. words.word_1comp (words.word_1comp a) = a

pred_set.GSPEC (λx. (x, )) = pred_set.EMPTY

e. f. f bool.the_value = e

words.w2n (words.n2w 1) = 1

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

t. (t ) ¬t

n. 0 < arithmetic.BIT2 0 n

x. numeral.iDUB x = x + x

n. words.word_lsb (words.n2w n) odd n

n.
    Number.Real.abs (Number.Real.fromNatural n) = Number.Real.fromNatural n

m. m * 1 = m

q. q div 1 = q

k. k mod 1 = 0

x. Number.Real.abs (Number.Real.~ x) = Number.Real.abs x

x. Number.Real.- x x = 0

x. Number.Real.+ x 0 = x

x. Number.Real.- x 0 = x

x. Number.Real.↑ x 1 = x

x. Number.Real.+ 0 x = x

x y. const x y = x

P. P bool.the_value ii. P ii

¬(words.word_2comp (words.n2w 1) = words.n2w 0)

() = λp q. p q p

fcp.dimindex bool.the_value = arithmetic.BIT2 7

words.dimword bool.the_value =
  arithmetic.BIT2 0 fcp.dimindex bool.the_value

words.INT_MAX bool.the_value =
  arithmetic.- (words.INT_MIN bool.the_value) 1

words.UINT_MAX bool.the_value =
  arithmetic.- (words.dimword bool.the_value) 1

t. t t

t. (t ) (t )

m. prim_rec.PRE m = arithmetic.- m 1

m. suc m = m + 1

n. suc n = 1 + n

n. 1 arithmetic.BIT2 0 n

a. arithmetic.- (suc a) a = 1

x. Number.Real.* x 0 = 0

x. Number.Real.+ x (Number.Real.~ x) = 0

x. real./ 0 x = 0

x. Number.Real.* 0 x = 0

x. Number.Real.+ (Number.Real.~ x) x = 0

x. Number.Real.- 0 x = Number.Real.~ x

x. Number.Real.* x 1 = x

x. Number.Real.* 1 x = x

x y. fst (x, y) = x

x y. snd (x, y) = y

b t. (if b then t else t) = t

f x. bool.LET f x = f x

P x. P x P ((select) P)

P x. bool.IN x P P x

fcp.dimindex bool.the_value = arithmetic.BIT2 15

pair.pair_CASE (x, y) f = f x y

n. words.w2n (words.n2w n) = n mod words.dimword bool.the_value

n. arithmetic.BIT2 0 * n = n + n

x. realax.inv x = real./ 1 x

x. q r. x = (q, r)

x y. x = y y = x

A B. A B B A

m n. m * n = n * m

m n. m + n = n + m

x y. Number.Real.> x y Number.Real.< y x

x y. Number.Real.≥ x y Number.Real.≤ y x

x y. Number.Real.* x y = Number.Real.* y x

x y. Number.Real.+ x y = Number.Real.+ y x

x y. Number.Real.< x y Number.Real.≤ x y

x y. Number.Real.≤ x y Number.Real.≤ y x

v w. words.word_add v w = words.word_add w v

v w. words.word_mul v w = words.word_mul w v

a b. words.word_or a b = words.word_or b a

fcp.dimindex bool.the_value = arithmetic.BIT2 31

(¬A ) (A )

words.word_2comp v = words.n2w 0 v = words.n2w 0

n. 0 < n 0 mod n = 0

n.
    Number.Real.≤ 1
      (Number.Real.↑ (Number.Real.fromNatural (arithmetic.BIT2 0)) n)

x. Number.Real.~ x = Number.Real.* (Number.Real.~ 1) x

x. Number.Real.abs x = x Number.Real.≤ 0 x

w.
    words.word_2comp w = words.word_mul (words.word_2comp (words.n2w 1)) w

w. words.w2n w = 0 w = words.n2w 0

A B. A B ¬A B

m n. m < n suc m n

m n. m < n ¬(m = n)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m. m = 0 n. m = suc n

y x. Number.Real.< x y ¬Number.Real.≤ y x

x y. Number.Real.- x y = Number.Real.+ x (Number.Real.~ y)

x y. Number.Real.< x y ¬(x = y)

v w. words.word_sub v w = words.word_add v (words.word_2comp w)

a b. ¬words.word_lo a b words.word_ls b a

v w. words.word_concat v w = words.w2w (words.word_join v w)

() = λp q. (λf. f p q) = λf. f

words.INT_MIN bool.the_value =
  arithmetic.BIT2 0 arithmetic.- (fcp.dimindex bool.the_value) 1

words.w2n (words.word_2comp (words.n2w 1)) =
  arithmetic.- (words.dimword bool.the_value) 1

n.
    Number.Real.fromNatural (suc n) =
    Number.Real.+ (Number.Real.fromNatural n) 1

n. words.n2w (suc n) = words.word_add (words.n2w n) (words.n2w 1)

x. Number.Real.< 0 x ¬(x = 0)

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

h l. words.word_extract h l = words.w2w words.word_bits h l

n k. k < n k mod n = k

m n. ¬(m n) suc n m

x n.
    Number.Real.↑ (Number.Real.fromNatural x) n =
    Number.Real.fromNatural (x n)

m n. Number.Real.fromNatural m = Number.Real.fromNatural n m = n

m n.
    Number.Real.≤ (Number.Real.fromNatural m) (Number.Real.fromNatural n)
    m n

m n. arithmetic.- m n = 0 m n

m n. m + n = m n = 0

x y.
    Number.Real.abs (Number.Real.- x y) =
    Number.Real.abs (Number.Real.- y x)

x y.
    Number.Real.* x (Number.Real.~ y) = Number.Real.~ (Number.Real.* x y)

x y.
    Number.Real.* (Number.Real.~ x) y = Number.Real.~ (Number.Real.* x y)

x y.
    Number.Real.≤ (Number.Real.~ x) (Number.Real.~ y) Number.Real.≤ y x

a b. words.word_lo a b words.w2n a < words.w2n b

a b. words.word_ls a b words.w2n a words.w2n b

v w. words.w2n v = words.w2n w v = w

v w. words.word_2comp v = words.word_2comp w v = w

w. n. w = words.n2w n n < words.dimword bool.the_value

m. arithmetic.- 0 m = 0 arithmetic.- m 0 = m

n. min n 0 = 0 min 0 n = 0

x. Number.Real.abs x = if Number.Real.≤ 0 x then x else Number.Real.~ x

f g x. (f g) x = f (g x)

w.
    words.w2w w =
    words.word_extract (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 w

x n. bit.MOD_2EXP x n = n mod arithmetic.BIT2 0 x

m n.
    Number.Real.* (Number.Real.fromNatural m) (Number.Real.fromNatural n) =
    Number.Real.fromNatural (m * n)

m n.
    Number.Real.+ (Number.Real.fromNatural m) (Number.Real.fromNatural n) =
    Number.Real.fromNatural (m + n)

m n. words.word_add (words.n2w m) (words.n2w n) = words.n2w (m + n)

x y.
    Number.Real.~ (Number.Real.+ x y) =
    Number.Real.+ (Number.Real.~ x) (Number.Real.~ y)

x y.
    Number.Real.abs (Number.Real.* x y) =
    Number.Real.* (Number.Real.abs x) (Number.Real.abs y)

x y. Number.Real.< 0 (Number.Real.- x y) Number.Real.< y x

x y. Number.Real.≤ 0 (Number.Real.- x y) Number.Real.≤ y x

w v. words.word_sub v w = words.n2w 0 v = w

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV then
    arithmetic.BIT2 0 * fcp.dimindex bool.the_value
  else 1

h l w. words.word_bits h l w = words.word_extract h l w

m n. n < m p. p + n = m

m n. m n p. n = m + p

n.
    words.word_2comp (words.n2w n) =
    words.n2w
      (arithmetic.- (words.dimword bool.the_value)
         (n mod words.dimword bool.the_value))

i. i < fcp.dimindex bool.the_value fcp.fcp_index (fcp.FCP g) i = g i

f g. f = g x. f x = g x

f v. (x. x = v f x) f v

P a. (x. x = a P x) P a

P t. (x. x = t P x) () P

f x y. pair.UNCURRY f (x, y) = f x y

() = λt1 t2. t. (t1 t) (t2 t) t

(odd 0 ) n. odd (suc n) ¬odd n

t1 t2. (t1 t2) (t2 t1) (t1 t2)

m n. m = n m n n m

m n. m = n m < n n < m

n x. Number.Real.↑ x n = 0 x = 0

x n. Number.Real.< 0 x Number.Real.< 0 (Number.Real.↑ x n)

x y.
    Number.Real.≤ x (Number.Real.~ y) Number.Real.≤ (Number.Real.+ x y) 0

x y.
    Number.Real.≤ (Number.Real.~ x) y Number.Real.≤ 0 (Number.Real.+ x y)

x y. Number.Real.≤ x y Number.Real.≤ y x x = y

(p ¬q) (p q) (¬q ¬p)

¬(¬A B) A ¬B

x. ¬(x = 0) real./ x x = 1

P Q. (x. P x Q) (x. P x) Q

¬(A B) (A ) ¬B

(x, y) = (a, b) x = a y = b

t1 t2 t3. t1 t2 t3 (t1 t2) t3

t1 t2 t3. t1 t2 t3 t1 t2 t3

A B C. A B C (A B) C

m n p. m < arithmetic.- n p m + p < n

m n p. arithmetic.- m n p m n + p

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. m + p = n + p m = n

m n p. m + p < n + p m < n

m n p. m + n m + p n p

m n p. m n n p m p

h l w. h < l words.word_extract h l w = words.n2w 0

n. 1 n = 1 n 1 = n

x y z.
    Number.Real.≤ y z
    Number.Real.≤ (Number.Real.+ x y) (Number.Real.+ x z)

x y z.
    Number.Real.< x (Number.Real.- y z)
    Number.Real.< (Number.Real.+ x z) y

x y z.
    Number.Real.≤ x (Number.Real.- y z)
    Number.Real.≤ (Number.Real.+ x z) y

x y z. Number.Real.- x y = z x = Number.Real.+ z y

x y z.
    Number.Real.< (Number.Real.+ x y) z
    Number.Real.< x (Number.Real.- z y)

x y z.
    Number.Real.* x (Number.Real.* y z) =
    Number.Real.* (Number.Real.* x y) z

x y z.
    Number.Real.+ x (Number.Real.+ y z) =
    Number.Real.+ (Number.Real.+ x y) z

x y z. Number.Real.+ x y = Number.Real.+ x z y = z

x y z.
    Number.Real.< (Number.Real.+ x y) (Number.Real.+ x z)
    Number.Real.< y z

x y z.
    Number.Real.≤ (Number.Real.- x z) (Number.Real.- y z)
    Number.Real.≤ x y

x y z. Number.Real.< x y Number.Real.< y z Number.Real.< x z

x y z. Number.Real.< x y Number.Real.≤ y z Number.Real.< x z

x y z. Number.Real.≤ x y Number.Real.< y z Number.Real.< x z

x y z. Number.Real.≤ x y Number.Real.≤ y z Number.Real.≤ x z

x. ¬(x = 0) Number.Real.* (realax.inv x) x = 1

f g h. f (g h) = f g h

v w x.
    words.word_add v (words.word_add w x) =
    words.word_add (words.word_add v w) x

v w x.
    words.word_mul v (words.word_mul w x) =
    words.word_mul (words.word_mul v w) x

a b c.
    words.word_or (words.word_or a b) c =
    words.word_or a (words.word_or b c)

v w x. words.word_add v w = words.word_add v x w = x

v w x. words.word_add v w = words.word_add x w v = x

v w.
    words.word_or v w = fcp.FCP (λi. fcp.fcp_index v i fcp.fcp_index w i)

f v. bool.IN v (pred_set.GSPEC f) x. (v, ) = f x

t1 t2. (if then t1 else t2) = t1 (if then t1 else t2) = t2

t1 t2. (t1 t2) t1 t2 ¬t1 ¬t2

n m. arithmetic.- n m = if m < n then numeral.iSUB n m else 0

m n. 0 < n (m = prim_rec.PRE n suc m = n)

x y. 0 < y (x mod y = x x < y)

m n. m * n = 0 m = 0 n = 0

m n. m + n = 0 m = 0 n = 0

n m. n m = 0 n = 0 0 < m

x y. ¬(y = 0) Number.Real.* (real./ x y) y = x

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV then
    arithmetic.BIT2 0 * fcp.dimindex bool.the_value + 1
  else 1

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV then
    fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
  else 1

(w. words.word_add w (words.n2w 0) = w)
  w. words.word_add (words.n2w 0) w = w

x y s. pred_set.INSERT y s x x = y bool.IN x s

m n. n < m p. m = n + (p + 1)

n.
    words.word_1comp (words.n2w n) =
    words.n2w
      (arithmetic.- (arithmetic.- (words.dimword bool.the_value) 1)
         (n mod words.dimword bool.the_value))

P. P 0 (n. P n P (suc n)) n. P n

(t. ¬¬t t) (¬ ) (¬ )

m n. ¬(m = n) suc m n suc n m

w h.
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    words.word_bits h 0 w = w

x y.
    words.word_ls y x
    words.w2n (words.word_sub x y) =
    arithmetic.- (words.w2n x) (words.w2n y)

x y s. bool.IN x (pred_set.INSERT y s) x = y bool.IN x s

A B C. A B C (A B) (A C)

P Q R. P Q R (P R) (Q R)

A B C. B C A (B A) (C A)

m n p. m n suc p * m suc p * n

m n p. p * (m + n) = p * m + p * n

p q n. n (p + q) = n p * n q

m n p. (m + n) * p = m * p + n * p

n. 0 < n n div n = 1 n mod n = 0

c m n.
    Number.Real.↑ c (m + n) =
    Number.Real.* (Number.Real.↑ c m) (Number.Real.↑ c n)

x y z.
    Number.Real.* x (Number.Real.+ y z) =
    Number.Real.+ (Number.Real.* x y) (Number.Real.* x z)

x y z.
    Number.Real.* x (Number.Real.- y z) =
    Number.Real.- (Number.Real.* x y) (Number.Real.* x z)

x y z.
    Number.Real.* (Number.Real.+ x y) z =
    Number.Real.+ (Number.Real.* x z) (Number.Real.* y z)

x y z.
    Number.Real.* (Number.Real.- x y) z =
    Number.Real.- (Number.Real.* x z) (Number.Real.* y z)

x y z.
    Number.Real.+ (real./ y x) (real./ z x) = real./ (Number.Real.+ y z) x

v w x.
    words.word_mul v (words.word_add w x) =
    words.word_add (words.word_mul v w) (words.word_mul v x)

v w x.
    words.word_mul (words.word_add v w) x =
    words.word_add (words.word_mul v x) (words.word_mul w x)

n a.
    bit.MOD_2EXP_MAX n a
    bit.MOD_2EXP n a = arithmetic.- (arithmetic.BIT2 0 n) 1

m n.
    words.n2w m = words.n2w n
    m mod words.dimword bool.the_value = n mod words.dimword bool.the_value

a b.
    words.word_ls (words.n2w a) (words.n2w b)
    a mod words.dimword bool.the_value b mod words.dimword bool.the_value

n m. n m = 1 n = 1 m = 0

P Q. (x. P x) (x. P x Q x) Q ((select) P)

y z.
    Number.Real.< 0 z (Number.Real.< 0 (real./ y z) Number.Real.< 0 y)

x y.
    Number.Real.< 0 y
    (Number.Real.< 0 (Number.Real.* x y) Number.Real.< 0 x)

x y. Number.Real.* x y = 0 x = 0 y = 0

x y.
    Number.Real.≤ 0 x Number.Real.< x y Number.Real.< (real./ x y) 1

x y.
    Number.Real.< 0 x Number.Real.< 0 y Number.Real.< 0 (real./ x y)

x y.
    Number.Real.< 0 x Number.Real.< 0 y
    Number.Real.< 0 (Number.Real.* x y)

x y.
    Number.Real.≤ 0 x Number.Real.≤ 0 y Number.Real.≤ 0 (real./ x y)

x y.
    Number.Real.≤ 0 x Number.Real.≤ 0 y
    Number.Real.≤ 0 (Number.Real.* x y)

y.
    ¬(y = 0)
    x.
      Number.Real.abs (real./ x y) =
      real./ (Number.Real.abs x) (Number.Real.abs y)

(t1 t2. (if then t1 else t2) = t1)
  t1 t2. (if then t1 else t2) = t2

(n. words.word_lo (words.n2w 0) n ¬(n = words.n2w 0))
  n. ¬words.word_lo n (words.n2w 0)

m n p. m arithmetic.- n p m + p n m 0

m n p. arithmetic.- m n < p m < n + p 0 < p

m n p. n * m = p * m m = 0 n = p

m n p. m * n < p * n 0 < n m < p

x n.
    bit.DIVMOD_2EXP x n =
    (n div arithmetic.BIT2 0 x, n mod arithmetic.BIT2 0 x)

v w.
    words.word_join v w =
    bool.LET
      (bool.LET
         (λcv cw.
            words.word_or (words.word_lsl cv (fcp.dimindex bool.the_value))
              cw) (words.w2w v)) (words.w2w w)

e a b. 1 < e (a < b e a < e b)

e a b. 1 < e (a b e a e b)

b. 1 < b n m. b m < b n m < n

b. 1 < b n m. b m b n m n

x y z.
    Number.Real.< 0 x
    (Number.Real.< (Number.Real.* x y) (Number.Real.* x z)
     Number.Real.< y z)

x y z.
    Number.Real.< 0 x
    (Number.Real.≤ (Number.Real.* x y) (Number.Real.* x z)
     Number.Real.≤ y z)

x y z. Number.Real.< 0 z (x = real./ y z Number.Real.* x z = y)

x y z.
    Number.Real.< 0 z
    (Number.Real.< x (real./ y z) Number.Real.< (Number.Real.* x z) y)

x y z.
    Number.Real.< 0 z
    (Number.Real.≤ x (real./ y z) Number.Real.≤ (Number.Real.* x z) y)

x y z. Number.Real.< 0 z (real./ x z = y x = Number.Real.* y z)

x y z.
    Number.Real.< 0 z
    (Number.Real.< (real./ x z) y Number.Real.< x (Number.Real.* y z))

x y z.
    Number.Real.< 0 z
    (Number.Real.≤ (real./ x z) y Number.Real.≤ x (Number.Real.* y z))

x y z.
    Number.Real.< 0 z
    (Number.Real.< (real./ x z) (real./ y z) Number.Real.< x y)

x y z.
    Number.Real.< 0 z
    (Number.Real.< (Number.Real.* x z) (Number.Real.* y z)
     Number.Real.< x y)

x y z. Number.Real.* x y = Number.Real.* x z x = 0 y = z

x y z. Number.Real.* x z = Number.Real.* y z z = 0 x = y

x y.
    x = y
    i.
      i < fcp.dimindex bool.the_value
      fcp.fcp_index x i = fcp.fcp_index y i

w i.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.w2w w) i
     i < fcp.dimindex bool.the_value fcp.fcp_index w i)

Fn. f. c i r. f (ind_type.CONSTR c i r) = Fn c i r (λn. f (r n))

numeral.iiSUC 0 = arithmetic.BIT2 0
  numeral.iiSUC (bit1 n) = bit1 (suc n)
  numeral.iiSUC (arithmetic.BIT2 n) = arithmetic.BIT2 (suc n)

m n x.
    Number.Real.< 1 x m < n
    Number.Real.< (Number.Real.↑ x m) (Number.Real.↑ x n)

n.
    numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n)
    numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n)
    numeral.iDUB 0 = 0

(n. n 0 = 1) m n. m suc n = m * m n

(p q r) (p q) (p ¬r) (¬q r ¬p)

(p q r) (p ¬q) (p ¬r) (q r ¬p)

Number.Real.* x (real./ y z) =
  if z = 0 then Number.Real.* x (marker.unint (real./ y z))
  else real./ (Number.Real.* x y) z

Number.Real.* (real./ x y) z =
  if y = 0 then Number.Real.* (marker.unint (real./ x y)) z
  else real./ (Number.Real.* x z) y

min 0 x = 0 min x 0 = 0 min x y = if x < y then x else y

(f v. const v f = const v) f v. f const v = const (f v)

w n.
    words.word_lsl w n =
    fcp.FCP
      (λi.
         i < fcp.dimindex bool.the_value n i
         fcp.fcp_index w (arithmetic.- i n))

R. wellFounded R P. (x. (y. R y x P y) P x) x. P x

(x. Number.Real.↑ x 0 = 1)
  x n. Number.Real.↑ x (suc n) = Number.Real.* x (Number.Real.↑ x n)

(a f. ind_type.FCONS a f 0 = a)
  a f n. ind_type.FCONS a f (suc n) = f n

x x' y y'. (x x') (x' (y y')) (x y x' y')

n k r. (q. k = q * n + r r < n) k mod n = r

c a.
    words.word_ls a (words.word_add c a)
    a = words.n2w 0 c = words.n2w 0
    words.word_lo a (words.word_2comp c)

(p q r) (p ¬q ¬r) (q ¬p) (r ¬p)

suc 0 = 1 (n. suc (bit1 n) = arithmetic.BIT2 n)
  n. suc (arithmetic.BIT2 n) = bit1 (suc n)

(n.
     words.word_ls (words.word_2comp (words.n2w 1)) n
     n = words.word_2comp (words.n2w 1))
  n. words.word_ls n (words.word_2comp (words.n2w 1))

h l n.
    bit.BITS h l n =
    n div arithmetic.BIT2 0 l mod
    arithmetic.BIT2 0 arithmetic.- (suc h) l

m n. 0 < m 0 < n x. x div m div n = x div m * n

P (arithmetic.- a b) d. (b = a + d P 0) (a = b + d P d)

A B. (¬(A B) ¬A ¬B) (¬(A B) ¬A ¬B)

m n.
    Number.Real.- (Number.Real.fromNatural m) (Number.Real.fromNatural n) =
    if arithmetic.- m n = 0 then
      Number.Real.~ (Number.Real.fromNatural (arithmetic.- n m))
    else Number.Real.fromNatural (arithmetic.- m n)

M R f.
    f = relation.WFREC R M wellFounded R
    x. f x = M (relation.RESTRICT f R x) x

Number.Real.+ x (real./ y z) =
  if z = 0 then Number.Real.+ x (marker.unint (real./ y z))
  else real./ (Number.Real.+ (Number.Real.* x z) y) z

x y.
    ¬(x = 0) ¬(y = 0)
    realax.inv (Number.Real.* x y) =
    Number.Real.* (realax.inv x) (realax.inv y)

n.
    even 0 even (arithmetic.BIT2 n) ¬even (bit1 n) ¬odd 0
    ¬odd (arithmetic.BIT2 n) odd (bit1 n)

(n. n 0 n = 0) m n. m suc n m = suc n m n

h l.
    words.word_bits h l =
    λw.
      fcp.FCP
        (λi.
           i + l min h (arithmetic.- (fcp.dimindex bool.the_value) 1)
           fcp.fcp_index w (i + l))

bool.TYPE_DEFINITION =
  λP rep.
    (x' x''. rep x' = rep x'' x' = x'') x. P x x'. x = rep x'

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

P.
    (rep. bool.TYPE_DEFINITION P rep)
    rep abs. (a. abs (rep a) = a) r. P r rep (abs r) = r

(m m * n m = 0 0 < n) (m n * m m = 0 0 < n)

numeral.texp_help 0 acc = arithmetic.BIT2 acc
  numeral.texp_help (bit1 n) acc =
  numeral.texp_help (prim_rec.PRE (bit1 n)) (bit1 acc)
  numeral.texp_help (arithmetic.BIT2 n) acc =
  numeral.texp_help (bit1 n) (bit1 acc)

numeral.exactlog 0 = 0 (n. numeral.exactlog (bit1 n) = 0)
  n.
    numeral.exactlog (arithmetic.BIT2 n) =
    bool.LET (λx. if x = 0 then 0 else bit1 x) (numeral.onecount n 0)

(x. numeral.onecount 0 x = x)
  (n x. numeral.onecount (bit1 n) x = numeral.onecount n (suc x))
  n x. numeral.onecount (arithmetic.BIT2 n) x = 0

arithmetic.BIT2 0 0 = 1
  arithmetic.BIT2 0 bit1 n =
  numeral.texp_help (prim_rec.PRE (bit1 n)) 0
  arithmetic.BIT2 0 arithmetic.BIT2 n = numeral.texp_help (bit1 n) 0

t. ( t t) (t t) ( t ) (t ) (t t t)

t. ( t ) (t ) ( t t) (t t) (t t t)

x1 x2 y1 y2.
    Number.Real.≤ 0 x1 Number.Real.≤ 0 y1 Number.Real.≤ x1 x2
    Number.Real.≤ y1 y2
    Number.Real.≤ (Number.Real.* x1 y1) (Number.Real.* x2 y2)

(m n.
     words.word_mul (words.n2w m) (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m * n)))
  m n.
    words.word_mul (words.word_2comp (words.n2w m))
      (words.word_2comp (words.n2w n)) = words.n2w (m * n)

t. ( t t) (t ) ( t ) (t t ) (t ¬t)

n m p. (min m n < p m < p n < p) (p < min m n p < m p < n)

n m p. (min m n p m p n p) (p min m n p m p n)

a.
    words.word_or words.word_T a = words.word_T
    words.word_or a words.word_T = words.word_T
    words.word_or (words.n2w 0) a = a words.word_or a (words.n2w 0) = a
    words.word_or a a = a

P Q x x' y y'.
    (P Q) (Q x = x') (¬Q y = y')
    (if P then x else y) = if Q then x' else y'

(p q r) (p q r) (p ¬r ¬q) (q ¬r ¬p) (r ¬q ¬p)

h l n w.
    h < fcp.dimindex bool.the_value
    words.word_extract h l (words.word_lsl w n) =
    if n h then
      words.word_lsl
        (words.word_extract (arithmetic.- h n) (arithmetic.- l n) w)
        (arithmetic.- n l)
    else words.n2w 0

(a. words.word_lsl a 0 = a) (a. words.word_asr a 0 = a)
  (a. words.word_lsr a 0 = a) (a. words.word_rol a 0 = a)
  a. words.word_ror a 0 = a

Number.Real.~ (real./ x y) =
  (if y = 0 then Number.Real.~ (marker.unint (real./ x y))
   else real./ (Number.Real.~ x) y)
  real./ x (Number.Real.~ y) =
  if y = 0 then marker.unint (real./ x y) else real./ (Number.Real.~ x) y

f g.
    (n. g (suc n) = f n (suc n))
    (n. g (bit1 n) = f (arithmetic.- (bit1 n) 1) (bit1 n))
    n. g (arithmetic.BIT2 n) = f (bit1 n) (arithmetic.BIT2 n)

w h l m n.
    words.word_extract h l (words.word_extract m n w) =
    words.word_extract
      (min m
         (min (h + n)
            (min (arithmetic.- (fcp.dimindex bool.the_value) 1)
               (arithmetic.- (fcp.dimindex bool.the_value + n) 1))))
      (l + n) w

n m.
    0 * n = 0 n * 0 = 0
    bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m)
    arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))

(m n.
     words.word_add (words.word_2comp (words.n2w m))
       (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m + n)))
  m n.
    words.word_add (words.n2w m) (words.word_2comp (words.n2w n)) =
    if n m then words.n2w (arithmetic.- m n)
    else words.word_2comp (words.n2w (arithmetic.- n m))

prim_rec.PRE 0 = 0 prim_rec.PRE 1 = 0
  (n.
     prim_rec.PRE (bit1 (bit1 n)) =
     arithmetic.BIT2 (prim_rec.PRE (bit1 n)))
  (n.
     prim_rec.PRE (bit1 (arithmetic.BIT2 n)) = arithmetic.BIT2 (bit1 n))
  n. prim_rec.PRE (arithmetic.BIT2 n) = bit1 n

Number.Real.* (real./ x y) (real./ u v) =
  if y = 0 then Number.Real.* (marker.unint (real./ x y)) (real./ u v)
  else if v = 0 then Number.Real.* (real./ x y) (marker.unint (real./ u v))
  else real./ (Number.Real.* x u) (Number.Real.* y v)

(bit1 x * y = z y = z div bit1 x z mod bit1 x = 0)
  (arithmetic.BIT2 x * y = z
   y = z div arithmetic.BIT2 x z mod arithmetic.BIT2 x = 0)

(m n.
     m < bit1 n
     m = arithmetic.- (bit1 n) 1 m < arithmetic.- (bit1 n) 1)
  m n. m < arithmetic.BIT2 n m = bit1 n m < bit1 n

words.word_extract h l (words.n2w n) =
  if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
    words.n2w
      (bit.BITS (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l n)
  else
    words.n2w
      (bit.BITS
         (min (min h (arithmetic.- (fcp.dimindex bool.the_value) 1))
            (arithmetic.- (fcp.dimindex bool.the_value) 1 + l)) l n)

(a b. bit.MOD_2EXP_EQ 0 a b )
  (n a b.
     bit.MOD_2EXP_EQ (suc n) a b
     (odd a odd b)
     bit.MOD_2EXP_EQ n (arithmetic.DIV2 a) (arithmetic.DIV2 b))
  n a. bit.MOD_2EXP_EQ n a a

(m n.
     words.n2w m = words.n2w n
     bit.MOD_2EXP_EQ (fcp.dimindex bool.the_value) m n)
  (n.
     words.n2w n = words.word_2comp (words.n2w 1)
     bit.MOD_2EXP_MAX (fcp.dimindex bool.the_value) n)
  n.
    words.word_2comp (words.n2w 1) = words.n2w n
    bit.MOD_2EXP_MAX (fcp.dimindex bool.the_value) n

(n. words.word_lsl (words.n2w 0) n = words.n2w 0)
  (n. words.word_asr (words.n2w 0) n = words.n2w 0)
  (n. words.word_lsr (words.n2w 0) n = words.n2w 0)
  (n. words.word_rol (words.n2w 0) n = words.n2w 0)
  n. words.word_ror (words.n2w 0) n = words.n2w 0

(Number.Real.< (Number.Real.fromNatural n) (Number.Real.fromNatural m)
   n < m)
  (Number.Real.< (Number.Real.~ (Number.Real.fromNatural n))
     (Number.Real.fromNatural m) ¬(n = 0) ¬(m = 0))
  (Number.Real.< (Number.Real.fromNatural n)
     (Number.Real.~ (Number.Real.fromNatural m)) )
  (Number.Real.< (Number.Real.~ (Number.Real.fromNatural n))
     (Number.Real.~ (Number.Real.fromNatural m)) m < n)

real./ x y = real./ u v
  if y = 0 then marker.unint (real./ x y) = real./ u v
  else if v = 0 then real./ x y = marker.unint (real./ u v)
  else if y = v then x = u
  else Number.Real.* x v = Number.Real.* y u

Number.Real.* (Number.Real.fromNatural a) (Number.Real.fromNatural b) =
  Number.Real.fromNatural (a * b)
  Number.Real.* (Number.Real.~ (Number.Real.fromNatural a))
    (Number.Real.fromNatural b) =
  Number.Real.~ (Number.Real.fromNatural (a * b))
  Number.Real.* (Number.Real.fromNatural a)
    (Number.Real.~ (Number.Real.fromNatural b)) =
  Number.Real.~ (Number.Real.fromNatural (a * b))
  Number.Real.* (Number.Real.~ (Number.Real.fromNatural a))
    (Number.Real.~ (Number.Real.fromNatural b)) =
  Number.Real.fromNatural (a * b)

m n.
    0 * m = 0 m * 0 = 0 1 * m = m m * 1 = m suc m * n = m * n + n
    m * suc n = m + m * n

(Number.Real.fromNatural n = Number.Real.fromNatural m n = m)
  (Number.Real.~ (Number.Real.fromNatural n) = Number.Real.fromNatural m
   n = 0 m = 0)
  (Number.Real.fromNatural n = Number.Real.~ (Number.Real.fromNatural m)
   n = 0 m = 0)
  (Number.Real.~ (Number.Real.fromNatural n) =
   Number.Real.~ (Number.Real.fromNatural m) n = m)

h m m' l s w.
    l m m' h m' = m + 1 s = arithmetic.- m' l
    words.word_or (words.word_lsl (words.word_extract h m' w) s)
      (words.word_extract m l w) =
    words.word_extract
      (min h
         (min (arithmetic.- (fcp.dimindex bool.the_value + l) 1)
            (arithmetic.- (fcp.dimindex bool.the_value) 1))) l w

v w.
    words.word_mul (words.n2w 0) v = words.n2w 0
    words.word_mul v (words.n2w 0) = words.n2w 0
    words.word_mul (words.n2w 1) v = v
    words.word_mul v (words.n2w 1) = v
    words.word_mul (words.word_add v (words.n2w 1)) w =
    words.word_add (words.word_mul v w) w
    words.word_mul v (words.word_add w (words.n2w 1)) =
    words.word_add v (words.word_mul v w)

n m.
    (0 n ) (bit1 n 0 ) (arithmetic.BIT2 n 0 )
    (bit1 n bit1 m n m) (bit1 n arithmetic.BIT2 m n m)
    (arithmetic.BIT2 n bit1 m ¬(m n))
    (arithmetic.BIT2 n arithmetic.BIT2 m n m)

n m.
    (0 < bit1 n ) (0 < arithmetic.BIT2 n ) (n < 0 )
    (bit1 n < bit1 m n < m)
    (arithmetic.BIT2 n < arithmetic.BIT2 m n < m)
    (bit1 n < arithmetic.BIT2 m ¬(m < n))
    (arithmetic.BIT2 n < bit1 m n < m)

Number.Real.↑ x 0 = 1 Number.Real.↑ 0 (bit1 n) = 0
  Number.Real.↑ 0 (arithmetic.BIT2 n) = 0
  Number.Real.↑ (Number.Real.fromNatural a) n =
  Number.Real.fromNatural (a n)
  Number.Real.↑ (Number.Real.~ (Number.Real.fromNatural a)) n =
  (if odd n then Number.Real.~ else λx. x)
    (Number.Real.fromNatural (a n))
  Number.Real.↑ (real./ x y) n =
  real./ (Number.Real.↑ x n) (Number.Real.↑ y n)

n m.
    (0 = bit1 n ) (bit1 n = 0 ) (0 = arithmetic.BIT2 n )
    (arithmetic.BIT2 n = 0 ) (bit1 n = arithmetic.BIT2 m )
    (arithmetic.BIT2 n = bit1 m ) (bit1 n = bit1 m n = m)
    (arithmetic.BIT2 n = arithmetic.BIT2 m n = m)

Number.Real.+ (Number.Real.fromNatural n) (Number.Real.fromNatural m) =
  Number.Real.fromNatural (n + m)
  Number.Real.+ (Number.Real.~ (Number.Real.fromNatural n))
    (Number.Real.fromNatural m) =
  (if n m then Number.Real.fromNatural (arithmetic.- m n)
   else Number.Real.~ (Number.Real.fromNatural (arithmetic.- n m)))
  Number.Real.+ (Number.Real.fromNatural n)
    (Number.Real.~ (Number.Real.fromNatural m)) =
  (if n < m then Number.Real.~ (Number.Real.fromNatural (arithmetic.- m n))
   else Number.Real.fromNatural (arithmetic.- n m))
  Number.Real.+ (Number.Real.~ (Number.Real.fromNatural n))
    (Number.Real.~ (Number.Real.fromNatural m)) =
  Number.Real.~ (Number.Real.fromNatural (n + m))

(h l v w.
     words.word_and (words.word_extract h l v) (words.word_extract h l w) =
     words.word_extract h l (words.word_and v w))
  (h l v w.
     words.word_or (words.word_extract h l v) (words.word_extract h l w) =
     words.word_extract h l (words.word_or v w))
  h l v w.
    words.word_xor (words.word_extract h l v) (words.word_extract h l w) =
    words.word_extract h l (words.word_xor v w)

0 * n = 0 n * 0 = 0
  bit1 x * bit1 y = numeral.internal_mult (bit1 x) (bit1 y)
  bit1 x * arithmetic.BIT2 y =
  bool.LET
    (λn.
       if odd n then
         numeral.texp_help (arithmetic.DIV2 n) (prim_rec.PRE (bit1 x))
       else numeral.internal_mult (bit1 x) (arithmetic.BIT2 y))
    (numeral.exactlog (arithmetic.BIT2 y))
  arithmetic.BIT2 x * bit1 y =
  bool.LET
    (λm.
       if odd m then
         numeral.texp_help (arithmetic.DIV2 m) (prim_rec.PRE (bit1 y))
       else numeral.internal_mult (arithmetic.BIT2 x) (bit1 y))
    (numeral.exactlog (arithmetic.BIT2 x))
  arithmetic.BIT2 x * arithmetic.BIT2 y =
  bool.LET
    (λm.
       bool.LET
         (λn.
            if odd m then
              numeral.texp_help (arithmetic.DIV2 m)
                (prim_rec.PRE (arithmetic.BIT2 y))
            else if odd n then
              numeral.texp_help (arithmetic.DIV2 n)
                (prim_rec.PRE (arithmetic.BIT2 x))
            else
              numeral.internal_mult (arithmetic.BIT2 x)
                (arithmetic.BIT2 y))
         (numeral.exactlog (arithmetic.BIT2 y)))
    (numeral.exactlog (arithmetic.BIT2 x))

b n m.
    numeral.iSUB b 0 x = 0 numeral.iSUB n 0 = n
    numeral.iSUB (bit1 n) 0 = numeral.iDUB n
    numeral.iSUB (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (bit1 m) = bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) 0 = bit1 n
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)

n m.
    numeral.iZ (0 + n) = n numeral.iZ (n + 0) = n
    numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m))
    numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (suc (n + m)) suc (0 + n) = suc n
    suc (n + 0) = suc n suc (bit1 n + bit1 m) = bit1 (suc (n + m))
    suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (0 + n) = numeral.iiSUC n
    numeral.iiSUC (n + 0) = numeral.iiSUC n
    numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (numeral.iiSUC (n + m))

(n. 0 + n = n) (n. n + 0 = n) (n m. n + m = numeral.iZ (n + m))
  (n. 0 * n = 0) (n. n * 0 = 0) (n m. n * m = n * m)
  (n. arithmetic.- 0 n = 0) (n. arithmetic.- n 0 = n)
  (n m. arithmetic.- n m = arithmetic.- n m) (n. 0 bit1 n = 0)
  (n. 0 arithmetic.BIT2 n = 0) (n. n 0 = 1)
  (n m. n m = n m) suc 0 = 1 (n. suc n = suc n)
  prim_rec.PRE 0 = 0 (n. prim_rec.PRE n = prim_rec.PRE n)
  (n. n = 0 n = 0) (n. 0 = n n = 0) (n m. n = m n = m)
  (n. n < 0 ) (n. 0 < n 0 < n) (n m. n < m n < m)
  (n. 0 > n ) (n. n > 0 0 < n) (n m. n > m m < n)
  (n. 0 n ) (n. n 0 n 0) (n m. n m n m)
  (n. n 0 ) (n. 0 n n = 0) (n m. n m m n)
  (n. odd n odd n) (n. even n even n) ¬odd 0 even 0