def nz0

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:329

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

329def nz0(+y: F.F64) -> {F.Bits{1, F.sgn(F.signbit(y))} == SF.encode(SF.sign(y), 0n, 1n) : F.F64}:
330  +s = SF.sign(y)
331  +e1 = Equal.cong(Bool, F.F64, t => F.Bits{1, F.sgn(t)}, F.signbit(y), s, FB.signbit_value(y))
332  +e2 = Equal.sym(F.F64, FR.bits(s, 1n), F.Bits{1, F.sgn(s)}, bsg(s))
333  +e3 = Equal.sym(F.F64, SF.encode(s, 0n, 1n), FR.bits(s, 1n), FR.enc_bits(s, 0n, 1n))
334  Equal.trans(F.F64, F.Bits{1, F.sgn(F.signbit(y))}, F.Bits{1, F.sgn(s)}, SF.encode(s, 0n, 1n), e1, Equal.trans(F.F64, F.Bits{1, F.sgn(s)}, FR.bits(s, 1n), SF.encode(s, 0n, 1n), e2, e3))