is mentioned by

Thm* i,x:Id, k:Knd, ds:a:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* @i: ma-single-effect(ds; da; k; x; f)  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-effect(ds; da; k; x; f)  D Thm* & ( Thm* & (D  Thm* & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k  Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((x after e) = f((z.(z when e)),val(e))  ds(x)?Top))

[s-effect-rule]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* xdom(ds). A=ds(x)   A Thm*  Thm* kdom(da). A=da(k)   A  Feasible(ma-single-effect(ds; da; k; x; f))

[ma-single-effect-feasible]

In prior sections: mb event system 4 mb event system 5

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