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
l:Alph*. L(l) 
M(l)
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). LangOf(Auto) = LangOf(MinAuto(Auto))
min_auto_sound
In prior sections: languages myhill nerode automata 4