F64next.bsg: 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 323-327 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=323&end_line=327

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/f64round.bend as FR

def bsg(+s: Bool) -> {FR.bits(s, 1n) == F.Bits{1, F.sgn(s)} : F.F64}:
  +e1 = Equal.cong(Nat, F.F64, z => F.Bits{U32.from_nat(1n), U32.from_nat(C.shift(31n, z))}, SF.b2n(s), SF.pick(Nat, s, 1n, 0n), Equal.sym(Nat, SF.pick(Nat, s, 1n, 0n), SF.b2n(s), FR.pb(s, 1n, {==})))
  +e2 = bs0(1n, {==}, s, 2147483648, {==})
  +e3 = Equal.cong(U32, F.F64, z => F.Bits{1, z}, SF.pick(U32, s, 2147483648, 0), F.sgn(s), Equal.sym(U32, F.sgn(s), SF.pick(U32, s, 2147483648, 0), FR.sgn_pick(s)))
  Equal.trans(F.F64, FR.bits(s, 1n), F.Bits{U32.from_nat(1n), U32.from_nat(C.shift(31n, SF.pick(Nat, s, 1n, 0n)))}, F.Bits{1, F.sgn(s)}, e1, Equal.trans(F.F64, F.Bits{U32.from_nat(1n), U32.from_nat(C.shift(31n, SF.pick(Nat, s, 1n, 0n)))}, F.Bits{1, SF.pick(U32, s, 2147483648, 0)}, F.Bits{1, F.sgn(s)}, e2, e3))

Uses (16):
  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=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&name=bs0
  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=pb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=sgn_pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n
  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/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