R:(Id
), uid:(|R|
), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm*
Thm* Inj(|R|;
; uid) d-feasible(
loc.
(ring-leader1(loc;R;uid;out;in)))R:(Id), in,out:(|R|IdLnk).
Thm* ring(R;in;out)
(
L:|R| List. 0<||L|| & (i:|R|. (i 
L)))| Rank | Theorem | Name |
| 5 | R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out) Thm*
Thm* Inj(|R|; ; uid) d-feasible(loc.(ring-leader1(loc;R;uid;out;in))) | [ring-leader1__feasible] |
| cites the following: | ||
| 4 | R:(Id), in,out:(|R|IdLnk).
Thm* ring(R;in;out) (L:|R| List. 0<||L|| & (i:|R|. (i L))) | [ring-list] |