Thm* Auto:Automata(Alph;St), g:((x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) , c:(StAlph*). (q:St. (Result(Auto)c(q)) = q) (q:St, a:Alph. c(Auto(q,a)) = A(g)(c(q),a) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) homo_step

Thm* Auto:Automata(Alph;St), g:((x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) , c:(StAlph*). (q:St. (Result(Auto)c(q)) = q) c(InitialState(Auto)) = nil x,y:Alph*//(x LangOf(Auto)-induced Equiv y) homo_init

Thm* Auto:Automata(Alph;St) , g:((x,y:Alph*//(x LangOf(Auto)-induced Equiv y))). Auto A(g) lang_auto_is_min

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: myhill nerode