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
InitialState(DA) else DA((Result(DA)tl(l)),hd(l)) fi
(recursive)
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
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
Thm* L:LangOver(Alph), g:((x,y:Alph*//(x L-induced Equiv y))), l:Alph*.
(Result(A(g))l) = l x,y:Alph*//(x L-induced Equiv y)
lang_auto_compute
In prior sections: det automata