Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. L:L(Alph). g:x,y:(Alph List)//(x Rl y) 
.
A(g) 
Automata(Alph;x,y:(Alph List)//(x Rl y))
Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto
Generated subgoals:1. g:x,y:(Alph List)//(x Rl y) . A(g) Automata(Alph;x,y:(Alph List)//(x Rl y))