(13steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
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  L)
  i:Id. R(i (i  L)


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


Generated subgoals:

None

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

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