law first_set64_is_set

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

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

111law first_set64_is_set:
112  for a: W.W64
113  for k: Nat
114  for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
115  {A.bits64.test(a, k) == True{} : Bool}