Thm* Auto:Automata(Alph;St), l:Alph*. ( < St,l,s. Auto(s,l) > :lInitialState(Auto)) = (Result(Auto)l) action_auto
Auto:Automata(Alph;St), l:Alph*.
( < St,
l,s. 
Auto(s,l) > :l
InitialState(Auto)) = (Result(Auto)l)
action_auto
Auto:Automata(Alph;St), l:Alph*.
( < St,l,s. Auto(s,l) > :lInitialState(Auto)) = (Result(Auto)l)
action_auto