PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: any iso min auto

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

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

About:
alluniverseimpliesquotientlist