(9steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: lpath-members-connected 1 2
1. p : IdLnk List
2. i : ||p||
3. j : (i+1)
4. lpath(p)
  (||l_interval(p;j;i)|| = 0    source(p[j]) = source(p[i]))
  & (||l_interval(p;j;i)|| = 0  
  & (
  & (source(p[j]) = source(hd(l_interval(p;j;i)))
  & (& source(p[i]) = destination(last(l_interval(p;j;i))))
By: Auto
THEN
RWO Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j   -1

Generated subgoals:

1 5. i-j = 0
  source(p[j]) = source(p[i])
1 step
2 5. i-j = 0
  source(p[j]) = source(hd(l_interval(p;j;i)))
1 step
3 5. i-j = 0
  source(p[i]) = destination(last(l_interval(p;j;i)))
3 steps

About:
listintnatural_numberaddsubtractuniverseequalimpliesandall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(9steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc