Def d(i;j) == mu(k.x.n(x)^k+1(i) = j)+1

is mentioned by

Thm* R:(Id), in,out:(|R|IdLnk), i,j:|R|. Thm* ring(R;in;out)  i = p(j)  d(i;p(j)) = d(i;j)-1	[rdist-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]

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