1. R : Id
2. uid : |R|
3. out : |R|IdLnk
4. in : |R|IdLnk
5. ring(R;in;out)
6. Inj(|R|; ; uid)
7. L : |R| List
8. 0<||L||
9. i:|R|. (i  L)
10. i:Id. R(i)  (i  L)
  (iL.(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of(
  (iL.(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L)
  (iL.(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).
  interface-check(loc.
  (ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg)))))

By:

Assert (i:Id.  (R(i) ( ((ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of( ((ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L) ((ltgma-outlinks((ring-leader1(i;R;uid;out;in));i). (interface-check(loc. ((ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg)))))

1	i:Id.    R(i)      (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of(   (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L)   (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).   interface-check(loc.   (ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg))))	4 steps
2	11. i:Id.  11. R(i) 11.  11. (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of( 11. (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L) 11. (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i). 11. interface-check(loc. 11. (ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg))))   (iL.(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of(   (iL.(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L)   (iL.(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).   interface-check(loc.   (ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg)))))	4 steps

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