def bitw.ffs_fls_k

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

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

519def bitw.ffs_fls_k(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(1n+k, A.bitw.fls(n, w)) == True{} : Bool}:
520  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {Nat.is_le(_, A.bitw.fls(n, w)) == True{} : Bool}
521  bitw.ffs_le_fls(n, w)