Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) 
Dec(
l:Alph*. LangOf(Auto)(l))
empty_lang_dec
n:
, f:(n
s). Bij(n; s; f)
Thm* Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) Dec(l:Alph*. LangOf(Auto)(l))
empty_lang_dec
In prior sections: finite sets list 3 autom exponent det automata myhill nerode automata 5