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

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

# only the whole sequence active: what the backtracking matcher accepts
def nfa.start(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGNfa.sem(seq, G.AaGNfa.start(seq), s) == G.AaGSeq.matches(seq, s) : Bool}:
  match seq:
    case Nil{}:
      {==}
    case Con{tok, r}:
      %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.falses(r), s), False{}, nfa.dead(r, G.AaGNfa.falses(r), s, nfa.falses_dead(r))) : {Bool.or(G.AaGSeq.matches(Con{tok, r}, s), _) == G.AaGSeq.matches(Con{tok, r}, s) : Bool}
      b.or_false_r(G.AaGSeq.matches(Con{tok, r}, s))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.or_false_r
  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.falses_dead
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.falses
  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=AaGNfa.start
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.matches
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok