def bitw.last_set_highest

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

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

486def bitw.last_set_highest(+n: Nat, +w: Word(n), +k: Nat, +j: Nat, e: {A.bitw.index(A.bitw.fls(n, w)) == Some{k} : Maybe<&2, Nat>}, l: {Nat.is_lt(k, j) == True{} : Bool}) -> {A.bitw.test(n, w, j) == False{} : Bool}:
487  %l : {Bool.and(_, A.bitw.test(n, w, j)) == False{} : Bool}
488  %bitw.index_some(A.bitw.fls(n, w), k, e) : {Bool.and(bitw.above(j, _), A.bitw.test(n, w, j)) == False{} : Bool}
489  bitw.fls_high(n, w, j)