law next_set_is_set

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

import Base
import bend-osdev-algo@0.1.0.0/bitmap.bend as M

170law next_set_is_set:
171  for words: List<&2, U32>
172  for size: Nat
173  for start: Nat
174  for l: {Nat.is_lt(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
175  {M.bitmap.test(words, M.bitmap.next_set(words, size, start)) == True{} : Bool}