Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). g:x,y:(Alph List)//(x Rl y) 
. c:St Alph List.
(q:St. Auto(c q) = q) 
c I(Auto) = []
Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto THEN D 0 THENA Auto
Generated subgoals:1. g:x,y:(Alph List)//(x Rl y) . c:St Alph List. (q:St. Auto(c q) = q) c I(Auto) = []