~/jendhub

def nfa.thm

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

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

3017def nfa.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.run(seq, s) == G.AaGSeq.matches(seq, s) : Bool}:
3018  Equal.trans(Bool, G.AaGNfa.run(s, True{}, seq, G.AaGNfa.start(seq)), G.AaGNfa.sem(seq, G.AaGNfa.start(seq), s), G.AaGSeq.matches(seq, s), nfa.run(s, True{}, seq, G.AaGNfa.start(seq), nfa.start_alive(seq)), nfa.start(seq, s))

Uses (13)

Used by (2)