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.Auto(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). 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). LangOf(Auto) = LangOf(MinAuto(Auto))
min_auto_sound