PROOF.bitseq.next_miss: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
Lines 645-674 of bend-osdev-algo@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&start_line=645&end_line=674

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

def bitseq.next_miss(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>, j: Nat, l: {Nat.is_le(start, j) == True{} : Bool}, m: {Nat.is_lt(j, M.bitseq.next(size, start, want, bs)) == True{} : Bool}) -> {M.bitseq.at(bs, j) == Bool.not(want) : Bool}:
  match size:
    case 0n:
      bitseq.lt0(j, {M.bitseq.at(bs, j) == Bool.not(want) : Bool}, m)
    case 1n+ +s:
      match start want bs j:
        case 1n+st w Nil{} 0n:
          Empty.absurd({False{} == Bool.not(w) : Bool}, absurd.ft(l))
        case 1n+st w Nil{} 1n+jp:
          bitseq.next_miss(s, st, w, Nil{}, jp, l, m)
        case 1n+st w Con{h, t} 0n:
          Empty.absurd({h == Bool.not(w) : Bool}, absurd.ft(l))
        case 1n+st w Con{h, t} 1n+jp:
          bitseq.next_miss(s, st, w, t, jp, l, m)
        case 0n False{} Nil{} +jj:
          bitseq.lt0(jj, {M.bitseq.at(Nil{}, jj) == True{} : Bool}, m)
        case 0n True{} Nil{} jj:
          {==}
        case 0n True{} Con{True{}, t} +jj:
          bitseq.lt0(jj, {M.bitseq.at(Con{True{}, t}, jj) == False{} : Bool}, m)
        case 0n False{} Con{False{}, t} +jj:
          bitseq.lt0(jj, {M.bitseq.at(Con{False{}, t}, jj) == True{} : Bool}, m)
        case 0n True{} Con{False{}, t} 0n:
          {==}
        case 0n True{} Con{False{}, t} 1n+ +jp:
          bitseq.next_miss(s, 0n, True{}, t, jp, nat.le_zero(jp), m)
        case 0n False{} Con{True{}, t} 0n:
          {==}
        case 0n False{} Con{True{}, t} 1n+ +jp:
          bitseq.next_miss(s, 0n, False{}, t, jp, nat.le_zero(jp), m)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitseq.lt0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.le_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bitmap.bend&name=bitseq.at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bitmap.bend&name=bitseq.next