def glob.alts_ref

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3030

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

3030def 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}:
3031  match alts:
3032    case Nil{}:
3033      {==}
3034    case Con{a, t}:
3035      %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}
3036      %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}
3037      {==}