def unfit_one

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

247# with a symbolic one == 1 (so no closed 2^k appears where these are used)
248def unfit_one(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +r: Nat) -> {C.fits(k, Nat.add(r, C.shift(k, one))) == False{} : Bool}:
249  L.subst(Nat, z => {C.fits(k, Nat.add(r, C.shift(k, z))) == False{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), unfit_shift(k, r, 0n))