Def Dconstant(loc;T;c;x;i)
Def == if loc = i [x : T initially x = c; only members of nil affect x :T]
Def == else nil fi

is mentioned by

Thm* c:T, x,i:Id. Thm* loc.(Dconstant(loc;T;c;x;i))  Thm* realizes es.e@i.(x when e) = c  T	[Dconstant__realizes]
Thm* c:T, x,i:Id. d-feasible(loc.(Dconstant(loc;T;c;x;i)))	[Dconstant__feasible]
Thm* loc:Id, T:Type, c:T, x,i:Id. (A,BDconstant(loc;T;c;x;i).A ||+ B)	[Dconstant__compatible]
Def ring-leader1(loc;R;uid;out;in) Def == if R(loc) Def == if [(send-once(loc;;;"send-me";x.x;"vote";out(loc);"me"));  Def == if [(trigger1(loc;;;x,y. x=y;loc;rcv Def == if [((in(loc)); "vote");"leader";"me"));  Def == if [(Dconstant(loc;;uid(loc);"me";loc));  Def == if [ma-single-sends1(; Def == if [ma-single-sends1(; Def == if [ma-single-sends1(; Def == if [ma-single-sends1("me"; Def == if [ma-single-sends1(rcv((in(loc)); "vote"); Def == if [ma-single-sends1((out(loc)); Def == if [ma-single-sends1("vote"; Def == if [ma-single-sends1((a,b. if a<b [b] else nil fi));  Def == if [only [rcv((in(loc)); "vote");  Def == if [only [locl("send-me")] sends on (out(loc) with "vote")] Def == else nil fi	[ring-leader1]

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