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

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

def glob.alts_ref(+alts: List<&2, List<&2, G.AaGTok>>, +s: List<&2, U32>) -> {G.AaGlob.matches_ref.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.matches(a, s), G.AaGlob.matches_ref.go(t, s)) == Bool.or(_, G.AaGlob.model.go(t, s)) : Bool}
      %glob.alts_ref(t, s) : {Bool.or(G.AaGSeq.matches(a, s), G.AaGlob.matches_ref.go(t, s)) == Bool.or(G.AaGSeq.matches(a, s), _) : Bool}
      {==}

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