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))
6. e : E
7. first(e)
8. e':E. (loc(pred(e)) = loc(e') & pred(e) <c e' & loc(e') = loc(e) & e' <c e)
9. e' : E
10. loc(e') = loc(e)
11. pred(e) <c e'
12. e' <c e
13. pred(e) <loc e
14. e':E. (pred(e) <loc e' & e' <loc e)
  loc(pred(e)) = loc(e')  Id

By:	RWO Thm* the_w:World, e,e':E. Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e') -2

None

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