Thm* Auto:Automata(Alph;St), l:Alph*. (Result(Auto)l) = (Action(Auto):lInitialState(Auto)) auto_maction
Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):l
InitialState(Auto))
auto_maction
a,s. 
Auto(s,a) >
Auto:Automata(Alph;St), l:Alph*.
(Result(Auto)l) = (Action(Auto):lInitialState(Auto))
auto_maction