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. f(last([u1 / v1]))
23. destination(u) = source(u1)
24. u1 = lnk-inv(u)
25. f(u1)
26. (lv1.f(l))
27. l:Edge(T). f(l) = f(inverse(l))
28. i:|T|, l1,l2:Edge(T).
28. (l1  to(i))  (l2  to(i))  l1 = l2  f(l1)  f(l2)
29. f(u1) = f(inverse(u1))
  (u  to(source(u1)))

1

8. L : |T| List 9. i:|T|. (i  L) 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. Edge(T) List 17. u : Edge(T) 18. u1 : Edge(T) 19. v1 : Edge(T) List 20. 0<||v1||+1  lpath([u1 / v1])  f(last([u1 / v1]))  (l[u1 / v1].f(l)) 21. 0<||v1||+1+1 22. lpath([u1 / v1]) 23. f(last([u1 / v1])) 24. destination(u) = source(u1) 25. u1 = lnk-inv(u)  IdLnk 26. f(u1) 27. (lv1.f(l)) 28. l:Edge(T). f(l) = f(inverse(l)) 29. i:|T|, l1,l2:Edge(T). 29. (l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  f(l1)  f(l2) 30. f(u1) = f(inverse(u1)) 31. i:|T|.  31. (lto(i).destination(l) = i 31. & T(source(l)) 31. & (l  from(source(l))) 31. & (lnk-inv(l)  from(i))) 31. & (lfrom(i).source(l) = i 31. & & T(destination(l)) 31. & & (l  to(destination(l))) 31. & & (lnk-inv(l)  to(i)))   (u  to(destination(u)))

2 steps

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