law last_set_highest

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

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

66law last_set_highest:
67  for x: U32
68  for k: Nat
69  for j: Nat
70  for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
71  for l: {Nat.is_lt(k, j) == True{} : Bool}
72  {A.bits32.test(x, j) == False{} : Bool}