Thm* Auto:Automata(Alph;St). Fin(Alph) Fin(St) (s:St. Dec(w:Alph*. (Result(Auto)w) = s)) reach_dec

In prior sections: core int 1 bool 1 int 2 finite sets list 3 autom