def bsg

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

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

323def bsg(+s: Bool) -> {FR.bits(s, 1n) == F.Bits{1, F.sgn(s)} : F.F64}:
324  +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, {==})))
325  +e2 = bs0(1n, {==}, s, 2147483648, {==})
326  +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)))
327  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))