LAWS.wit_next: law of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/LAWS.bend as LAWS
Lines 377-379 of bend-osdev-algo@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&start_line=377&end_line=379

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

# an answer below the size, and a j with start <= j < answer
law wit_next:
  {(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}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bitmap.bend&name=bitmap.next_clear
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bitmap.bend&name=bitmap.next_set