R:(Id
), uid:(|R|
), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm*
Thm* Inj(|R|;
; uid)
Thm*
Thm*
loc.
(ring-leader1(loc;R;uid;out;in))
Thm* realizes es.
ldr:|R|.
Thm* realizes es.
e@ldr.kind(e) = locl("leader")
Thm* realizes es.& (
i:|R|. e@i.kind(e) = locl("leader") i = ldr 
|R|)f:(A
), L:A List. 0<||L|| (aL.(xL.f(x)
f(a)))R:(Id), in,out:(|R|IdLnk).
Thm* ring(R;in;out)
(L:|R| List. 0<||L|| & (i:|R|. (i L)))R:(Id). SQType(|R|)R:(Id), in,out:(|R|IdLnk), j:|R|. ring(R;in;out) n(p(j)) = jR:(Id), in,out:(|R|IdLnk), i,j:|R|.
Thm* ring(R;in;out)
i = p(j) d(i;p(j)) = d(i;j)-1
r B) (B r C) (A r C)