PROOF.glob.alts: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3020-3028 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=3020&end_line=3028

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

def glob.alts(+alts: List<&2, List<&2, G.AaGTok>>, +s: List<&2, U32>) -> {G.AaGlob.matches.go(alts, s) == G.AaGlob.model.go(alts, s) : Bool}:
  match alts:
    case Nil{}:
      {==}
    case Con{a, t}:
      %glob.thm(a, s) : {Bool.or(G.AaGSeq.run(a, s), G.AaGlob.matches.go(t, s)) == Bool.or(_, G.AaGlob.model.go(t, s)) : Bool}
      %nfa.thm(a, s) : {Bool.or(G.AaGSeq.run(a, s), G.AaGlob.matches.go(t, s)) == Bool.or(_, G.AaGlob.model.go(t, s)) : Bool}
      %glob.alts(t, s) : {Bool.or(G.AaGSeq.run(a, s), G.AaGlob.matches.go(t, s)) == Bool.or(G.AaGSeq.run(a, s), _) : Bool}
      {==}

Uses (10):
  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=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=glob.thm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.thm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.run
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGlob.matches.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGlob.model.go