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
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)
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 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)))
