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

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

Thm* Alph:Type, L:LangOver(Alph), g:((x,y:Alph*//(x L-induced Equiv y))). A(g) Automata(Alph;x,y:Alph*//(x L-induced Equiv y)) lang_auto_wf

In prior sections: languages myhill nerode