Auto:Automata(Alph;St), l:x,y:Alph*//(x LangOf(Auto)-induced Equiv y).
Auto(l)
quo_list_accept
== FinalState(DA)(Result(DA)l)
Thm* Auto:Automata(Alph;St), l:x,y:Alph*//(x LangOf(Auto)-induced Equiv y).
Auto(l)
quo_list_accept
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: det automata