Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St).
Con(Auto) 
1-1-Corresp(St;x,y:(Alph List)//(x Rl y)) Fin(Alph) Fin(St)
Auto 
A(
l.Auto(l)
)
Applied Tactic: D 0 THENA Auto THEN D 0 THENA Auto THEN D 0 THENA Auto
Generated subgoals:1. Con(Auto) 1-1-Corresp(St;x,y:(Alph List)//(x Rl y)) Fin(Alph) Fin(St) Auto A(l.Auto(l))