def bitseq.next_ge

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

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

619def bitseq.next_ge(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>, l: {Nat.is_lt(M.bitseq.next(size, start, want, bs), size) == True{} : Bool}) -> {Nat.is_le(start, M.bitseq.next(size, start, want, bs)) == True{} : Bool}:
620  match size:
621    case 0n:
622      Empty.absurd({Nat.is_le(start, 0n) == True{} : Bool}, absurd.ft(l))
623    case 1n+ +s:
624      match start want bs:
625        case 1n+st w Nil{}:
626          bitseq.next_ge(s, st, w, Nil{}, l)
627        case 1n+st w Con{h, t}:
628          bitseq.next_ge(s, st, w, t, l)
629        case 0n False{} Nil{}:
630          {==}
631        case 0n True{} Nil{}:
632          {==}
633        case 0n True{} Con{True{}, t}:
634          {==}
635        case 0n False{} Con{False{}, t}:
636          {==}
637        case 0n True{} Con{False{}, t}:
638          {==}
639        case 0n False{} Con{True{}, t}:
640          {==}