(4steps 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: rnext-rprev
  R:(Id), in,out:(|R|IdLnk), j:|R|. ring(R;in;out)  n(p(j)) = j
By: Auto THEN Unfold `ring` -1 THEN Unfolds [`rnext`;`rprev`] 0 THEN ExRepD
THEN
InstHyp [j] 5
THEN
ExRepD
THEN
StrongHypSubst -1 0

Generated subgoals:

1 1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. j : |R|
5. i:|R|. 
5. R(source(in(i))) & R(destination(out(i)))
5. & source(out(i)) = i
5. & & destination(in(i)) = i
5. & & in(destination(out(i))) = out(i)
5. & & out(source(in(i))) = in(i)
6. i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id
7. |R|
8. R(source(in(j)))
9. R(destination(out(j)))
10. source(out(j)) = j
11. destination(in(j)) = j
12. in(destination(out(j))) = out(j)
13. out(source(in(j))) = in(j)
  destination(in(j)) = j  |R|
1 step
2 1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. j : |R|
5. i:|R|. 
5. R(source(in(i))) & R(destination(out(i)))
5. & source(out(i)) = i
5. & & destination(in(i)) = i
5. & & in(destination(out(i))) = out(i)
5. & & out(source(in(i))) = in(i)
6. i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id
7. |R|
8. R(source(in(j)))
9. R(destination(out(j)))
10. source(out(j)) = j
11. destination(in(j)) = j
12. in(destination(out(j))) = out(j)
13. out(source(in(j))) = in(j)
14. z : IdLnk
15. z = in(j)
  destination(z)  |R|
2 steps

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

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