Nuprl - Proof: rel star closure 2

(7steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star closure 2

1. T : Type
2. R : T

T

Prop
3. R2 : T

T

Prop
4. Trans(T)(R2(_1,_2))
5.

x,y:T. (x R y)

(x R2 y)
6. n :

7. 0<n
8.

x,y:T. (x R^n-1 y)

(x R2 y)

x = y
9. x : T
10. y : T
11. x R^n y

(x R2 y)

x = y

By:	MoveToConcl -1 THEN RecUnfold `rel_exp` 0 THEN SplitOnConclITE THEN Reduce 0 THEN ExRepD

Generated subgoal:

1 11. n = 0
12. z : T
13. x R z
14. z R^n-1 y
(x R2 y) x = y
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions mb nat Sections MarkB generic Doc