is mentioned by

Thm* i:Id, w:World, p:FairFifo, t:. Thm* isnull(a(i;t))  (valtype(<i,t>) ~ valtype(i;a(i;t)))	[es-valtype-w-valtype]
Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))	[assert-w-first]
Thm* the_w:World, e:E. isnull(act(e))	[w-act-not-null]
Thm* the_w:World, e:E. act(e)  {a:Action(loc(e))| isnull(a) }	[w-act_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, 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]
Def pred(e) Def == if isnull(a(loc(e);time(e)-1)) pred(<loc(e),time(e)-1>) Def == else <loc(e),time(e)-1> fi Def (recursive)	[w-pred]
Def first(e) Def == if time(e)=0 true Def == i; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>) Def == else false fi Def (recursive)	[w-first]
Def E == {p:(Id)| isnull(a(1of(p);2of(p))) }	[w-E]
Def FairFifo Def == (i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List) Def == & (i:Id, t:. Def == & (isnull(a(i;t)) Def == & ( Def == & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) Def == & (& m(i;t) = nil  Msg List) Def == & (i:Id, t:, l:IdLnk. Def == & (isrcv(l;a(i;t)) Def == & ( Def == & (destination(l) = i Def == & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg) Def == & (l:IdLnk, t:. Def == & (t':.  Def == & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)	[fair-fifo]
Def isrcv(l;a) == isnull(a)isrcv(kind(a))lnk(kind(a)) = l	[w-isrcvl]

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