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) 
(i L)
11. i : Id
12. R(i)
13. destination(in(i)) = i
(ltgma-outlinks(
(ring-leader1(i;R;uid;out;in));i).(destination(1of(
(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg)) L)
(ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).
interface-check(
loc.
(ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg))))
