F64next.nz0: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as F64next
Lines 329-334 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&start_line=329&end_line=334

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

def nz0(+y: F.F64) -> {F.Bits{1, F.sgn(F.signbit(y))} == SF.encode(SF.sign(y), 0n, 1n) : F.F64}:
  +s = SF.sign(y)
  +e1 = Equal.cong(Bool, F.F64, t => F.Bits{1, F.sgn(t)}, F.signbit(y), s, FB.signbit_value(y))
  +e2 = Equal.sym(F.F64, FR.bits(s, 1n), F.Bits{1, F.sgn(s)}, bsg(s))
  +e3 = Equal.sym(F.F64, SF.encode(s, 0n, 1n), FR.bits(s, 1n), FR.enc_bits(s, 0n, 1n))
  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))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=signbit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&name=bsg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=enc_bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sign
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sgn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=signbit