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) 
(q:St. a:Alph. c (
Auto q a) = A(g) (c q) a)
Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto THEN D 0 THENW Auto
Generated subgoals:1. g:x,y:(Alph List)//(x Rl y) . c:St Alph List.
(q:St. Auto(c q) = q) (q:St. a:Alph. c (Auto q a) = A(g) (c q) a)