(10steps 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 cons
  l:IdLnk, p:IdLnk List.
  lpath([l / p])
  
  lpath(p)
  & (||p|| = 0    destination(l) = source(hd(p)) & hd(p) = lnk-inv(l))
By: Auto

Generated subgoals:

1 1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
  lpath(p)
1 step
2 1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ||p|| = 0  
  destination(l) = source(hd(p))
1 step
3 1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ||p|| = 0  
  hd(p) = lnk-inv(l)
1 step
4 1. l : IdLnk
2. p : IdLnk List
3. lpath(p)
4. ||p|| = 0    destination(l) = source(hd(p)) & hd(p) = lnk-inv(l)
  lpath([l / p])
6 steps

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

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