PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: any ge min auto

Alph,St:Type, Auto:Automata(Alph;St), S:Type, A:Automata(Alph;S). Fin(Alph) Fin(St) LangOf(Auto) = LangOf(A) Con(A) |S| |x,y:Alph*//(x LangOf(Auto)-induced Equiv y)|
By: UnivCD
Generated subgoal:

11. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. S: Type
5. A: Automata(Alph;S)
6. Fin(Alph)
7. Fin(St)
8. LangOf(Auto) = LangOf(A)
9. Con(A)
|S| |x,y:Alph*//(x LangOf(Auto)-induced Equiv y)|

About:
alluniverseimpliesquotientlist