def bitw.clz_last_set

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

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

503def bitw.clz_last_set(+m: Nat, +w: Word(1n+m), +k: Nat, +e: {A.bitw.index(A.bitw.fls(1n+m, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.add(A.bitw.clz(1n+m, w), k) == m : Nat}:
504  %Equal.sym(Nat, A.bitw.fls(1n+m, w), 1n+k, bitw.index_some(A.bitw.fls(1n+m, w), k, e)) : {Nat.add(Nat.sub(1n+m, _), k) == m : Nat}
505  nat.sub_add(m, k, bitw.last_le(m, w, k, e))