mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def (x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])

is mentioned by

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* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id.
Thm* A
Thm* 
Thm* T
Thm* 
Thm* x = "trigger"
Thm* 
Thm* locl(a) = k  (A,Btrigger1(loc;T;A;P;i;k;a;x).A ||+ B)		[trigger1__compatible]
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  (A,Brecognizer1(loc;T;A;P;k;i;r;x).A ||+ B)		[recognizer1__compatible]
Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id.
Thm* "done" = x  A  T  (A,Bsend-once(loc;T;A;a;f;tg;l;x).A ||+ B)		[send-once__compatible]
Thm* loc,a,i:Id. (A,Bonce(loc;a;i).A ||+ B)[once__compatible]
Thm* loc:Id, T:Type, c:T, x,i:Id. (A,BDconstant(loc;T;c;x;i).A ||+ B)[Dconstant__compatible]

In prior sections: mb event system 1 mb event system 6

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

mb event system 7 Sections EventSystems Doc