def bitw.ctz_first_set

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

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

494def bitw.ctz_first_set(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {A.bitw.ctz(n, w) == k : Nat}:
495  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {A.bitw.ctz(n, w) == bitw.ctz_spec(n, _) : Nat}
496  bitw.ctz_ffs(n, w)