(25steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rdist-rprev

  R:(Id), in,out:(|R|IdLnk), i,j:|R|.
  ring(R;in;out i = p(j d(i;p(j)) = d(i;j)-1


By: Auto


Generated subgoal:

1 1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. i = p(j)
  d(i;p(j)) = d(i;j)-1

24 steps

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

(25steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc