Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):l
InitialState(Auto))
auto_maction
s) == if null(L)
s else S.act(hd(L),(S:tl(L)s)) fi (recursive)
Thm* Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):lInitialState(Auto))
auto_maction
In prior sections: action sets det automata myhill nerode