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
|T| == 
f:(S
T). Surj(S; T; f)
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
In prior sections: automata 4