F64next.nzc: 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 339-349 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=339&end_line=349

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/f64cmp.bend as FC

def nzc(+x: F.F64, +y: F.F64, +hu: {Bool.or(SF.is_nan(x), SF.is_nan(y)) == False{} : Bool}, +iz: Bool, +hiz: {SF.is_zero(x) == iz : Bool}) -> {F.na_z(x, y, iz) == SF.pick(F.F64, iz, SF.encode(SF.sign(y), 0n, 1n), STEP(x, y)) : F.F64}:
  match iz:
    case True{}:
      nz0(y)
    case False{}:
      +e1 = Equal.cong(Bool, F.F64, t => F.na_step(x, Bool.xor(t, F.signbit(x))), F.lt(x, y), Cmp.is_lt(SF.ord(x, y)), ltc(x, y, hu))
      +e2 = Equal.cong(Bool, F.F64, t => F.na_step(x, Bool.xor(Cmp.is_lt(SF.ord(x, y)), t)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
      +e3 = st_c(x, FC.or_l(SF.is_nan(x), SF.is_nan(y), hu), hiz, Bool.xor(Cmp.is_lt(SF.ord(x, y)), SF.sign(x)))
      +a1 = F.na_step(x, Bool.xor(Cmp.is_lt(SF.ord(x, y)), F.signbit(x)))
      +a2 = F.na_step(x, Bool.xor(Cmp.is_lt(SF.ord(x, y)), SF.sign(x)))
      Equal.trans(F.F64, F.na_step(x, Bool.xor(F.lt(x, y), F.signbit(x))), a1, STEP(x, y), e1, Equal.trans(F.F64, a1, a2, STEP(x, y), e2, e3))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.xor
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_lt
  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.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/f64cmp.bend&name=or_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&name=STEP
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&name=ltc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&name=nz0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&name=st_c
  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=is_nan
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=ord
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  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=lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=na_step
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=na_z
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=signbit