Nuprl - Proof: rel plus implies

(16steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel plus implies

T:Type, R:(T

Prop), x,y:T.

(x R^+ y)

(x R y)

(

z:T. (x R^+ z) & (z R y))

By:	Auto THEN Unfold `rel_plus` -1 THEN Reduce -1 THEN ExRepD THEN MoveToConcl -1 THEN MoveToConcl -2 THEN MoveToConcl -2 THEN NatPlusInd -1

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. n :
4. 0<n
5. 0<n-1  (x,y:T. (x R^n-1 y)  (x R y)  (z:T. (x R^+ z) & (z R y)))
6. n = 1
7. 0<1
8. x : T
9. y : T
10. x R^1 y
  (x R y)  (z:T. (x R^+ z) & (z R y))
2 steps

2 1. T : Type
2. R : TTProp
3. n :
4. 0<n
5. 0<n-1  (x,y:T. (x R^n-1 y)  (x R y)  (z:T. (x R^+ z) & (z R y)))
6. n = 1
7. 0<n
8. x : T
9. y : T
10. x R^n y
  (x R y)  (z:T. (x R^+ z) & (z R y))
13 steps

About:

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

(16steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc

1	1. T : Type 2. R : TTProp 3. n : 4. 0<n 5. 0<n-1 (x,y:T. (x R^n-1 y) (x R y) (z:T. (x R^+ z) & (z R y))) 6. n = 1 7. 0<1 8. x : T 9. y : T 10. x R^1 y (x R y) (z:T. (x R^+ z) & (z R y))	2 steps
2	1. T : Type 2. R : TTProp 3. n : 4. 0<n 5. 0<n-1 (x,y:T. (x R^n-1 y) (x R y) (z:T. (x R^+ z) & (z R y))) 6. n = 1 7. 0<n 8. x : T 9. y : T 10. x R^n y (x R y) (z:T. (x R^+ z) & (z R y))	13 steps