law ctz_clz64

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

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

156law ctz_clz64:
157  for a: W.W64
158  for k: Nat
159  for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
160  {Nat.is_le(Nat.add(A.bits64.ctz(a), A.bits64.clz(a)), 63n) == True{} : Bool}