Nuprl - Proof: rel exp add

(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

T:Type, R:(T

Prop), m,n:

, x,y,z:T.

(x R^m y)

(y R^n z)

(x R^m+n z)

By:	InductionOnNat

Generated subgoals:

1 1. T : Type
2. R : TTProp
  n:, x,y,z:T. (x R^0 y)  (y R^n z)  (x R^0+n z)
1 step

2 1. T : Type
2. R : TTProp
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)
4 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

1	1. T : Type 2. R : TTProp n:, x,y,z:T. (x R^0 y) (y R^n z) (x R^0+n z)	1 step
2	1. T : Type 2. R : TTProp 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)	4 steps