Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))

is mentioned by

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* xdom(ds). A=ds(x)   A Thm*  Thm* kdom(da). A=da(k)   A  Feasible(ma-single-sends(ds; da; k; l; f))	[ma-single-sends-feasible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* T Thm*  Thm* xdom(ds). A=ds(x)   A Thm*  Thm* (s:State(ds). Dec(v:T. P(s,v))) Thm*  Thm* Feasible((with ds: ds Thm* Faction a:T Thm* Fprecondition a(v) is Thm* FP s v))	[ma-single-pre-feasible]
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* xdom(ds). A=ds(x)   A Thm*  Thm* kdom(da). A=da(k)   A  Feasible(ma-single-effect(ds; da; k; x; f))	[ma-single-effect-feasible]

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