Selected Objects

def	auto_action	Action(Auto) == < St,a,s. Auto(s,a) >
THM	auto_maction	Auto:Automata(Alph;St), l:Alph*. (Result(Auto)l) = (Action(Auto):lInitialState(Auto))
THM	empty_lang_dec	Auto:Automata(Alph;St). Fin(Alph) & Fin(St) Dec(l:Alph*. LangOf(Auto)(l))
THM	auto1_lang	n:2. n = 0 (l:2*. LangOf(Auto)(l))
THM	auto2_lang	n:2. n = 0 (l:2*. LangOf(Auto)(l))
THM	auto3_lang	n:2. n = 0 (l:3*. LangOf(Auto)(l))