law next_clear_none_before

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

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

213law next_clear_none_before:
214  for words: List<&2, U32>
215  for size: Nat
216  for start: Nat
217  for j: Nat
218  for l: {Nat.is_le(start, j) == True{} : Bool}
219  for m: {Nat.is_lt(j, M.bitmap.next_clear(words, size, start)) == True{} : Bool}
220  {M.bitmap.test(words, j) == True{} : Bool}