def tbf

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64nrp.bend:50

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/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT

50# the top bits of shift(k, V) when k + bit_length(V) = J
51def tbf(+k: Nat, +V: Nat, +J: Nat, +ek: {Nat.add(k, M.bit_length(V)) == J : Nat}) -> {C.fits(J, C.shift(k, V)) == True{} : Bool}:
52  L.subst(Nat, z => {C.fits(z, C.shift(k, V)) == True{} : Bool}, Nat.add(k, M.bit_length(V)), J, ek, Equal.trans(Bool, C.fits(Nat.add(k, M.bit_length(V)), C.shift(k, V)), C.fits(M.bit_length(V), V), True{}, RT.fits_sh(k, M.bit_length(V), V), RT.bl_fit(V)))