IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
world-event-system31112 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:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html