mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )

is mentioned by

Thm* x:Id, t,v:Top, x1:Id, t1,v1:Top.
Thm* x = x1  x : t initially x = v ||+ x1 : t1 initially x1 = v1		[ma-single-init-ma-single-init-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top.
Thm* x : t || x1 : t1
Thm* 
Thm* x1 : t1 initially x1 = v ||+ only members of L affect x :t		[ma-single-init-ma-single-frame-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top.
Thm* x : t || x1 : t1
Thm* 
Thm* only members of L affect x :t ||+ x1 : t1 initially x1 = v		[ma-single-frame-ma-single-init-compatible]
Thm* l:IdLnk, tg:Id, L:Top, x:Id, t,v:Top.
Thm* x : t initially x = v ||+ only L sends on (l with tg)		[ma-single-init-ma-single-sframe-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type,
Thm* v:t.
Thm* ds || x1 : t
Thm* 
Thm* x1 : t initially x1 = v ||+ ma-single-effect(ds; da; k; x; f)		[ma-single-init-ma-single-effect-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type,
Thm* v:t.
Thm* ds || x1 : t
Thm* 
Thm* ma-single-effect(ds; da; k; x; f) ||+ x1 : t initially x1 = v		[ma-single-effect-ma-single-init-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List,
Thm* x:Id, t:Type, v:t.
Thm* ds || x : t  x : t initially x = v ||+ ma-single-sends(ds; da; k; l; f)		[ma-single-init-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List,
Thm* x:Id, t:Type, v:t.
Thm* ds || x : t  ma-single-sends(ds; da; k; l; f) ||+ x : t initially x = v		[ma-single-sends-ma-single-init-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t.
Thm* ds || x : t
Thm* 
Thm* x : t initially x = v ||+ (with ds: ds
Thm* xaction a:T
Thm* xprecondition a(v) is
Thm* xP s v)		[ma-single-init-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t.
Thm* ds || x : t
Thm* 
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ x : t initially x = v		[ma-single-pre-ma-single-init-compatible]
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* i:Id, T:Type, v:T, x:Id.
Thm* @i: x : T initially x = v  Dsys
Thm* & (D:Dsys. 
Thm* & (@i: x : T initially x = v  D
Thm* & (
Thm* & (D 
Thm* & (realizes es.(vartype(i;x) r T)
Thm* & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T))		[s-init-rule]
Def recognizer1(loc;T;A;P;k;i;r;x)
Def == if loc = i
Def == if [r :  initially r = false; 
Def == if [only members of [k] affect r :; 
Def == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)]
Def == else nil fi		[recognizer1]
Def Dconstant(loc;T;c;x;i)
Def == if loc = i [x : T initially x = c; only members of nil affect x :T]
Def == else nil fi		[Dconstant]

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 7 Sections EventSystems Doc