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* 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* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi	[fpf-join-cap-sq]
Thm* eq:EqDecider(A), ds:x:A fp-> Type, x:A. ds(x)?Void r ds(x)?Top	[fpf-cap-void-subtype]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)	[subtype-fpf-cap-top]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type. g  f  (x:X. f(x)?Top r g(x)?Top)	[subtype-fpf-cap]
Thm* B:(AType), f:a:A fp-> B(a). f  a:A fp-> Top	[fpf-trivial-subtype-top]

In prior sections: mb list 1 mb event system 1 mb event system 3 mb event system 4 mb basic mb event system 2

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