is mentioned by

Thm* i,a,x:Id, A,T:Type, P:(ATProp). Thm* @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r A) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T)) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& ((kind(e) = locl(a)  Knd  P((x when e),val(e))) Thm* & (realizes es.& (& (e':E.  Thm* & (realizes es.& (& ((e <loc e')  e = e'  E Thm* & (realizes es.& (& (& kind(e') = locl(a)  Knd Thm* & (realizes es.& (& (&  (v:T. P((x after e'),v)))))	[s-pre-rule1]
Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp). Thm* @i: (with ds: ds action a:T precondition a(v) is P s v)  Dsys Thm* & (D:Dsys.  Thm* & (@i: (with ds: ds Thm* & (@action a:T Thm* & (@precondition a(v) is Thm* & (@P s v)  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.& (kind(e) = locl(a)  Knd  (valtype(e) r T)) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e))) Thm* & (realizes es.& (& (e':E.  Thm* & (realizes es.& (& ((e <loc e')  e = e'  E Thm* & (realizes es.& (& (& kind(e') = locl(a)  Knd Thm* & (realizes es.& (& (&  (v:T. P((z.(z after e')),v)))))	[s-pre-rule]
Thm* i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* @i (with ds: ds Thm* @i action a:T Thm* @i precondition a(v) is Thm* @i P s v)  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.& (kind(e) = locl(a)  Knd  (valtype(e) r T)) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id Thm* realizes es.& ( Thm* realizes es.& ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e))) Thm* realizes es.& (& (e':E.  Thm* realizes es.& (& ((e <loc e')  e = e'  E Thm* realizes es.& (& (& kind(e') = locl(a)  Knd Thm* realizes es.& (& (&  (v:T. P((z.(z after e')),v))))	[pre-rule]

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

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