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

By:	(Analyze 0) THEN (Unfold `w-locl` -1) THEN (RWO (Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t'))) (-3) THEN (InstHyp [time(e')] -3)

1

5. t':. t'<time(e)  isnull(a(loc(e);t')) 6. e' : E 7. loc(e') = loc(e)  Id 8. time(e')<time(e) 9. isnull(a(loc(e);time(e')))   False

1 step

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