1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i:|R|. 
4. R(source(in(i))) & R(destination(out(i)))
4. & source(out(i)) = i
4. & & destination(in(i)) = i
4. & & in(destination(out(i))) = out(i)
4. & & out(source(in(i))) = in(i)
5. i,j:|R|. k:. x.destination(out(x))^k(i) = j
6. i : |R|
7. k : 
8. (x.destination(out(x)))  |R||R|
9. i@0 : |R|
10. i@0 = i
11. j : |R|
12. n : 
13. n1:. 
13. n1<n
13. 
13. x.destination(out(x))^n1(i) = j  (m:k. x.destination(out(x))^m(i) = j)
14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j
15. n<k
16. f : |R||R|
17. (x.destination(out(x))) = f
18. f^k(i) = i
19. z : Id
20. z = i
  z  |R|

1

6. i : Id 7. R(i) 8. k :  9. (x.destination(out(x)))  |R||R| 10. i@0 : |R| 11. i@0 = i  Id 12. j : |R| 13. n :  14. n1:.  14. n1<n 14.  14. x.destination(out(x))^n1(i) = j  Id 14.  14. (m:k. x.destination(out(x))^m(i) = j  Id) 15. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j  Id 16. n<k 17. f : |R||R| 18. (x.destination(out(x))) = f 19. f^k(i) = i  Id 20. z : Id 21. z = i   R(z)

1 step

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