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
s:St. 
l:Alph*. (Result(A)l) = s
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
In prior sections: automata 4