IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ring-leader1 feasible11 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|. (iL)
i:Id. R(i) (iL)
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