(8steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rdist wf 1 1
1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. n : |R||R|
8. (x.n(x)) = n
  n1:. (k.n^k+1(i) = j)(n1)
By: Reduce 0 THEN Unfold `ring` -3 THEN ExRepD THEN InstHyp [i;j] -4 THEN ExRepD

Generated subgoal:

1 6. i:|R|. 
6. R(source(in(i))) & R(destination(out(i)))
6. & source(out(i)) = i
6. & & destination(in(i)) = i
6. & & in(destination(out(i))) = out(i)
6. & & out(source(in(i))) = in(i)
7. i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id
8. |R|
9. n : |R||R|
10. (x.n(x)) = n
11. k : 
12. x.destination(out(x))^k(i) = j  Id
  n1:. n^n1+1(i) = j
5 steps

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

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