Nuprl - Pf mn_23 2 1 2 1 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. n: {1...}
2. A: Type
3. L: LangOver(A)
4. L A*Prop
5. R: A*A*Prop
6. EquivRel x,y:A*. x R y
7. n ~ (x,y:A*//(x R y))
8. x,y,z:A*. (x R y) ((z @ x) R (z @ y))
9. g: (x,y:A*//(x R y))
10. l:A*. L(l) g(l)
11. x,y:x,y:A*//(x R y). Dec(x Rg y)
12. EquivRel x,y:A*. x L-induced Equiv y

m:. m ~ (x,y:A*//(x L-induced Equiv y))

By: Inst Thm* R:(A*A*Prop). (EquivRel 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))). EquivRel u,v:x,y:A*//(x R y). u Rg v) [A;R;g]

Generated subgoal:

1 13. EquivRel u,v:x,y:A*//(x R y). u Rg v
m:. m ~ (x,y:A*//(x L-induced Equiv y))

About: