Nuprl - Pf Rl_iff

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. A: Type
2. R: A*A*Prop
3. EquivRel x,y:A*. x R y
4. x,y,z:A*. (x R y) ((z @ x) R (z @ y))
5. g: (x,y:A*//(x R y))
6. L: LangOver(A)
7. l:A*. L(l) g(l)
8. x: A*
9. y: A*

(z:A*. L(z @ x) L(z @ y)) (z:A*. g(z @ x) g(z @ y))

By: Assert (L A*Prop) THEN RWO "7" 0

Generated subgoals:

1 L A*Prop

2 10. L A*Prop
(z:A*. g(z @ x) g(z @ y)) (z:A*. g(z @ x) g(z @ y))

About:

1	`L A*Prop`
2	10. `L AProp` `(z:A. g(z @ x) g(z @ y)) (z:A*. g(z @ x) g(z @ y))`