(248steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: world-event-system 3 1 1 1 2

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. t : 
6. 0<t
7. i:Id. 
7. first(<i,t-1>)
7. 
7. pred(<i,t-1>) <loc <i,t-1>
7. & (e':E. (pred(<i,t-1>) <loc e' & e' <loc <i,t-1>))
8. t = 0
9. i : Id
10. isnull(a(i;t-1))
  false  <i,t-1> <loc <i,t> & (e':E. (<i,t-1> <loc e' & e' <loc <i,t>))


By: Unfold `w-locl` 0 THEN Reduce 0 THEN Analyze 0


Generated subgoals:

None

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

(248steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc