1. D : Dsys
2. {es:ES| es is an event system of D }Prop
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 }

1

ES(w;p) is an event system of D

2 steps

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