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. loc(e') = loc(e)  e' <c e)
5. e:E. first(e)  pred(e) <loc e & (e':E. (pred(e) <loc e' & e' <loc e))
  e:E. 
  first(e)
  
  loc(pred(e)) = loc(e)  Id & pred(e) <c e
  & (e':E. loc(e') = loc(e)  Id  (pred(e) <c e' & e' <c e))

By:	(RepeatFor 3 (ParallelOp -1) (THEN (RWO (Thm* the_w:World, e,e':E. (Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e') (-1 (THEN (Analyze 0) THEN (InstHyp [e'] -4) THEN (Analyze -1)

1

6. e : E 7. first(e) 8. e':E.  8. (loc(pred(e)) = loc(e')  Id & pred(e) <c e' 8. (& loc(e') = loc(e)  Id 8. (& e' <c e) 9. e' : E 10. loc(e') = loc(e)  Id 11. pred(e) <c e' 12. e' <c e   loc(pred(e)) = loc(e')  Id

2 steps

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