Def ESAxioms{i:l}
Def ESAxioms(E;
Def ESAxioms(T;
Def ESAxioms(M;
Def ESAxioms(loc;
Def ESAxioms(kind;
Def ESAxioms(val;
Def ESAxioms(when;
Def ESAxioms(after;
Def ESAxioms(sends;
Def ESAxioms(sender;
Def ESAxioms(index;
Def ESAxioms(first;
Def ESAxioms(pred;
Def ESAxioms(causl)
Def == (e,e':E. loc(e) = loc(e')  Id  causl(e,e')  e = e'  causl(e',e))
Def == & (e:E. (first(e))  (e':E. loc(e') = loc(e)  Id  causl(e',e)))
Def == & (e:E. 
Def == & ((first(e))
Def == & (
Def == & (loc(pred(e)) = loc(e)  Id & causl(pred(e),e)
Def == & (& (e':E. 
Def == & (& (loc(e') = loc(e)  Id  (causl(pred(e),e') & causl(e',e))))
Def == & (e:E. 
Def == & ((first(e))  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x)))
Def == & (Trans e,e':E. causl(e,e'))
Def == & SWellFounded(causl(e,e'))
Def == & (e:E. 
Def == & (isrcv(kind(e))
Def == & (
Def == & ((sends(lnk(kind(e)),sender(e)))[(index(e))]
Def == & (=
Def == & (msg(lnk(kind(e));tag(kind(e));val(e))
Def == & ( Msg(M))
Def == & (e:E. isrcv(kind(e))  causl(sender(e),e))
Def == & (e,e':E.
Def == & (causl(e,e')
Def == & (
Def == & ((first(e')) & causl(e,pred(e'))  e = pred(e')
Def == & ( isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e'))
Def == & (e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e))))
Def == & (e:E, l:IdLnk.
Def == & (loc(e) = source(l)  sends(l,e) = nil  Msg_sub(l; M) List)
Def == & (e,e':E.
Def == & (isrcv(kind(e))
Def == & (
Def == & (isrcv(kind(e'))
Def == & (
Def == & (lnk(kind(e)) = lnk(kind(e'))
Def == & (
Def == & ((causl(e,e')
Def == & ((
Def == & ((causl(sender(e),sender(e'))
Def == & (( sender(e) = sender(e')  E & index(e)<index(e')))
Def == & (e:E, l:IdLnk, n:||sends(l,e)||.
Def == & (e':E. 
Def == & (isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n)

is mentioned by

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]

In prior sections: mb event system 2

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