Thm* Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S). Fin(Alph) Fin(S) Con(A) (S ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) LangOf(Auto) = LangOf(A) A MinAuto(Auto) any_iso_min_auto

Thm* Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S). Fin(Alph) Fin(St) LangOf(Auto) = LangOf(A) Con(A) |S| |x,y:Alph*//(x LangOf(Auto)-induced Equiv y)| any_ge_min_auto

Thm* Auto:Automata(Alph;St). Fin(Alph) & Fin(St) Con(MinAuto(Auto)) min_auto_con

Thm* Auto:Automata(Alph;St). Con(Auto) & (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & Fin(Alph) & Fin(St) Auto A(l.Auto(l)) min_is_unique

Thm* Auto:Automata(Alph;St), c:(StAlph*). (q:St. (Result(Auto)c(q)) = q) & Fin(Alph) & Fin(St) & (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) Inj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c) homo_is_inj

Thm* f:(AB). (A ~ B) & Fin(B) Surj(A; B; f) Inj(A; B; f) surj_is_inj_gen

Thm* Auto:Automata(Alph;St), c:(StAlph*). (q:St. (Result(Auto)c(q)) = q) & Fin(Alph) & Fin(St) Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c) homo_is_surj

Thm* E:(Alph*Alph*Prop). Fin(Alph) & (EquivRel x,y:Alph*. x E y) & (x,y:Alph*. Dec(x E y)) (h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))) fin_alph_list_quo

Thm* Auto:Automata(Alph;St). Fin(Alph) & Fin(St) (x,y:Alph*. Dec(x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) Rl_quo_is_decidable

Thm* Auto:Automata(Alph;St). Fin(Alph) & Fin(St) Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) mn_13

In prior sections: finite sets list 3 autom exponent det automata myhill nerode