PROOF.nfa.run: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 2982-2992 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=2982&end_line=2992

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

# the run: the positions accept the path (a: whether some position is active)
def nfa.run(+s: List<&2, U32>, +a: Bool, +seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +e: {G.AaGNfa.alive(bs) == a : Bool}) -> {G.AaGNfa.run(s, a, seq, bs) == G.AaGNfa.sem(seq, bs, s) : Bool}:
  match s:
    case Nil{}:
      {==}
    case Con{h, t}:
      match a:
        case False{}:
          Equal.sym(Bool, G.AaGNfa.sem(seq, bs, Con{h, t}), False{}, nfa.dead(seq, bs, Con{h, t}, e))
        case True{}:
          Equal.trans(Bool, G.AaGNfa.run(t, G.AaGNfa.alive(G.AaGNfa.next(seq, bs, False{}, False{}, h)), seq, G.AaGNfa.next(seq, bs, False{}, False{}, h)), G.AaGNfa.sem(seq, G.AaGNfa.next(seq, bs, False{}, False{}, h), t), G.AaGNfa.sem(seq, bs, Con{h, t}), nfa.run(t, G.AaGNfa.alive(G.AaGNfa.next(seq, bs, False{}, False{}, h)), seq, G.AaGNfa.next(seq, bs, False{}, False{}, h), {==}), nfa.step(seq, bs, False{}, False{}, h, t))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=nfa.dead
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.step
  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.next
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.run
  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