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

In prior sections: det automata