Nuprl - Proof: preserved by star 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: preserved by star 1 1

1. T : Type
2. P : T

Prop
3. R : T

Prop
4.

x,y:T. P(x)

(x R y)

P(y)
5. x : T
6. y : T
7. P(x)
8. n :

9. x R^n y

P(y)

By:	MoveToConcl -1 THEN RepeatFor 3 (MoveToConcl -2) THEN Analyze -1 THEN IntInd -2

Generated subgoals:

1 5. 00
6. x : T
7. y : T
8. P(x)
9. x R^0 y
  P(y)
1 step

2 5. n :
6. 0<n
7. n-10  (x,y:T. P(x)  (x R^n-1 y)  P(y))
8. n0
9. x : T
10. y : T
11. P(x)
12. x R^n y
  P(y)
4 steps

About:

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

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

1	5. 00 6. x : T 7. y : T 8. P(x) 9. x R^0 y P(y)	1 step
2	5. n : 6. 0<n 7. n-10 (x,y:T. P(x) (x R^n-1 y) P(y)) 8. n0 9. x : T 10. y : T 11. P(x) 12. x R^n y P(y)	4 steps