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. L1 : |T| List
9. i:|T|. (i  L1)
10. |T|
11. spanner(f;T;to;from)
12. i : |T|
13. j : |T|
14. spanner-root(f;T;to;from;i)
15. spanner-root(f;T;to;from;j)
16. p:Edge(T) List. 0<||p||  lpath(p)  f(last(p))  (lp.f(l))
17. bi-graph(T;to;from)
18. i,j:|T|.
18. p:Edge(T) List. 
18. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)
19. L : |T| List
20. i:|T|. (i  L)
21. |T|
22. u : Edge(T)
23. v : Edge(T) List
24. lpath([u / v])
25. ||v||+1 = 0  i = j
26. ||v||+1 = 0  i = source(u) & j = destination(last([u / v]))
27. q:Edge(T) List. lconnects(q;i;j)  q = [u / v]
  f(last([u / v]))

By:	AllHyps (h.Unfold `spanner-root` h THEN BackThru h THEN Reduce 0)

1

15. l:Edge(T). (l  to(j))  f(l) 16. p:Edge(T) List. 0<||p||  lpath(p)  f(last(p))  (lp.f(l)) 17. bi-graph(T;to;from) 18. i,j:|T|. 18. p:Edge(T) List.  18. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p) 19. L : |T| List 20. i:|T|. (i  L) 21. |T| 22. u : Edge(T) 23. v : Edge(T) List 24. lpath([u / v]) 25. ||v||+1 = 0  i = j  Id 26. ||v||+1 = 0  i = source(u) & j = destination(last([u / v])) 27. q:Edge(T) List. lconnects(q;i;j)  q = [u / v]   (last([u / v])  to(j))

2 steps

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