(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 1 1 2 2

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)
8. x.n(x)^d(i;j)(i) = j
9. k:k<d(i;j x.n(x)^k(i) = j
10. x.n(x)^d(i;p(j))(i) = p(j)
11. k:k<d(i;p(j))  x.n(x)^k(i) = p(j)
12. n(p(j)) = j
13. x.n(x)^d(i;p(j))+1(i) = j
  d(i;p(j)) = d(i;j)-1


By: Assert (d(i;j)d(i;p(j))+1)


Generated subgoals:

1   d(i;j)d(i;p(j))+1
2 steps
2 14. d(i;j)d(i;p(j))+1
  d(i;p(j)) = d(i;j)-1

15 steps

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