Thm* L:LangOver(Alph), g:((x,y:Alph*//(x L-induced Equiv y))). (l:Alph*. L(l) g(l)) LangOf(A(g)) = L lang_auto_lem

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 finite sets list 3 autom exponent rel 1 quot 1 relation autom languages det automata myhill nerode