Package hol-floating-point: HOL floating point theories
Information
| name | hol-floating-point |
| version | 1.1 |
| description | HOL floating point theories |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | badaaa151d79d4d7f6fc3966e93133726b89c39d |
| requires | base hol-base hol-words hol-integer hol-real |
| show | Data.Bool Data.Pair Function HOL4 Number.Natural Relation |
Files
- Package tarball hol-floating-point-1.1.tgz
- Theory source file hol-floating-point.thy (included in the package tarball)
Defined Type Operators
- HOL4
- binary_ieee
- binary_ieee.float
- binary_ieee.float_compare
- binary_ieee.float_value
- binary_ieee.rounding
- binary_ieee
Defined Constants
- HOL4
- binary_ieee
- binary_ieee.closest
- binary_ieee.closest_such
- binary_ieee.exponent_boundary
- binary_ieee.float_CASE
- binary_ieee.float_Exponent
- binary_ieee.float_Exponent_fupd
- binary_ieee.float_Sign
- binary_ieee.float_Sign_fupd
- binary_ieee.float_Significand
- binary_ieee.float_Significand_fupd
- binary_ieee.float_abs
- binary_ieee.float_abs1985
- binary_ieee.float_add
- binary_ieee.float_bottom
- binary_ieee.float_compare
- binary_ieee.float_compare2num
- binary_ieee.float_compare_CASE
- binary_ieee.float_compare_size
- binary_ieee.float_div
- binary_ieee.float_equal
- binary_ieee.float_greater_equal
- binary_ieee.float_greater_than
- binary_ieee.float_is_finite
- binary_ieee.float_is_infinite
- binary_ieee.float_is_integral
- binary_ieee.float_is_nan
- binary_ieee.float_is_normal
- binary_ieee.float_is_subnormal
- binary_ieee.float_is_zero
- binary_ieee.float_less_equal
- binary_ieee.float_less_than
- binary_ieee.float_minus_infinity
- binary_ieee.float_minus_min
- binary_ieee.float_minus_zero
- binary_ieee.float_mul
- binary_ieee.float_mul_add
- binary_ieee.float_mul_sub
- binary_ieee.float_negate
- binary_ieee.float_negate1985
- binary_ieee.float_plus_infinity
- binary_ieee.float_plus_min
- binary_ieee.float_plus_zero
- binary_ieee.float_round
- binary_ieee.float_round_to_integral
- binary_ieee.float_size
- binary_ieee.float_some_nan
- binary_ieee.float_sqrt
- binary_ieee.float_sub
- binary_ieee.float_to_int
- binary_ieee.float_to_real
- binary_ieee.float_top
- binary_ieee.float_value
- binary_ieee.float_value_CASE
- binary_ieee.float_value_size
- binary_ieee.integral_round
- binary_ieee.is_closest
- binary_ieee.largest
- binary_ieee.num2float_compare
- binary_ieee.num2rounding
- binary_ieee.real_to_float
- binary_ieee.recordtype.float
- binary_ieee.round
- binary_ieee.roundTiesToEven
- binary_ieee.roundTowardNegative
- binary_ieee.roundTowardPositive
- binary_ieee.roundTowardZero
- binary_ieee.rounding2num
- binary_ieee.rounding_CASE
- binary_ieee.rounding_size
- binary_ieee.threshold
- binary_ieee.ulp
- binary_ieee.EQ
- binary_ieee.Float
- binary_ieee.GT
- binary_ieee.Infinity
- binary_ieee.LT
- binary_ieee.NaN
- binary_ieee.ULP
- binary_ieee.UN
- machine_ieee
- machine_ieee.convert
- machine_ieee.float_to_fp16
- machine_ieee.float_to_fp32
- machine_ieee.float_to_fp64
- machine_ieee.fp16_abs
- machine_ieee.fp16_abs1985
- machine_ieee.fp16_add
- machine_ieee.fp16_bottom
- machine_ieee.fp16_compare
- machine_ieee.fp16_div
- machine_ieee.fp16_equal
- machine_ieee.fp16_greaterEqual
- machine_ieee.fp16_greaterThan
- machine_ieee.fp16_isFinite
- machine_ieee.fp16_isInfinite
- machine_ieee.fp16_isIntegral
- machine_ieee.fp16_isNan
- machine_ieee.fp16_isNormal
- machine_ieee.fp16_isSubnormal
- machine_ieee.fp16_isZero
- machine_ieee.fp16_lessEqual
- machine_ieee.fp16_lessThan
- machine_ieee.fp16_mul
- machine_ieee.fp16_mul_add
- machine_ieee.fp16_mul_sub
- machine_ieee.fp16_negInf
- machine_ieee.fp16_negMin
- machine_ieee.fp16_negZero
- machine_ieee.fp16_negate
- machine_ieee.fp16_negate1985
- machine_ieee.fp16_posInf
- machine_ieee.fp16_posMin
- machine_ieee.fp16_posZero
- machine_ieee.fp16_roundToIntegral
- machine_ieee.fp16_sqrt
- machine_ieee.fp16_sub
- machine_ieee.fp16_to_float
- machine_ieee.fp16_to_int
- machine_ieee.fp16_to_real
- machine_ieee.fp16_top
- machine_ieee.fp32_abs
- machine_ieee.fp32_abs1985
- machine_ieee.fp32_add
- machine_ieee.fp32_bottom
- machine_ieee.fp32_compare
- machine_ieee.fp32_div
- machine_ieee.fp32_equal
- machine_ieee.fp32_greaterEqual
- machine_ieee.fp32_greaterThan
- machine_ieee.fp32_isFinite
- machine_ieee.fp32_isInfinite
- machine_ieee.fp32_isIntegral
- machine_ieee.fp32_isNan
- machine_ieee.fp32_isNormal
- machine_ieee.fp32_isSubnormal
- machine_ieee.fp32_isZero
- machine_ieee.fp32_lessEqual
- machine_ieee.fp32_lessThan
- machine_ieee.fp32_mul
- machine_ieee.fp32_mul_add
- machine_ieee.fp32_mul_sub
- machine_ieee.fp32_negInf
- machine_ieee.fp32_negMin
- machine_ieee.fp32_negZero
- machine_ieee.fp32_negate
- machine_ieee.fp32_negate1985
- machine_ieee.fp32_posInf
- machine_ieee.fp32_posMin
- machine_ieee.fp32_posZero
- machine_ieee.fp32_roundToIntegral
- machine_ieee.fp32_sqrt
- machine_ieee.fp32_sub
- machine_ieee.fp32_to_float
- machine_ieee.fp32_to_fp64
- machine_ieee.fp32_to_int
- machine_ieee.fp32_to_real
- machine_ieee.fp32_top
- machine_ieee.fp64_abs
- machine_ieee.fp64_abs1985
- machine_ieee.fp64_add
- machine_ieee.fp64_bottom
- machine_ieee.fp64_compare
- machine_ieee.fp64_div
- machine_ieee.fp64_equal
- machine_ieee.fp64_greaterEqual
- machine_ieee.fp64_greaterThan
- machine_ieee.fp64_isFinite
- machine_ieee.fp64_isInfinite
- machine_ieee.fp64_isIntegral
- machine_ieee.fp64_isNan
- machine_ieee.fp64_isNormal
- machine_ieee.fp64_isSubnormal
- machine_ieee.fp64_isZero
- machine_ieee.fp64_lessEqual
- machine_ieee.fp64_lessThan
- machine_ieee.fp64_mul
- machine_ieee.fp64_mul_add
- machine_ieee.fp64_mul_sub
- machine_ieee.fp64_negInf
- machine_ieee.fp64_negMin
- machine_ieee.fp64_negZero
- machine_ieee.fp64_negate
- machine_ieee.fp64_negate1985
- machine_ieee.fp64_posInf
- machine_ieee.fp64_posMin
- machine_ieee.fp64_posZero
- machine_ieee.fp64_roundToIntegral
- machine_ieee.fp64_sqrt
- machine_ieee.fp64_sub
- machine_ieee.fp64_to_float
- machine_ieee.fp64_to_fp32
- machine_ieee.fp64_to_int
- machine_ieee.fp64_to_real
- machine_ieee.fp64_top
- machine_ieee.int_to_fp16
- machine_ieee.int_to_fp32
- machine_ieee.int_to_fp64
- machine_ieee.real_to_fp16
- machine_ieee.real_to_fp32
- machine_ieee.real_to_fp64
- binary_ieee
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
- →
- bool
- Data
- Option
- Data.Option.option
- Pair
- ×
- Sum
- Data.Sum.+
- Unit
- Data.Unit.unit
- Option
- HOL4
- bool
- bool.itself
- fcp
- fcp.bit0
- fcp.bit1
- fcp.cart
- ind_type
- ind_type.recspace
- integer
- integer.int
- bool
- Number
- Natural
- natural
- Real
- Number.Real.real
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- Option
- Data.Option.none
- Data.Option.some
- Pair
- ,
- fst
- snd
- Bool
- Function
- const
- id
- ∘
- HOL4
- arithmetic
- arithmetic.-
- arithmetic.BIT2
- arithmetic.DIV2
- bit
- bit.BITS
- bit.DIVMOD_2EXP
- bit.MOD_2EXP
- bit.MOD_2EXP_EQ
- bit.MOD_2EXP_MAX
- bool
- bool.the_value
- bool.ARB
- bool.IN
- bool.LET
- bool.TYPE_DEFINITION
- fcp
- fcp.dimindex
- fcp.fcp_index
- fcp.FCP
- ind_type
- ind_type.BOTTOM
- ind_type.CONSTR
- ind_type.FCONS
- integer
- integer.ABS
- integer.Num
- intreal
- intreal.real_of_int
- intreal.INT_CEILING
- intreal.INT_FLOOR
- marker
- marker.unint
- marker.Abbrev
- numeral
- numeral.exactlog
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- numeral.internal_mult
- numeral.onecount
- numeral.texp_help
- pair
- pair.pair_CASE
- pair.UNCURRY
- pred_set
- pred_set.EMPTY
- pred_set.FINITE
- pred_set.GSPEC
- pred_set.INSERT
- pred_set.UNIV
- prim_rec
- prim_rec.PRE
- real
- real./
- realax
- realax.inv
- relation
- relation.RESTRICT
- relation.WFREC
- transc
- transc.sqrt
- words
- words.dimword
- words.n2w
- words.w2n
- words.w2w
- words.word_1comp
- words.word_2comp
- words.word_T
- words.word_add
- words.word_and
- words.word_asr
- words.word_bits
- words.word_concat
- words.word_extract
- words.word_join
- words.word_lo
- words.word_ls
- words.word_lsb
- words.word_lsl
- words.word_lsr
- words.word_mul
- words.word_or
- words.word_rol
- words.word_ror
- words.word_sub
- words.word_xor
- words.INT_MAX
- words.INT_MIN
- words.UINT_MAX
- arithmetic
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- div
- even
- min
- mod
- odd
- suc
- zero
- Real
- Number.Real.*
- Number.Real.+
- Number.Real.-
- Number.Real.<
- Number.Real.≤
- Number.Real.>
- Number.Real.≥
- Number.Real.↑
- Number.Real.~
- Number.Real.abs
- Number.Real.fromNatural
- Natural
- Relation
- empty
- wellFounded
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