At: reach dec 1 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. Fin(St)
6. s: St
7. RL: St*
8. 
s:St. (
w:Alph*. (Result(Auto)w) = s) 
mem_f(St;s;RL)
Dec(mem_f(St;s;RL))
By: BackThru
Thm* s:S, l:S*. Fin(S) 
Dec(mem_f(S;s;l))
Generated subgoals:None
About:
