Def ES
Def == E:Type
Def == EqDecider(E)(T:IdIdType
Def == EqDecider(E)(V:IdIdType
Def == EqDecider(E)(M:IdLnkIdType
Def == EqDecider(E)(Top(loc:EId
Def == EqDecider(E)(Top(kind:EKnd
Def == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e))
Def == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x))
Def == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x))
Def == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List))
Def == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E
Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends
Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e))
Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||)
Def == EqDecider(E)(Top(first:E
Def == EqDecider(E)(Top(pred:{e':E| (first(e')) }E
Def == EqDecider(E)(Top(causl:EEProp
Def == EqDecider(E)(Top(ESAxioms{i:l}
Def == EqDecider(E)(Top(ESAxioms(E;
Def == EqDecider(E)(Top(ESAxioms(T;
Def == EqDecider(E)(Top(ESAxioms(M;
Def == EqDecider(E)(Top(ESAxioms(loc;
Def == EqDecider(E)(Top(ESAxioms(kind;
Def == EqDecider(E)(Top(ESAxioms(val;
Def == EqDecider(E)(Top(ESAxioms(when;
Def == EqDecider(E)(Top(ESAxioms(after;
Def == EqDecider(E)(Top(ESAxioms(sends;
Def == EqDecider(E)(Top(ESAxioms(sender;
Def == EqDecider(E)(Top(ESAxioms(index;
Def == EqDecider(E)(Top(ESAxioms(first;
Def == EqDecider(E)(Top(ESAxioms(pred;
Def == EqDecider(E)(Top(ESAxioms(causl)
Def == EqDecider(E)(Top(Top))

is mentioned by

Thm* D,D':Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes es.P(es)  D  D'  D' realizes es.P(es)	[realizes-monotone-wrt-sub]
Thm* D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes2 es.P(es)  D realizes es.P(es)	[d-realizes2-implies-realizes]
Thm* D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes2 es.P(es)  Prop{i''}	[d-realizes2_wf]
Thm* D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes es.P(es)  Prop{i''}	[d-realizes_wf]
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 2 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