Thm* Auto:Automata(Alph;St), g:((x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) , c:(StAlph*). (q:St. (Result(Auto)c(q)) = q) c(InitialState(Auto)) = nil x,y:Alph*//(x LangOf(Auto)-induced Equiv y) homo_init

In prior sections: det automata