Def ring(R;in;out)
Def == (i:|R|. 
Def == ((R(source(in(i)))) & (R(destination(out(i))))
Def == (& source(out(i)) = i
Def == (& & destination(in(i)) = i
Def == (& & in(destination(out(i))) = out(i)  IdLnk
Def == (& & out(source(in(i))) = in(i)  IdLnk)
Def == & (i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id)
Def == & |R|

is mentioned

In prior sections: mb event system 7

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html