def bitseq.next_miss

bend-osdev-algo@0.1.0.0 · PROOF.bend:645

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

645def 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}:
646  match size:
647    case 0n:
648      bitseq.lt0(j, {M.bitseq.at(bs, j) == Bool.not(want) : Bool}, m)
649    case 1n+ +s:
650      match start want bs j:
651        case 1n+st w Nil{} 0n:
652          Empty.absurd({False{} == Bool.not(w) : Bool}, absurd.ft(l))
653        case 1n+st w Nil{} 1n+jp:
654          bitseq.next_miss(s, st, w, Nil{}, jp, l, m)
655        case 1n+st w Con{h, t} 0n:
656          Empty.absurd({h == Bool.not(w) : Bool}, absurd.ft(l))
657        case 1n+st w Con{h, t} 1n+jp:
658          bitseq.next_miss(s, st, w, t, jp, l, m)
659        case 0n False{} Nil{} +jj:
660          bitseq.lt0(jj, {M.bitseq.at(Nil{}, jj) == True{} : Bool}, m)
661        case 0n True{} Nil{} jj:
662          {==}
663        case 0n True{} Con{True{}, t} +jj:
664          bitseq.lt0(jj, {M.bitseq.at(Con{True{}, t}, jj) == False{} : Bool}, m)
665        case 0n False{} Con{False{}, t} +jj:
666          bitseq.lt0(jj, {M.bitseq.at(Con{False{}, t}, jj) == True{} : Bool}, m)
667        case 0n True{} Con{False{}, t} 0n:
668          {==}
669        case 0n True{} Con{False{}, t} 1n+ +jp:
670          bitseq.next_miss(s, 0n, True{}, t, jp, nat.le_zero(jp), m)
671        case 0n False{} Con{True{}, t} 0n:
672          {==}
673        case 0n False{} Con{True{}, t} 1n+ +jp:
674          bitseq.next_miss(s, 0n, False{}, t, jp, nat.le_zero(jp), m)