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