Def es is an event system of D
Def == w:World, p:FairFifo. PossibleWorld(D;w) & es = ES(w)  ES

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]

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