law clz_last_set

bend-osdev-algo@0.1.0.0 · LAWS.bend:85

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

85law clz_last_set:
86  for x: U32
87  for k: Nat
88  for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
89  {Nat.add(A.bits32.clz(x), k) == 31n : Nat}