def bitw.first_set_lowest

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

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

474def bitw.first_set_lowest(+n: Nat, +w: Word(n), +k: Nat, +j: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}, l: {Nat.is_lt(j, k) == True{} : Bool}) -> {A.bitw.test(n, w, j) == False{} : Bool}:
475  %l : {Bool.and(_, A.bitw.test(n, w, j)) == False{} : Bool}
476  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {Bool.and(bitw.below(j, _), A.bitw.test(n, w, j)) == False{} : Bool}
477  bitw.ffs_low(n, w, j)