Nuprl - Proof: rel star closure

(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

T:Type, R,R2:(T

Prop).

Trans(T)(R2(_1,_2))

(

x,y:T. (x R y)

(x R2 y))

(

x,y:T. (x (R^*) y)

(x R2 y)

x = y)

By:	Auto THEN Unfold `rel_star` -1 THEN Reduce -1 THEN ExRepD THEN MoveToConcl -1 THEN MoveToConcl -2 THEN MoveToConcl -2 THEN NatInd -1

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. R2 : TTProp
4. Trans(T)(R2(_1,_2))
5. x,y:T. (x R y)  (x R2 y)
6. x : T
7. y : T
8. x R^0 y
  (x R2 y)  x = y
1 step

2 1. T : Type
2. R : TTProp
3. R2 : TTProp
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
5 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

1	1. T : Type 2. R : TTProp 3. R2 : TTProp 4. Trans(T)(R2(_1,_2)) 5. x,y:T. (x R y) (x R2 y) 6. x : T 7. y : T 8. x R^0 y (x R2 y) x = y	1 step
2	1. T : Type 2. R : TTProp 3. R2 : TTProp 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	5 steps