T:(Id
), to,from:(|T|(IdLnk List)), f:(Edge(T)).
Thm* bi-tree(T;to;from)
Thm*
Thm* spanner(f;T;to;from)
(
i:|T|. spanner-root(f;T;to;from;i))T:(Id), to,from:(|T|(IdLnk List)).
Thm* bi-tree(T;to;from)
(n:
. p:Edge(T) List. lpath(p) ||p||
n)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))L:A List, x:A. (A 
r B) (x L) (x L)T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)
source(u) |T|P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))