(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
1. p : IdLnk List
2. i : ||p||
3. j : (i+1)
4. lpath(p)
  lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))
By: Unfold `lconnects` 0 THEN Analyze 0

Generated subgoals:

1   lpath(l_interval(p;j;i))
1 step
2   (||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))))
6 steps

About:
listintnatural_numberaddequalimpliesand
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