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@0n
k:(n+1). x R^k y| By: |
Thm* R:(TTProp), k:, x,y:T.
Thm* (x R^k y) Thm* 
Thm* ( L:T List.
Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))
-2 THEN ExRepD |
| 1 |
n List
8. ||L|| = n@0+1
9. L[0] = x 10. last(L) = y 11. i:n@0. L[i] R L[(i+1)]
12. n@0n
k:(n+1). x R^k y | 34 steps |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |