Def (L) == reduce(A,B. A  B;;L)

is mentioned by

Thm* l:IdLnk, tg:Id, L:MsgA List. Thm* (ML.T r M.din(l,tg))  (T r (L).din(l,tg))	[sub-join-list-din]
Thm* L:MsgA List, P:(IdLnkIdTypeProp), i:Id. Thm* (ML.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks((L);i).P(ltg))	[ma-outlinks-join-list]
Thm* L:MsgA List. ma-is-empty((L))  reduce(M,x. ma-is-empty(M) & x;True;L)	[assert-ma-join-list-is-empty]
Thm* L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)	[ma-join-list-is-empty]
Thm* L:MsgA List. ma-is-empty((L))	[ma-is-empty_wf_join]
Thm* L:MsgA List. (L)  MsgAForm	[msg-form-join-list]
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.  Thm* (A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-property]

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