(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 3 1
1. p : IdLnk List
2. i : ||p||
3. j : (i+1)
4. lpath(p)
5. i-j = 0
  source(p[i]) = destination(p[(i-1)])
By: Unfold `lpath` -2 THEN InstHyp [i-1] -2

Generated subgoal:

1 4. i:(||p||-1). 
4. destination(p[i]) = source(p[(i+1)]) & p[(i+1)] = lnk-inv(p[i])
5. i-j = 0
6. destination(p[(i-1)]) = source(p[(i-1+1)])
7. p[(i-1+1)] = lnk-inv(p[(i-1)])
  source(p[i]) = destination(p[(i-1)])
1 step

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