law next_set_at_least

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

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

177law next_set_at_least:
178  for words: List<&2, U32>
179  for size: Nat
180  for start: Nat
181  for l: {Nat.is_lt(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
182  {Nat.is_le(start, M.bitmap.next_set(words, size, start)) == True{} : Bool}