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
l:Alph*. L(l) M(l)
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* A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) LangOf(A1) = LangOf(A2) A1 
A2 & A2 A1 A1 
A2
refine_iso
In prior sections: languages myhill nerode