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)
5. e : E
6. e':E. loc(e') = loc(e)  e' <c e
7. e' : E
8. loc(e') = loc(e)  e' <c e
  e' <loc e

By:	((RWO ((Thm* the_w:World, e,e':E. ((Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e') ((0) (THEN ((Analyze 0)) THEN ThinTrivial

None

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