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
s,a. a.s),nil,g >
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