Def  == {i:| 0i }

is mentioned by

Thm* T:(Id), to,from:(|T|(IdLnk List)). Thm* bi-tree(T;to;from)  (n:. p:Edge(T) List. lpath(p)  ||p||n)	[bi-tree-diameter]
Thm* 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|)	[ring-leader1__realizes]
Thm* 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]
Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk). Thm* ring(R;in;out) Thm*  Thm* Inj(|R|; ; uid)  ring-leader1(loc;R;uid;out;in)  MsgA List	[ring-leader1_wf]
Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk). Thm* ring(R;in;out) Thm*  Thm* Inj(|R|; ; uid)  (A,Bring-leader1(loc;R;uid;out;in).A ||+ B)	[ring-leader1__compatible]
Thm* x,y:. Dec(x = y)	[decidable__equal_nat]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 5

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html