Def lconnects(p;i;j)
Def == lpath(p)
Def == & (||p|| = 0    i = j  Id)
Def == & (||p|| = 0    i = source(hd(p)) & j = destination(last(p)))

is mentioned by

Def bi-tree(T;to;from) Def == bi-graph(T;to;from) Def == & (i,j:|T|. Def == & (p:Edge(T) List.  Def == & (lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)) Def == & (L:|T| List. i:|T|. (i  L)) Def == & |T|

[bi-tree]

In prior sections: mb event system 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html