At: mn 12 1 2 2 1 2 1 2 1 1 2 1 1
1. Alph: Type
2. L: LangOver(Alph)
3. Fin(Alph)
4. St: Type
5. Auto: Automata(Alph;St)
6. Fin(St)
7. L = LangOf(Auto)
8. EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)
9. s: St
Dec(
t:Alph*. (Result(Auto)t) = s)
By: Inst
Thm* 
Auto:Automata(Alph;St).
Fin(Alph) 
Fin(St) (s:St. Dec(w:Alph*. (Result(Auto)w) = s))
[Alph;St;Auto]
Generated subgoals:None
About:
