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

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.  Thm* FairFifo Thm*  Thm* ESAxioms{i:l} Thm* ESAxioms(E; Thm* ESAxioms((i,x. vartype(i;x)); Thm* ESAxioms(the_w.M; Thm* ESAxioms((e.loc(e)); Thm* ESAxioms((e.kind(e)); Thm* ESAxioms((e.val(e)); Thm* ESAxioms((x,e. (x when e)); Thm* ESAxioms((x,e. (x after e)); Thm* ESAxioms((l,e. sends(l;e)); Thm* ESAxioms((e.sender(e)); Thm* ESAxioms((e.index(e)); Thm* ESAxioms((e.first(e)); Thm* ESAxioms((e.pred(e)); Thm* ESAxioms((e,e'. e <c e'))	[world-event-system]
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, e,e':E. FairFifo  e <c e'  time(e)<time(e')	[w-causl-time]
Thm* the_w:World, e:E. Thm* FairFifo  isrcv(kind(e))  index(e)  ||sends(lnk(kind(e));sender(e))||	[w-index_wf]
Thm* the_w:World, e:E. FairFifo  isrcv(kind(e))  sender(e)  E	[w-sender_wf]
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, e:E. Thm* FairFifo Thm*  Thm* isrcv(kind(e)) Thm*  Thm* (t:time(e).  Thm* (match(lnk(kind(e));t;time(e)) 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)	[better-w-match-exists]
Thm* the_w:World, e:E. Thm* FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))	[w-match-exists]
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, e:E. first(e)  pred(e)  E	[w-pred_wf]
Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E	[w-pred-aux]
Thm* the_w:World, e:E. <loc(e),time(e)> ~ e	[w-loc-time]
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. first(e)	[w-first_wf]
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, e:E. val(e)  V(loc(e);kind(e))	[w-eval_wf]
Thm* the_w:World, i:Id, k:Knd. V(i;k)  Type	[w-V_wf]
Thm* the_w:World, e:E. kind(e)  Knd	[w-ekind_wf]
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, e,e':E. e = e'  e = e'	[assert-w-eq-E-iff]
Thm* the_w:World, e,e':E. e = e'  e = e'	[assert-w-eq-E]
Thm* the_w:World. FairFifo  Prop	[fair-fifo_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, 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, l:IdLnk, mss:Msg List. onlnk(l;mss)  Msg List	[w-onlnk_wf]
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. Msg  Type	[w-Msg_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]

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