1. l : IdLnk
2. u : IdLnk
3. v : IdLnk List
4. lpath([u / v])
5. destination(l) = source(u)
6. u = lnk-inv(l)
  lpath([l; u / v])

By:	ParallelOp -3 THEN Analyze 0 THEN CaseNat 0 `i' THEN Reduce 0 THEN RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0 THEN InstHyp [i-1] 4

1	4. i:(||[u / v]||-1).  4. destination([u / v][i]) = source([u / v][(i+1)]) 4. & [u / v][(i+1)] = lnk-inv([u / v][i]) 5. destination(l) = source(u) 6. u = lnk-inv(l)  IdLnk 7. i : (||[l; u / v]||-1) 8. i = 0 9. destination([u / v][(i-1)]) = source([u / v][(i-1+1)]) 10. [u / v][(i-1+1)] = lnk-inv([u / v][(i-1)])   destination([u / v][(i-1)]) = source([u / v][(i+1-1)])	1 step
2	4. i:(||[u / v]||-1).  4. destination([u / v][i]) = source([u / v][(i+1)]) 4. & [u / v][(i+1)] = lnk-inv([u / v][i]) 5. destination(l) = source(u) 6. u = lnk-inv(l)  IdLnk 7. i : (||[l; u / v]||-1) 8. i = 0 9. destination([u / v][(i-1)]) = source([u / v][(i-1+1)]) 10. [u / v][(i-1+1)] = lnk-inv([u / v][(i-1)])   [u / v][(i+1-1)] = lnk-inv([u / v][(i-1)])	1 step

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