Thm* Auto:Automata(Alph;St). Fin(Alph) & Fin(St) Dec(l:Alph*. LangOf(Auto)(l)) empty_lang_dec

In prior sections: core int 1 bool 1 rel 1 choice 1 int 2 finite sets list 3 autom exponent quot 1 relation autom det automata myhill nerode automata 5