is mentioned by

Thm* A:MsgA. A ||	[ma-empty-compatible-right]
Thm* A:MsgA.  || A	[ma-empty-compatible-left]
Thm* M:MsgA.   M	[ma-empty-sub]
Thm* ma-is-empty()	[ma-empty-is-empty]
Thm* M:MsgA. ma-is-empty(M)  M =   MsgA	[assert-ma-is-empty]
Def @i (with ds: ds init: init action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) Def == if (with ds: ds Def == if (init: init Def == if action a:T Def == if aprecondition a(v) is Def == if aP) Def == else  fi	[d-single-pre-init]
Def @i (with ds: ds action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) (with ds: ds action a:T precondition a(v) is P s v) Def == else  fi	[d-single-pre]
Def d-single-sends(i; ds; da; k; l; f)(j) Def == if eqof(IdDeq)(j,i) ma-single-sends(ds; da; k; l; f) else  fi	[d-single-sends]
Def d-single-effect(i; ds; da; k; x; f)(j) Def == if eqof(IdDeq)(j,i) ma-single-effect(ds; da; k; x; f) else  fi	[d-single-effect]
Def @i: only L sends on (l with tg)(j) Def == if eqof(IdDeq)(j,i) only L sends on (l with tg) else  fi	[d-single-sframe]
Def @i: only L affects x : t(j) Def == if eqof(IdDeq)(j,i) only members of L affect x :t else  fi	[d-single-frame]
Def @i: x:T initially x = v(j) Def == if eqof(IdDeq)(j,i) x : T initially x = v else  fi	[d-single-init]

In prior sections: mb event system 4

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