def bitw.ctz_clz

bend-osdev-algo@0.1.0.0 · PROOF.bend:523

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

523def bitw.ctz_clz(+m: Nat, +w: Word(1n+m), +k: Nat, +e: {A.bitw.index(A.bitw.ffs(1n+m, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(Nat.add(A.bitw.ctz(1n+m, w), A.bitw.clz(1n+m, w)), m) == True{} : Bool}:
524  %Equal.sym(Nat, A.bitw.ctz(1n+m, w), k, bitw.ctz_first_set(1n+m, w, k, e)) : {Nat.is_le(Nat.add(_, A.bitw.clz(1n+m, w)), m) == True{} : Bool}
525  bitw.ctz_clz.h(k, m, A.bitw.fls(1n+m, w), bitw.ffs_fls_k(1n+m, w, k, e), bitw.fls_le(1n+m, w))