PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: mn 13 1 1 2 1 1 1 1 1 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
6. R: Alph*Alph*Prop
7. EquivRel x,y:Alph*. x R y
8. g: (x,y:Alph*//R(x,y))
9. m:
10. m ~ (x,y:Alph*//R(x,y))
11. l:Alph*. LangOf(Auto)(l) g(l)
12. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)

Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
By: Inst Thm* n:{1...}, A:Type, L:LangOver(A), R:(A*A*Prop). Fin(A) (EquivRel x,y:A*. x R y) (n ~ (x,y:A*//(x R y))) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). l:A*. L(l) g(l)) (m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l))) [m;Alph;LangOf(Auto);R]
Generated subgoals:

14. Fin(Alph)
5. Fin(St)
6. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
7. R: Alph*Alph*Prop
8. EquivRel x,y:Alph*. x R y
9. g: (x,y:Alph*//R(x,y))
10. m:
11. m ~ (x,y:Alph*//R(x,y))
12. l:Alph*. LangOf(Auto)(l) g(l)
13. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
1m
24. Fin(Alph)
5. Fin(St)
6. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
7. R: Alph*Alph*Prop
8. EquivRel x,y:Alph*. x R y
9. g: (x,y:Alph*//R(x,y))
10. m:
11. m ~ (x,y:Alph*//R(x,y))
12. l:Alph*. LangOf(Auto)(l) g(l)
13. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
g:((x,y:Alph*//(x R y))). l:Alph*. LangOf(Auto)(l) g(l)
313. (m:. m ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))) & (l:Alph*. Dec(LangOf(Auto)(l)))
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))

About:
quotientlistuniverseandfunctionpropapply
boolnatural_numberallassertimpliesexists