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
f:(A
B), g:(BA). InvFuns(A; B; f; g)
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).
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
In prior sections: fun 1 finite sets exponent relation autom myhill nerode