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* A1:Automata(Alph;S1), A2:Automata(Alph;S2). LangOf(A1) = LangOf(A2) x,y:Alph*//(x LangOf(A1)-induced Equiv y) = x,y:Alph*//(x LangOf(A2)-induced Equiv y) lang_eq_imp_quo_eq

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

Thm* Auto:Automata(Alph;St), l:Alph*. (Result(MinAuto(Auto))l) = l x,y:Alph*//(x LangOf(Auto)-induced Equiv y) min_auto_comp

Thm* Auto:Automata(Alph;St), l:x,y:Alph*//(x LangOf(Auto)-induced Equiv y). Auto(l) quo_list_accept

Thm* Auto:Automata(Alph;St). LangOf(Auto) = LangOf(MinAuto(Auto)) min_auto_sound

Thm* Alph,St:Type, Auto:Automata(Alph;St). MinAuto(Auto) Automata(Alph;x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) min_auto_wf

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