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
b == if b
True else False fi
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: bool 1 list 1 finite sets list 3 autom exponent quot 1 myhill nerode