Nuprl - Proof: world-event-system 3 1 2

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

, i:Id.
5.

first(<i,t>)
5.

5. pred(<i,t>) <loc <i,t> & (

e':E.

(pred(<i,t>) <loc e' & e' <loc <i,t>))

e:E.

first(e)

pred(e) <loc e & (

e':E.

(pred(e) <loc e' & e' <loc e))

By:	RepeatFor 2 (Analyze 0) THEN InstHyp [time(e);loc(e)] 5 THEN All (RWO Thm* the_w:World, e:E. <loc(e),time(e)> ~ e)

Generated subgoals:

None

About:

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