is mentioned by

Thm* the_w:World, e:E. act(e)  {a:Action(loc(e))| isnull(a) }	[w-act_wf]
Thm* the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a)  msg(a)  Msg	[w-msg_wf]
Thm* the_w:World, i:Id, t:. a(i;t)  Action(i)	[w-a_wf]
Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). Thm* isrcv(l;a)  isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l	[assert-w-isrcvl]
Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). isrcv(l;a)	[w-isrcvl_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  val(a)  valtype(i;a)	[w-val_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  valtype(i;a)  Type	[w-valtype_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  kind(a)  Knd	[w-kind_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)	[w-isnull_wf]

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