law next_clear_is_clear

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

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

199law next_clear_is_clear:
200  for words: List<&2, U32>
201  for size: Nat
202  for start: Nat
203  for l: {Nat.is_lt(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
204  {M.bitmap.test(words, M.bitmap.next_clear(words, size, start)) == False{} : Bool}