Def (x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])

is mentioned by

Thm* L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.B ||+ M)  (L) ||+ M)	[ma-join-list-compat2]
Thm* L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-compat]
Thm* L:MsgA List. (A,BL.A ||+ B)  (AL.Feasible(A))  Feasible((L))	[ma-join-list-feasible]
Thm* L:MsgA List, M:MsgA. (A,BL.A ||+ B)  (M  L)  M  (L)	[ma-sub-join-list]
Thm* L:MsgA List. (A,BL.A ||+ B)  (L)  MsgA	[ma-join-list_wf]
Thm* L:MsgA List.  Thm* (A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-property]

In prior sections: mb event system 1

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