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

1

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

3 steps

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