Def  == {i:| 0i }

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, t:. Thm* FairFifo Thm*  Thm* isrcv(kind(e)) Thm*  Thm* match(lnk(kind(e));t;time(e)) Thm*  Thm* onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))|| Thm* -||snds(lnk(kind(e));t)||)] Thm* = Thm* msg(a(loc(e);time(e))) Thm*  Msg	[w-match-property]
Thm* the_w:World, e:E, t,t':. Thm* FairFifo Thm*  Thm* isrcv(kind(e)) Thm*  Thm* match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'	[w-match-unique]
Thm* the_w:World, l:IdLnk, t,t':. Thm* match(l;t;t') Thm*  Thm* ||snds(l;t)||||rcvs(l;t')|| Thm* & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||	[assert-w-match]
Thm* the_w:World, l:IdLnk, t,t':. match(l;t;t')	[w-match_wf]
Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E	[w-pred-aux]
Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))	[assert-w-first]
Thm* the_w:World, i:Id, t:. first(<i,t>)	[w-first-aux]
Thm* the_w:World, l:IdLnk, t:. m(l;t)  Msg List	[w-ml_wf]
Thm* w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||	[w-onlnk-m]
Thm* the_w:World, i:Id, t:. Thm* m(i;t)  {m:Msg(the_w.M)| source(mlnk(m)) = i } List	[w-m_wf]
Thm* the_w:World, i:Id, t:. a(i;t)  Action(i)	[w-a_wf]
Thm* the_w:World, i:Id, t:, x:Id. s(i;t).x  vartype(i;x)	[w-s_wf]
Def ES(the_w;p) Def == <E Def == ,product-deq(Id;;IdDeq;NatDeq) Def == ,(i,x. vartype(i;x)) Def == ,(i,a. V(i;locl(a))) Def == ,the_w.M Def == , Def == ,(e.loc(e)) Def == ,(e.kind(e)) Def == ,(e.val(e)) Def == ,(x,e. (x when e)) Def == ,(x,e. (x after e)) Def == ,(l,e. sends(l;e)) Def == ,(e.sender(e)) Def == ,(e.index(e)) Def == ,(e.first(e)) Def == ,(e.pred(e)) Def == ,(e,e'. e <c e') Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p) Def == ,>	[w-es]
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 World Def == T:IdIdType Def == TA:IdIdType Def == M:IdLnkIdType Def == (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i))) Def == (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top	[world]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2

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