IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rdist-property11212211 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. i@0:. i@0<d(i;j)-1 x.n(x)^i@0+1(i) = j 10. k : 11. k<d(i;j)
12. x.n(x)^k(i) = j x.n(x)^k(i) = j
By:
ParallelOp -1 THEN HypSubst -1 0 THEN Try (Fold `member` 0)
THEN
Try (DoSubsume THEN Analyze 0 THEN Analyze -1)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html