Def IdLnk == IdId

is mentioned by

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, l:IdLnk, e:E. sends(l;e)  Msg_sub(l; the_w.M) List	[better-w-sends-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, l:IdLnk, t:. m(l;t)  Msg List	[w-ml_wf]
Thm* the_w:World, l:IdLnk, mss:Msg List. Thm* withlnk(l;mss)  (t:Idthe_w.M(l,t)) List	[w-withlnk_wf]
Thm* w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||	[w-onlnk-m]
Thm* the_w:World, l:IdLnk, mss:Msg List. onlnk(l;mss)  Msg List	[w-onlnk_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* w:World. w.M  IdLnkIdType	[w-M_wf]
Thm* i:Id, TA:(IdIdType), M:(IdLnkIdType). Thm* w-action-dec(TA;M;i)  KndType	[w-action-dec_wf]
Thm* es:ES, l:IdLnk, tg:Id, e:E. Thm* kind(e) = rcv(l; tg) Thm*  Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)	[es-kind-rcv]
Thm* es:ES, l:IdLnk, tg:Id, e:E. Thm* isrcv(e)  lnk(e) = l  tag(e) = tg  kind(e) = rcv(l; tg)	[es-rcv-kind]
Thm* the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e)  (Msg on l) List	[es-tg-sends_wf]
Thm* the_es:ES, m:Msg. mlnk(m)  IdLnk	[mlnk_wf2]
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: 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