law next_clear_at_least

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

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

206law next_clear_at_least:
207  for words: List<&2, U32>
208  for size: Nat
209  for start: Nat
210  for l: {Nat.is_lt(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
211  {Nat.is_le(start, M.bitmap.next_clear(words, size, start)) == True{} : Bool}