Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(Alph)

  5. Fin(St)

  6. s : St

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

Conclusion:

Dec(w:Alph List. Auto(w) = s)

Applied Tactic: (D (-1) THEN RWH (HypC (-1)) 0 ...a)
Generated subgoals:

1. Dec(mem_f(St;s;RL))