def mant_z

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:223

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

223# the significand is zero exactly for the zeros
224def mant_z(+x: F.F64) -> {Nat.is_eq(SF.mant(x), 0n) == SF.is_zero(x) : Bool}:
225  +c = Nat.is_eq(SF.efield(x), 0n)
226  +fz0 = Nat.is_eq(SF.frac(x), 0n)
227  +e1 = FB.z2(SF.frac(x), 52n, SF.b2n(Bool.not(c)))
228  +e2 = Equal.cong(Bool, Bool, b => Bool.and(fz0, b), Nat.is_eq(SF.b2n(Bool.not(c)), 0n), c, bzc(c))
229  Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), Bool.and(fz0, Nat.is_eq(SF.b2n(Bool.not(c)), 0n)), SF.is_zero(x), e1, Equal.trans(Bool, Bool.and(fz0, Nat.is_eq(SF.b2n(Bool.not(c)), 0n)), Bool.and(fz0, c), SF.is_zero(x), e2, and_comm(fz0, c)))