Nuprl - Proof: rdist-property 1 1 2 1 2 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rdist-property 1 1 2 1 2 1 2

1. R : Id

2. in : |R|

IdLnk
3. out : |R|

IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. (

x.n(x)^k+1(i) = j)

x.n(x)^n+1(i) = j
9.

x.n(x)^d(i;j)(i) = j

By:	RW assert_pushdownC -1 THEN Try (DoSubsume THEN Analyze 0 THEN Analyze -1)

Generated subgoal:

1 9. x.n(x)^d(i;j)(i) = j Id
x.n(x)^d(i;j)(i) = j
1 step

About:

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