is mentioned by

Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg)) Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List. Thm* (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i))	[ma-send-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x). Thm* (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w))	[ma-ef-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (a:Id, s:M2.state. Thm* (a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s))	[ma-npre-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v))	[ma-pre-sub]
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if (l; tg)) Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List. Thm* M.send(k;l;s;v;ms;i)  Prop	[ma-send_wf]
Thm* M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). Thm* M.ef(k,x,s,v,w)  Prop	[ma-ef_wf]
Thm* M:MsgA, a:Id, s:M.state, v:M.da(locl(a)). M.pre(a,s,v)  Prop	[ma-pre_wf]
Thm* M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s)  Prop	[ma-npre_wf]

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