def signbit_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:230

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/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

230def signbit_g(+one: Nat, +h1: {one == 1n : Nat}, +l: U32, +h: U32, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {Cmp.is_le(U32.cmp(c, h)) == SF.sign(F.Bits{l, h}) : Bool}:
231  +e1 = Equal.cong(Cmp, Bool, t => Cmp.is_le(t), U32.cmp(c, h), Nat.cmp(v(c), v(h)), U.u32_cmp(c, h))
232  +e2 = Equal.cong(Nat, Bool, z => Nat.is_le(z, v(h)), v(c), C.shift(31n, one), pwv(31n, {==}, one, h1, c, hc))
233  Equal.trans(Bool, Cmp.is_le(U32.cmp(c, h)), Nat.is_le(v(c), v(h)), Bool.not(C.fits(31n, v(h))), e1, Equal.trans(Bool, Nat.is_le(v(c), v(h)), Nat.is_le(C.shift(31n, one), v(h)), Bool.not(C.fits(31n, v(h))), e2, le_fit(31n, one, h1, v(h))))