1. Alph :

2. St :

3. Auto : Automata(Alph;St)

4. Fin(St)

5. Fin(Alph)

RL:St List. s:St. (w:Alph List. Auto(w) = s) mem_f(St;s;RL)

(InstLemma `reach_aux` [Alph;<St, a:Alph. s:St. Auto s a>;I(Auto)] ...a)

1. <St, a:Alph. s:St. Auto s a> ActionSet(Alph)

2. <St, a:Alph. s:St. Auto s a>.car

3. Fin(<St, a:Alph. s:St. Auto s a>.car)

4. RL:St List. s:St. (w:Alph List. Auto(w) = s) mem_f(St;s;RL)