Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):l
InitialState(Auto))
auto_maction
InitialState(DA) else 
DA((Result(DA)tl(l)),hd(l)) fi
(recursive)
Thm* Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):lInitialState(Auto))
auto_maction
In prior sections: det automata automata 4 automata 5