Auto:Automata(Alph;St), l:Alph*.
(Result(MinAuto(Auto))l) = l 
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
min_auto_comp
InitialState(DA) else 
DA((Result(DA)tl(l)),hd(l)) fi
(recursive)
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), c:(St
Alph*).
(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* Auto:Automata(Alph;St), c:(StAlph*).
(q:St. (Result(Auto)c(q)) = q) & Fin(Alph) & Fin(St)
Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c)
homo_is_surj
In prior sections: det automata automata 4