mb event system 7 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* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> ds(x)?Void, x:Id,
Thm* t:Type, v:t.
Thm* ds || x : t
Thm* 
Thm* (x  dom(init)  init(x) = v  t)
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ x : t initially x = v		[ma-single-pre-init-ma-single-init-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id,
Thm* L:Knd List, t:Type.
Thm* ds || x : t
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ only members of L affect x :t		[ma-single-pre-init-ma-single-frame-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Top, P:Top, init:x:Id fp-> Top, l:IdLnk, tg:Id,
Thm* L:Knd List.
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ only L sends on (l with tg)		[ma-single-pre-init-ma-single-sframe-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd,
Thm* d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-effect(d1; da; k; x; f)		[ma-single-pre-init-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd,
Thm* l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-sends(d1; da; k; l; f)		[ma-single-pre-init-ma-single-sends-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top,
Thm* d1:x:Id fp-> Type, P1:Top.
Thm* ds || d1
Thm* 
Thm* a = a1
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ (with ds: d1
Thm* aaction a1:T1
Thm* aprecondition a1(v) is
Thm* aP1 s v)		[ma-single-pre-init-ma-single-pre-compatible]

In prior sections: mb event system 6 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 7 Sections EventSystems Doc