IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rdist-rprev
1
1
2
2
2
1
1
2
1
1
1
2
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. 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
18.
i,j:|R|. n(i) = n(j) 
i = j
x.n(x)^d(i;j)-1(i) = p(j)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html