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 == ,>

is mentioned by

Def D realizes2 es.P(es) == w:World, p:FairFifo. PossibleWorld(D;w)  P(ES(w))	[d-realizes2]
Def D  Def realizes es.P(es) Def == D':Dsys.  Def == D  D'  (w:World, p:FairFifo. PossibleWorld(D';w)  P(ES(w)))	[d-realizes]
Def es is an event system of D Def == w:World, p:FairFifo. PossibleWorld(D;w) & es = ES(w)  ES	[d-es]

In prior sections: mb event system 3

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