2. to : |T|
(IdLnk List)
3. from : |T|
(IdLnk List)
4. f : Edge(T)
5. bi-graph(T;to;from)
6.
i,j:|T|.
6.
p:Edge(T) List.
6. lconnects(p;i;j) & (
q:Edge(T) List. lconnects(q;i;j) 
q = p)
7. L : |T| List
8.
i:|T|. (i 
L)
9. j : |T|
10. bi-graph(T;to;from)
11. spanner(f;T;to;from)
12.
||to(j)|| = 0
13.
(i:|T|. l:Edge(T). (l to(i)) f(l))
14.
i:|T|. (lto(i).f(l))
15. n :
16. 0<n
17. u : Edge(T)
18. v : Edge(T) List
19. lpath([u / v])
20. ||v||+1 = n-1
21.
f(u)
22. (
lv.f(l))
23. l : Edge(T)
24. (l
to(source(u)))
25.
f(l)
26.
||[u / v]|| = 0
27.
i:|T|.
27. (
lto(i).destination(l) = i
27. & T(source(l))
27. & (l
from(source(l)))
27. & (lnk-inv(l)
from(i)))
27. & (
lfrom(i).source(l) = i
27. & & T(destination(l))
27. & & (l
to(destination(l)))
27. & & (lnk-inv(l)
to(i)))
28.
l:IdLnk.
28. (l
to(source(u)))
28.
28. destination(l) = source(u)
28. & T(source(l))
28. & (l
from(source(l)))
28. & (lnk-inv(l)
from(source(u)))
29. (
lfrom(source(u)).source(l) = source(u)
29. & T(destination(l))
29. & (l
to(destination(l)))
29. & (lnk-inv(l)
to(source(u))))
Edge(T) 
r IdLnk
