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

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

# the matcher agrees with the list model: induction on the sequence, and on
# the path under a star
def glob.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool}:
  match seq:
    case Nil{}:
      match s:
        case Nil{}:
          {==}
        case Con{h, t}:
          {==}
    case Con{tok, r}:
      match tok:
        case G.AaGChar{c}:
          match s:
            case Nil{}:
              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
            case Con{h, t}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == _ : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_eq(h, c), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_char(c, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
              %glob.thm(r, t) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
              {==}
        case G.AaGAny{}:
          match s:
            case Nil{}:
              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
            case Con{h, t}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == _ : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_any(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
              %glob.thm(r, t) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
              {==}
        case G.AaGClass{n, rs}:
          match s:
            case Nil{}:
              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
            case Con{h, t}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == _ : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_class(n, rs, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
              %glob.thm(r, t) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
              {==}
        case G.AaGStar{}:
          match s:
            case Nil{}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
              glob.thm(r, Nil{})
            case Con{h, t}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == _ : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_star(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
              %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
              %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), _)) : Bool}
              {==}
        case G.AaGStar2{}:
          match s:
            case Nil{}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
              glob.thm(r, Nil{})
            case Con{h, t}:
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == _ : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), gr_star2(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
              %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : Bool}
              %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), _) : Bool}
              {==}

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ne
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_char
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_class
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_star
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_star2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fa_app
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_cuts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_char
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_class
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_star
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_star2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGClass.has
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.all
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.empty_first
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.grow
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.fits_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.len
  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=AaGSeq.model
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok