law last_set64_highest

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

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

136law last_set64_highest:
137  for a: W.W64
138  for k: Nat
139  for j: Nat
140  for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
141  for l: {Nat.is_lt(k, j) == True{} : Bool}
142  {A.bits64.test(a, j) == False{} : Bool}