Nuprl - Proof: ring-leader1 feasible 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ring-leader1 feasible 1 1

1. R : Id

2. uid : |R|

3. out : |R|

IdLnk
4. in : |R|

IdLnk
5. ring(R;in;out)
6. Inj(|R|;

; uid)
7. L : |R| List
8. 0<||L||
9.

i:|R|. (i

i:Id. R(i)

By:	Auto THEN InstHyp [i] -3 THEN MaAuto THEN RepeatFor 2 (ParallelLast THEN MaAuto) THEN ExRepD THEN ParallelLast THEN MaAuto

Generated subgoals:

None

About:

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