def bitseq.next_le

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

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

573def bitseq.next_le(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>) -> {Nat.is_le(M.bitseq.next(size, start, want, bs), size) == True{} : Bool}:
574  match size:
575    case 0n:
576      {==}
577    case 1n+ +s:
578      match start want bs:
579        case 1n+st w Nil{}:
580          bitseq.next_le(s, st, w, Nil{})
581        case 1n+st w Con{h, t}:
582          bitseq.next_le(s, st, w, t)
583        case 0n False{} Nil{}:
584          {==}
585        case 0n True{} Nil{}:
586          nat.le_refl(s)
587        case 0n True{} Con{True{}, t}:
588          {==}
589        case 0n False{} Con{False{}, t}:
590          {==}
591        case 0n True{} Con{False{}, t}:
592          bitseq.next_le(s, 0n, True{}, t)
593        case 0n False{} Con{True{}, t}:
594          bitseq.next_le(s, 0n, False{}, t)