PROOF.nfa.dead: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 2958-2980 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=2958&end_line=2980

import Base
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

# no position active: nothing accepted
def nfa.dead(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +s: List<&2, U32>, +e: {G.AaGNfa.alive(bs) == False{} : Bool}) -> {G.AaGNfa.sem(seq, bs, s) == False{} : Bool}:
  match seq:
    case Nil{}:
      match bs:
        case Nil{}:
          {==}
        case Con{b, rest}:
          match b:
            case True{}:
              b.absurd_tf(Bool, G.AaGNfa.sem(Nil{}, Con{True{}, rest}, s), False{}, e)
            case False{}:
              {==}
    case Con{tok, r}:
      match bs:
        case Nil{}:
          nfa.dead(r, Nil{}, s, {==})
        case Con{b, rest}:
          match b:
            case True{}:
              b.absurd_tf(Bool, G.AaGNfa.sem(Con{tok, r}, Con{True{}, rest}, s), False{}, e)
            case False{}:
              nfa.dead(r, rest, s, e)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.absurd_tf
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.alive
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.sem
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok