At: min is unique111 1. Alph: Type 2. St: Type 3. Auto: Automata(Alph;St) 4. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y 5. Con(Auto) 6. St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) 7. Fin(Alph) 8. Fin(St)
Auto A(l.Auto(l)) By: Unfold `connected` 5
THEN
FwdThru
Thm*Q:(ABProp). (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x)))
[5]
THEN
Thin 5
THEN
Analyze 8 Generated subgoal: