is mentioned by

Thm* D,D':Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes es.P(es)  D  D'  D' realizes es.P(es)	[realizes-monotone-wrt-sub]
Thm* A,B,C:MsgA. Thm* A || B Thm*  Thm* ma-frame-compatible(A; B) Thm*  Thm* ma-sframe-compatible(A; B) Thm*  Thm* C || A Thm*  Thm* ma-frame-compatible(C; A) Thm*  Thm* ma-sframe-compatible(C; A) Thm*  Thm* C || B Thm*  Thm* ma-frame-compatible(C; B) Thm*  Thm* ma-sframe-compatible(C; B) Thm*  Thm* C || A  B & ma-frame-compatible(C; A  B) & ma-sframe-compatible(C; A  B)	[ma-compatible-join]

In prior sections: core well fnd int 1 bool 1 int 2 list 1 rel 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 5 sqequal 1

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