Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). S:. A:Automata(Alph;S).
Fin(Alph)
Fin(S)
Con(A)
1-1-Corresp(S;x,y:(Alph List)//(x Rl y))
L(Auto) = L(A)
A 
MinAuto(Auto)
Applied Tactic: UnivCD THENA Auto
Generated subgoals:1. A MinAuto(Auto)2. EquivRel(Alph List;x,y.x Rl y)