PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 2
1. n: {1...}
2. A: Type
3. L: LangOver(A)
4. L A*Prop

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)))
By: GenExRepD
Generated subgoals:

15. R: A*A*Prop
6. Fin(A)
7. EquivRel x,y:A*. x R y
8. n ~ (x,y:A*//(x R y))
9. x,y,z:A*. (x R y) ((z @ x) R (z @ y))
10. g: (x,y:A*//(x R y))
11. l:A*. L(l) g(l)
m:. m ~ (x,y:A*//(x L-induced Equiv y))
25. R: A*A*Prop
6. Fin(A)
7. EquivRel x,y:A*. x R y
8. n ~ (x,y:A*//(x R y))
9. x,y,z:A*. (x R y) ((z @ x) R (z @ y))
10. g: (x,y:A*//(x R y))
11. l:A*. L(l) g(l)
12. l: A*
Dec(L(l))

About:
allfunctionlistpropimpliesnatural_numberquotient
existsboolapplyassertanduniversemember