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. t':. t'<time(e)  isnull(a(loc(e);t'))
6. e' : E
7. loc(e') = loc(e)
8. time(e')<time(e)
9. isnull(a(loc(e);time(e')))
  False

By:	((RevHypSubst -3 -1) (THEN ((Inst Thm* the_w:World, e:E. isnull(act(e)) [the_w;e']) (THEN ((Analyze -1) (THEN ((Unfold `w-act` 0)) THEN NthHypSq -1 THEN RepeatFor 3 Analyze THEN Try (Unfolds [`w-loc`;`w-time`] 0) THEN Try Trivial

None

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