D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
  D realizes2 es.P(es)  Prop{i''}

1

1. D : Dsys 2. {es:ES| es is an event system of D }Prop{i'} 3. w : World 4. p : FairFifo 5. PossibleWorld(D;w)   ES(w;p)  {es:ES| es is an event system of D }

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html