law clz64_last_set

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

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

150law clz64_last_set:
151  for a: W.W64
152  for k: Nat
153  for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
154  {Nat.add(A.bits64.clz(a), k) == 63n : Nat}