law next_clear_le_size

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

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

193law next_clear_le_size:
194  for words: List<&2, U32>
195  for size: Nat
196  for start: Nat
197  {Nat.is_le(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}