Nuprl - Proof: rel exp add 2

(6steps 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 exp add 2

1. T : Type
2. R : T

T

Prop
3. m :

4. 0<m
5.

n:

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

(y R^n z)

(x R^m-1+n z)

n:

, x,y,z:T. (x R^m y)

(y R^n z)

(x R^m+n z)

By:	Auto THEN MoveToConcl -2 THEN RecUnfold `rel_exp` 0 THEN SplitOnConclITE THEN Reduce 0 THEN SplitOnConclITE THEN Reduce 0

Generated subgoal:

1 6. n :
7. x : T
8. y : T
9. z : T
10. y R^n z
11. m=0
12. m+n=0
13. z:T. (x R z) & (z R^m-1 y)
z@0:T. (x R z@0) & (z@0 R^m+n-1 z)
3 steps

About:

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

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