Nuprl - Pf mn

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

By: Assert (x,y:x,y:A*//(x R y). Dec(x Rg y))

Generated subgoals:

1 12. x: x,y:A*//(x R y)
13. y: x,y:A*//(x R y)
Dec(x Rg y)

2 12. x,y:x,y:A*//(x R y). Dec(x Rg y)
m:. m ~ (x,y:A*//(x L-induced Equiv y))

About:

1	12. `x:` `x,y:A//(x R y)` 13. `y:` `x,y:A//(x R y)` `Dec(x Rg y)`
2	12. `x,y:x,y:A//(x R y). Dec(x Rg y)` `m:. m ~ (x,y:A//(x L-induced Equiv y))`