Def Id == Atom

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':E. Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e')	[w-locl-iff]
Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E	[w-pred-aux]
Thm* the_w:World, i:Id, t:. first(<i,t>)	[w-first-aux]
Thm* the_w:World, x:Id, e:E. (x after e)  vartype(loc(e);x)	[w-after_wf]
Thm* the_w:World, x:Id, e:E. (x when e)  vartype(loc(e);x)	[w-when_wf]
Thm* the_w:World, i:Id, k:Knd. V(i;k)  Type	[w-V_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, tg:Id, mss:Msg List. w-tagged(tg; mss)  Msg List	[w-tagged_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, 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]
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]
Thm* w:World. w.T  IdIdType	[w-T_wf]
Thm* w:World. w.TA  IdIdType	[w-TA_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* es:ES, x,i:Id, T:Type, c:T. Thm* (x,y:T. Dec(x = y  T)) Thm*  Thm* (vartype(i;x) r T) Thm*  Thm* (e:E. loc(e) = i  Id  first(e)  (x when e) = c  T) Thm*  Thm* (e':E.  Thm* (loc(e') = i  Id Thm* ( Thm* ((x after e') = c  T Thm* ( Thm* ((ev:E. ev  e'  & (x after ev) = (x when ev)  T))	[change-since-init]
Thm* es:ES, x,i:Id, T:Type. Thm* (x,y:T. Dec(x = y  T)) Thm*  Thm* (vartype(i;x) r T) Thm*  Thm* (e',e:E. Thm* (e  e'  Thm* ( Thm* (loc(e') = i  Id Thm* ( Thm* ((x after e') = (x when e)  T Thm* ( Thm* ((ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T))	[change-lemma]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). e@i.P(e)  Prop	[existse-at_wf]
Thm* es:ES, i,x:Id, T:Type, I:(TProp). Thm* (vartype(i;x) r T) & e@i.first(e)  I((x when e)) Thm*  Thm* e@i.I((x when e))  I((x after e))  @i always.I(x)	[es-invariant1]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). Thm* e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e)	[alle-at-iff]
Thm* es:ES, x:Id, e:E. Thm* first(e)  (x after pred(e)) = (x when e)  vartype(loc(e);x)	[es-after-pred]
Thm* the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e)  (Msg on l) List	[es-tg-sends_wf]
Thm* es:ES, e,e':E. [e, e']  {ev:E| loc(ev) = loc(e')  Id } List	[es-interval_wf2]
Thm* the_es:ES, m:Msg. mtag(m)  Id	[es-mtag_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 <loc e' == loc(e) = loc(e')  Id & time(e)<time(e')	[w-locl]
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]
Def e@i.P(e) == e:E. loc(e) = i  Id & P(e)	[existse-at]
Def e@i.P(e) == e:E. loc(e) = i  Id  P(e)	[alle-at]

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