def unfit_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:235

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

235# shift(k, q) with q >= 1 does not fit k bits added to anything
236def unfit_shift(+k: Nat, +r: Nat, +qp: Nat) -> {C.fits(k, Nat.add(r, C.shift(k, 1n+qp))) == False{} : Bool}:
237  +h1 = N.le_trans(C.pow2(k), C.shift(k, 1n+qp), Nat.add(r, C.shift(k, 1n+qp)), L.subst(Nat, z => {Nat.is_le(z, C.shift(k, 1n+qp)) == True{} : Bool}, C.shift(k, 1n), C.pow2(k), shift_one(k), shift_mono(k, 1n, 1n+qp, N.zero_le(qp))), L.subst(Nat, z => {Nat.is_le(C.shift(k, 1n+qp), z) == True{} : Bool}, Nat.add(C.shift(k, 1n+qp), r), Nat.add(r, C.shift(k, 1n+qp)), N.add_comm(C.shift(k, 1n+qp), r), N.le_add_right(C.shift(k, 1n+qp), r)))
238  Equal.trans(Bool, C.fits(k, Nat.add(r, C.shift(k, 1n+qp))), Nat.is_lt(Nat.add(r, C.shift(k, 1n+qp)), C.pow2(k)), False{}, fits_lt(k, Nat.add(r, C.shift(k, 1n+qp))), N.le_not_lt(Nat.add(r, C.shift(k, 1n+qp)), C.pow2(k), h1))