T:(Id
), to,from:(|T|(IdLnk List)), f:(Edge(T)).
Thm* bi-tree(T;to;from)
Thm*
Thm* spanner(f;T;to;from)
Thm*
Thm* (
i,j:|T|.
Thm* (spanner-root(f;T;to;from;i)
spanner-root(f;T;to;from;j) i = j)L:T List, x:T. 
null(L) last([x / L]) = last(L)l:IdLnk, p:IdLnk List.
Thm* lpath([l / p])
Thm*
Thm* lpath(p)
Thm* & (
||p|| = 0 
destination(l) = source(hd(p)) & hd(p) = lnk-inv(l))P:(TProp). (xnil.P(x))l:IdLnk. destination(lnk-inv(l)) = source(l)l:IdLnk. lnk-inv(lnk-inv(l)) = l IdLnkp:. 
p = pG:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)
((e to(i)) destination(e) = i)T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)
destination(u) |T|P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)
source(u) |T|G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)
((inverse(e) to(i)) source(e) = i)