Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) 
Dec(
l:Alph*. LangOf(Auto)(l))
empty_lang_dec
AlphStates)
States(States
)
Thm* Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) Dec(l:Alph*. LangOf(Auto)(l))
empty_lang_dec
Thm* Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):l
InitialState(Auto))
auto_maction
In prior sections: det automata myhill nerode automata 4 automata 5 automata 6