Nuprl - Pf mn_23 2 1 2 1 1 1 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
13. EquivRel u,v:x,y:A*//(x R y). u Rg v
14. x,y:A*//(x L-induced Equiv y) = x,y:A*//(x Rg y)
15. (x,y:A*//(x Rg y)) ~ (u,v:(x,y:A*//(x R y))//(u Rg v))

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

By: FwdThru Thm* n:{1...}, A:Type, R:(AAProp). (n ~ A) (EquivRel x,y:A. x R y) (x,y:A. Dec(x R y)) (m:(n+1). m ~ (x,y:A//(x R y))) [7;13]

Generated subgoal:

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

About: