Def State(ds) == x:Idds(x)?Top

is mentioned by

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* (with ds: ds action a:T precondition a(v) is P s v)  MsgA	[ma-single-pre_wf]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* ma-single-effect(ds; da; k; x; f)  MsgA	[ma-single-effect_wf]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  State(ds')  State(ds)	[ma-state-subtype2]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  (State(ds') r State(ds))	[ma-state-subtype]

In prior sections: mb event system 4

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