law ctz_first_set

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

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

79law ctz_first_set:
80  for x: U32
81  for k: Nat
82  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
83  {A.bits32.ctz(x) == k : Nat}