(16steps 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-property 1 1 2 1 2 1
1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. (k.x.n(x)^k+1(i) = j)  
8. n:. x.n(x)^n+1(i) = j
9. x.n(x)^d(i;j)-1+1(i) = j
  x.n(x)^d(i;j)(i) = j
By: Subst ((d(i;j)-1+1) ~ d(i;j)) -1

Generated subgoals:

1   (d(i;j)-1+1) ~ d(i;j)
Auto
2 9. x.n(x)^d(i;j)(i) = j
  x.n(x)^d(i;j)(i) = j
2 steps

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

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