Nuprl - Pf mn_23 2 1 2 1 1 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))
16. m: (n+1)
17. m ~ (u,v:(x,y:A*//(x R y))//(u Rg v))

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

By: FwdThru Thm* (A ~ B) (B ~ A) [15]

Generated subgoal:

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

About: