1. r : 
2. 0<r
3. L:Top List. ||nth_tl(r-1;L)|| = if r-1<||L|| ||L||-(r-1) else 0 fi
  L:Top List. 
  ||if r0 L else nth_tl(r-1;tl(L)) fi|| = if r<||L|| ||L||-r else 0 fi

1	4. L : Top List 5. 0<r 6. r<||L||   ||nth_tl(r-1;tl(L))|| = ||L||-r	1 step
2	4. L : Top List 5. 0<r 6. ||L||r   ||nth_tl(r-1;tl(L))|| = 0	3 steps

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