law next_set_none_before

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

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

184law next_set_none_before:
185  for words: List<&2, U32>
186  for size: Nat
187  for start: Nat
188  for j: Nat
189  for l: {Nat.is_le(start, j) == True{} : Bool}
190  for m: {Nat.is_lt(j, M.bitmap.next_set(words, size, start)) == True{} : Bool}
191  {M.bitmap.test(words, j) == False{} : Bool}