1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. i = p(j)
8. x.n(x)^d(i;j)(i) = j
9. k:. k<d(i;j)  x.n(x)^k(i) = j
10. x.n(x)^d(i;p(j))(i) = p(j)
11. k:. k<d(i;p(j))  x.n(x)^k(i) = p(j)
12. n(p(j)) = j
13. x.n(x)^d(i;p(j))+1(i) = j
14. d(i;j)d(i;p(j))+1
15. d(i;p(j))d(i;j)-1
16. d(i;j)-1  
17. x.n(x)^d(i;j) = (x.n(x)) o (x.x) o x.n(x)^d(i;j)-1
  x.n(x)^d(i;j)-1(i) = p(j)

1

8. n(x.n(x)^d(i;j)-1(i)) = j 9. k:. k<d(i;j)  x.n(x)^k(i) = j 10. x.n(x)^d(i;p(j))(i) = p(j) 11. k:. k<d(i;p(j))  x.n(x)^k(i) = p(j) 12. n(p(j)) = j 13. x.n(x)^d(i;p(j))+1(i) = j 14. d(i;j)d(i;p(j))+1 15. d(i;p(j))d(i;j)-1 16. d(i;j)-1   17. x.n(x)^d(i;j) = (x.n(x)) o (x.x) o x.n(x)^d(i;j)-1   x.n(x)^d(i;j)-1(i) = p(j)

3 steps

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