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