Def  == *

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]
Thm* i,a:Id, T:Type, ds:x: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 Thm* @i init: init Thm* @i action a:T Thm* @i precondition a(v) is Thm* @i P s v)  Thm* realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)	[pre-init-rule]
Thm* P:(UnitProp). Dec(P())  Dec(x:Unit. P(x))	[decidable__ex_unit]

In prior sections: core bool 1 mb event system 2 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