mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def (with ds: ds
Def (init: init
Def action a:T
Def aprecondition a(v) is
Def aP)
Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )

is mentioned by

Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp),
Thm* init:x:Id fp-> ds(x)?Void.
Thm* (x:Id. x  dom(ds)  x  dom(init))
Thm* 
Thm* @i: (with ds: ds init: initaction a:T precondition a(v) is P)  Dsys
Thm* & (D:Dsys. 
Thm* & (@i: (with ds: ds
Thm* & (@init: init
Thm* & (action a:T
Thm* & (aprecondition a(v) is
Thm* & (aP)  D
Thm* & (
Thm* & (D 
Thm* & (realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id))		[s-pre-init-rule]

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

mb event system 6 Sections EventSystems Doc