R:(Id), in,out:(|R|IdLnk).
  ring(R;in;out)  (L:|R| List. 0<||L|| & (i:|R|. (i  L)))

1

1. R : Id 2. in : |R|IdLnk 3. out : |R|IdLnk 4. i:|R|.  4. R(source(in(i))) & R(destination(out(i))) 4. & source(out(i)) = i 4. & & destination(in(i)) = i 4. & & in(destination(out(i))) = out(i) 4. & & out(source(in(i))) = in(i) 5. i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id 6. |R|   L:|R| List. 0<||L|| & (i:|R|. (i  L))

41 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html