def hab_of

bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:303

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/random/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WI
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as AR

303# t <= 2^w for t < n <= 2^w
304def hab_of(+w: Nat, +m: Nat, +k: Nat, +hw: {C.fits(w, 1n+m) == True{} : Bool}) -> {Nat.is_le(Nat.add(SR.pow2mod(w, 1n+m), C.shift(w, k)), C.shift(w, 1n+k)) == True{} : Bool}:
305  +W = C.shift(w, 1n)
306  +t = SR.pow2mod(w, 1n+m)
307  +ht = N.lt_le(t, W, N.lt_trans(t, 1n+m, W,
308    %Equal.sym(Nat, SR.pow2mod(w, 1n+m), Nat.mod(W, 1n+m), pm(w, m)) : {Nat.is_lt(_, 1n+m) == True{} : Bool}
309    AR.dm_lt(m, W),
310    WI.lt_one(w, 1n, {==}, 1n+m, hw)))
311  %Equal.sym(Nat, C.shift(w, 1n+k), Nat.add(W, C.shift(w, k)), WI.shift_add(w, 1n, k)) : {Nat.is_le(Nat.add(t, C.shift(w, k)), _) == True{} : Bool}
312  WI.le_add_r(t, W, C.shift(w, k), ht)