def glob.alts

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

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

3020def 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}:
3021  match alts:
3022    case Nil{}:
3023      {==}
3024    case Con{a, t}:
3025      %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}
3026      %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}
3027      %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}
3028      {==}