1. T : Id
2. to : |T|(IdLnk List)
3. from : |T|(IdLnk List)
4. f : Edge(T)
5. bi-tree(T;to;from)
6. bi-graph(T;to;from)
7. i,j:|T|.
7. p:Edge(T) List. 
7. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)
8. L:|T| List. i:|T|. (i  L)
9. |T|
10. spanner(f;T;to;from)
11. i : |T|
12. j : |T|
13. spanner-root(f;T;to;from;i)
14. spanner-root(f;T;to;from;j)
  p:Edge(T) List. 0<||p||  lpath(p)  f(last(p))  (lp.f(l))

By:

InductionOnList THEN Reduce 0 THEN MaAuto THEN Reduce 0 THEN RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) 0 THEN MaAuto THEN DVar `v' THEN All Reduce THEN Try (Unfold `last` -1 THEN Reduce -1 THEN Trivial) THEN Try (BackThru Thm* P:(TProp). (xnil.P(x))) THEN RWO Thm* l:IdLnk, p:IdLnk List. Thm* lpath([l / p]) Thm*  Thm* lpath(p) Thm* & (||p|| = 0    destination(l) = source(hd(p)) & hd(p) = lnk-inv(l)) -2 THEN MaAuto THEN RWO Thm* L:T List, x:T. null(L)  last([x / L]) = last(L) -1 THEN Reduce 0

1	15. Edge(T) List 16. u : Edge(T) 17. u1 : Edge(T) 18. v1 : Edge(T) List 19. 0<||v1||+1  lpath([u1 / v1])  f(last([u1 / v1]))  (l[u1 / v1].f(l)) 20. 0<||v1||+1+1 21. lpath([u1 / v1]) 22. ||[u1 / v1]|| = 0   22.  22. destination(u) = source(hd([u1 / v1])) & hd([u1 / v1]) = lnk-inv(u)  IdLnk 23. f(last([u1 / v1]))   f(u)	20 steps
2	15. Edge(T) List 16. u : Edge(T) 17. u1 : Edge(T) 18. v1 : Edge(T) List 19. 0<||v1||+1  lpath([u1 / v1])  f(last([u1 / v1]))  (l[u1 / v1].f(l)) 20. 0<||v1||+1+1 21. lpath([u1 / v1]) 22. ||[u1 / v1]|| = 0   22.  22. destination(u) = source(hd([u1 / v1])) & hd([u1 / v1]) = lnk-inv(u)  IdLnk 23. f(last([u1 / v1]))   (l[u1 / v1].f(l))	1 step

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