2. R :
n
nProp
3. x :
n
4. y :
n
5. n@0 :
6.
j:. j<n@0 
(x R^j y) (
k:(n+1). x R^k y)
7. x R^n@0 y
8. n@0
n
k:(n+1). x R^k y
nnProp
n
n
j:. j<n@0 (x R^j y) (k:(n+1). x R^k y)
n
k:(n+1). x R^k y| By: |
|
None
About:
 |  |  |  |  |  |  |  |