PROOF.nfa.step: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 2934-2956 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=2934&end_line=2956

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

# one byte: the positions after it accept t exactly when, before it, the
# positions (with the carried ones) accept h then t
def nfa.step(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +cin: Bool, +ain: Bool, +h: U32, +t: List<&2, U32>) -> {G.AaGNfa.sem(seq, G.AaGNfa.next(seq, bs, cin, ain, h), t) == Bool.or(Bool.and(ain, G.AaGSeq.matches(seq, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(seq, Con{h, t})), G.AaGNfa.sem(seq, bs, Con{h, t}))) : Bool}:
  match seq:
    case Nil{}:
      nfa.taut_nil(ain, X.AaText.is_nil(t), cin, G.AaGNfa.hd(bs))
    case Con{tok, r}:
      match tok:
        case G.AaGChar{c}:
          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_eq(h, c)), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_eq(h, c)), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_eq(h, c)), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), ain), G.AaGSeq.matches(Con{G.AaGChar{c}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGChar{c}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGChar{c}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGChar{c}, r}, bs, Con{h, t}))) : Bool}
          nfa.taut_adv(G.AaGNfa.hd(bs), cin, ain, U32.is_eq(h, c), G.AaGSeq.matches(Con{G.AaGChar{c}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
        case G.AaGAny{}:
          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), ain), G.AaGSeq.matches(Con{G.AaGAny{}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGAny{}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGAny{}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGAny{}, r}, bs, Con{h, t}))) : Bool}
          nfa.taut_adv(G.AaGNfa.hd(bs), cin, ain, U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGAny{}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
        case G.AaGClass{n, rs}:
          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), G.AaGClass.has(n, rs, h)), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), G.AaGClass.has(n, rs, h)), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), G.AaGClass.has(n, rs, h)), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), ain), G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGClass{n, rs}, r}, bs, Con{h, t}))) : Bool}
          nfa.taut_adv(G.AaGNfa.hd(bs), cin, ain, G.AaGClass.has(n, rs, h), G.AaGSeq.matches(Con{G.AaGClass{n, rs}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
        case G.AaGStar{}:
          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), U32.is_ne(h, 47)), ain), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGStar{}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGStar{}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGStar{}, r}, bs, Con{h, t}))) : Bool}
          nfa.taut_star(G.AaGNfa.hd(bs), cin, ain, U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))
        case G.AaGStar2{}:
          %Equal.sym(Bool, G.AaGNfa.sem(r, G.AaGNfa.next(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h), t), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), G.AaGSeq.matches(r, t)), Bool.or(Bool.and(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), G.AaGSeq.matches(r, Con{h, t})), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))), nfa.step(r, G.AaGNfa.tl(bs), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), False{}), h, t)) : {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(G.AaGNfa.hd(bs), cin), True{}), ain), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)), _) == Bool.or(Bool.and(ain, G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(Con{G.AaGStar2{}, r}, Con{h, t})), G.AaGNfa.sem(Con{G.AaGStar2{}, r}, bs, Con{h, t}))) : Bool}
          nfa.taut_star2(G.AaGNfa.hd(bs), cin, ain, G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t), G.AaGSeq.matches(r, t), G.AaGSeq.matches(r, Con{h, t}), G.AaGNfa.sem(r, G.AaGNfa.tl(bs), Con{h, t}))

Uses (20):
  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=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=nfa.taut_adv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_nil
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_star
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_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=AaGNfa.hd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.next
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.sem
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGNfa.tl
  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/text.bend&name=AaText.is_nil