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