mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* 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]
cites the following:
3Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)][select_l_interval]
2Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j  [length_l_interval]
4Thm* l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j][hd_l_interval]
4Thm* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)][last_l_interval]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 2 Sections EventSystems Doc