def lt62

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mulp.bend:44

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/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
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

44def lt62(+one: Nat, +h1: {one == 1n : Nat}, +sig: WU.U64, +c: U32, +hc: {c == U32{WD.pw(32n, 30n)} : U32}) -> {X.lt(sig, WU.U64{0, c}) == C.fits(62n, SW.value(sig)) : Bool}:
45  l1 = WA.lt_value(sig, WU.U64{0, c})
46  +ec = Equal.trans(Nat, C.shift(32n, v(c)), C.shift(32n, C.shift(30n, one)), C.shift(62n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(c), C.shift(30n, one), FB.pwv(30n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(62n, one), C.shift(32n, C.shift(30n, one)), WW.shift_comp(32n, 30n, one)))
47  Equal.trans(Bool, X.lt(sig, WU.U64{0, c}), Nat.is_lt(SW.value(sig), C.shift(32n, v(c))), C.fits(62n, SW.value(sig)), l1, Equal.trans(Bool, Nat.is_lt(SW.value(sig), C.shift(32n, v(c))), Nat.is_lt(SW.value(sig), C.shift(62n, one)), C.fits(62n, SW.value(sig)), Equal.cong(Nat, Bool, z => Nat.is_lt(SW.value(sig), z), C.shift(32n, v(c)), C.shift(62n, one), ec), FR.lt_fit(62n, one, h1, SW.value(sig))))