n:
2. n = 0 
(l:3*. LangOf(Auto
)(l)) auto3_lang
DA(l)
Thm* n:2. n = 0 (l:3*. LangOf(Auto)(l)) auto3_lang
Thm* n:2. n = 0 (l:2*. LangOf(Auto
)(l)) auto2_lang
Thm* n:2. n = 0 (l:2*. LangOf(Auto
)(l)) auto1_lang
Thm* 
Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) 
Dec(l:Alph*. LangOf(Auto)(l))
empty_lang_dec
In prior sections: myhill nerode automata 4 automata 5 automata 6