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* A,B:Dsys. A  B  (w:World. PossibleWorld(B;w)  PossibleWorld(A;w))	[possible-world-monotonic]
Thm* D:Dsys, w:World. PossibleWorld(D;w)  Prop{i'}	[possible-world_wf]
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 mb event system 5

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