law ctz_clz

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

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

99law ctz_clz:
100  for x: U32
101  for k: Nat
102  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
103  {Nat.is_le(Nat.add(A.bits32.ctz(x), A.bits32.clz(x)), 31n) == True{} : Bool}