def bitseq.next_hit

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

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

596def bitseq.next_hit(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>, l: {Nat.is_lt(M.bitseq.next(size, start, want, bs), size) == True{} : Bool}) -> {M.bitseq.at(bs, M.bitseq.next(size, start, want, bs)) == want : Bool}:
597  match size:
598    case 0n:
599      Empty.absurd({M.bitseq.at(bs, 0n) == want : Bool}, absurd.ft(l))
600    case 1n+ +s:
601      match start want bs:
602        case 1n+st w Nil{}:
603          bitseq.next_hit(s, st, w, Nil{}, l)
604        case 1n+st w Con{h, t}:
605          bitseq.next_hit(s, st, w, t, l)
606        case 0n False{} Nil{}:
607          {==}
608        case 0n True{} Nil{}:
609          Empty.absurd({False{} == True{} : Bool}, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(s, s), True{}, Equal.sym(Bool, Nat.is_lt(s, s), False{}, nat.lt_irrefl(s)), l)))
610        case 0n True{} Con{True{}, t}:
611          {==}
612        case 0n False{} Con{False{}, t}:
613          {==}
614        case 0n True{} Con{False{}, t}:
615          bitseq.next_hit(s, 0n, True{}, t, l)
616        case 0n False{} Con{True{}, t}:
617          bitseq.next_hit(s, 0n, False{}, t, l)