1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
  x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)

By:	AssertBY ((k.x.n(x)^k+1(i) = j)  ) (Reduce 0 THEN Try (DoSubsume THEN Analyze 0 THEN Analyze -1))

1

7. (k.x.n(x)^k+1(i) = j)     x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)

14 steps

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