Def lpath(p)
Def == i:(||p||-1). 
Def == destination(p[i]) = source(p[(i+1)]) & p[(i+1)] = lnk-inv(p[i])  IdLnk

is mentioned by

Thm* p:IdLnk List, i:||p||, j:(i+1). Thm* lpath(p)  lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))	[lpath-members-connected]
Thm* 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))	[lpath_cons]
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)))	[lconnects]

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