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)
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)
23. f(last([u1 / v1]))
  f(u)

By:	Reduce -2 THEN Analyze -2 THEN AssertBY (l[u1 / v1].f(l)) BackThruSomeHyp

1

22. f(last([u1 / v1])) 23. destination(u) = source(u1) 24. u1 = lnk-inv(u)  IdLnk 25. (l[u1 / v1].f(l))   f(u)

19 steps

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