6. St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
7. Fin(Alph)
8. Fin(St)
Auto 
A(
l.Auto(l)
) Con(Auto) & (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & Fin(Alph) & Fin(St) 
Auto A(l.Auto(l))| 1 | 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)) |
About:
 |  |  |  |  |  |