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)