Nuprl - Pf mn_23 2 1 2 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)

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

By: FwdThru Thm* R:(TTProp). (EquivRel x,y:T. x R y) (Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop). (EquivRel u,v:x,y:T//(x R y). u Q v) ((x,y:T//(x Q y)) ~ (u,v:(x,y:T//(x R y))//(u Q v)))) [13]

Generated subgoal:

1 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))

About: