(248steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: world-event-system 2 2
1. the_w : World
2. FairFifo
3. e,e':E. loc(e) = loc(e')  e <c e'  e = e'  e' <c e
4. e:E. first(e)  (e':E. e' <loc e)
  e:E. first(e)  (e':E. loc(e') = loc(e)  Id  e' <c e)
By: ParallelOp -1 THEN ParallelOp -1 THEN ParallelOp -1

Generated subgoals:

1 5. e : E
6. first(e)
7. e':E. e' <loc e
8. e' : E
9. e' <loc e
  loc(e') = loc(e)  Id  e' <c e
1 step
2 5. e : E
6. e':E. loc(e') = loc(e)  Id  e' <c e
7. e' : E
8. loc(e') = loc(e)  Id  e' <c e
  e' <loc e
1 step

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

(248steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc