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* 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

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

Thm* A1:Automata(Alph;S1), A2:Automata(Alph;S2). Con(A1) & Con(A2) A1 A2 |S1| |S2| refine_ge

Thm* A1:Automata(Alph;S1), A2:Automata(Alph;S2). A1 A2 A2 A1 auto_iso_sym

In prior sections: det automata myhill nerode