Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph,St:. Auto:Automata(Alph;St). g:x,y:(Alph List)//(x Rl y) . Auto A(g)

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) . Auto A(g)