law wit_next

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

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

377# an answer below the size, and a j with start <= j < answer
378law wit_next:
379  {(Nat.is_lt(M.bitmap.next_set([0, 8], 64n, 3n), 64n), Nat.is_le(3n, 10n), Nat.is_lt(10n, M.bitmap.next_set([0, 8], 64n, 3n)), Nat.is_lt(M.bitmap.next_clear([4294967295, 1], 64n, 3n), 64n), Nat.is_lt(10n, M.bitmap.next_clear([4294967295, 1], 64n, 3n))) == (True{}, True{}, True{}, True{}, True{}) : Bool & Bool & Bool & Bool & Bool}