Nuprl - Proof: ring-leader1 feasible 1 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ring-leader1 feasible 1 2 1 1 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

L)
10.

i:Id. R(i)

L)
11. i : Id
12. R(i)

destination(in(i)) = i

By:	DupHyp 5 THEN Unfold `ring` -1 THEN ExRepD THEN InstHyp [i] -3 THEN ExRepD THEN MaAuto

Generated subgoals:

None

About:

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