def shb_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64est.bend:49

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/proofs/lib/nat.bend as N
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/width.bend as WW

49# high(t, b) 2^t <= b
50def shb_le(+t: Nat, +bv: Nat) -> {Nat.is_le(C.shift(t, C.high(t, bv)), bv) == True{} : Bool}:
51  +s = C.shift(t, C.high(t, bv))
52  +l0 = C.low(t, bv)
53  +eq = Equal.trans(Nat, Nat.add(s, l0), Nat.add(l0, s), bv, N.add_comm(s, l0), Equal.sym(Nat, bv, Nat.add(l0, s), WW.low_high(t, bv)))
54  L.subst(Nat, z => {Nat.is_le(s, z) == True{} : Bool}, Nat.add(s, l0), bv, eq, N.le_add_right(s, l0))