PROOF.bitw.clz_last_set: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
Lines 503-505 of bend-osdev-algo@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&start_line=503&end_line=505

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

def 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}:
  %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}
  nat.sub_add(m, k, bitw.last_le(m, w, k, e))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.index_some
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.last_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bitw.clz
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bitw.fls
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bitw.index