is mentioned by

Thm* R:(Id), in,out:(|R|IdLnk). Thm* ring(R;in;out)  (i,j:|R|. n(i) = n(j)  i = j)	[rnext-one-one]
Thm* R:(Id), in,out:(|R|IdLnk), j:|R|. ring(R;in;out)  n(p(j)) = j	[rnext-rprev]
Thm* R:(Id), in,out:(|R|IdLnk), i,j:|R|. Thm* ring(R;in;out) Thm*  Thm* x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)	[rdist-property]
Def d(i;j) == mu(k.x.n(x)^k+1(i) = j)+1	[rdist]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html