automata 7 Sections AutomataTheory Doc

Def InitialState(a) == 1of(2of(a))

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

In prior sections: det automata automata 4