PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: min is unique

Alph,St:Type, Auto:Automata(Alph;St). Con(Auto) & (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & Fin(Alph) & Fin(St) Auto A(l.Auto(l))
By:
Analyze 0
THEN
Analyze 0
THEN
Analyze 0
Generated subgoal:

11. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
Con(Auto) & (St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & Fin(Alph) & Fin(St) Auto A(l.Auto(l))

About:
alluniverseimpliesandquotientlistlambda