PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: mn 13 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph) & Fin(St)
5. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y

Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
By: Inst Thm* L:LangOver(Alph). Fin(Alph) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto)) (R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) c (g:((x,y:Alph*//R(x,y))). Fin(x,y:Alph*//R(x,y)) & (l:Alph*. L(l) g(l)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)))) [Alph;LangOf(Auto)]
Generated subgoals:

14. Fin(Alph)
5. Fin(St)
6. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
St:Type, Auto@0:Automata(Alph;St). Fin(St) & LangOf(Auto) = LangOf(Auto@0)
26. R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) c (g:((x,y:Alph*//R(x,y))). Fin(x,y:Alph*//R(x,y)) & (l:Alph*. LangOf(Auto)(l) g(l)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)))
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))

About:
quotientlistuniverseandexists