Nuprl - Proof: world-event-system 3 1

(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. 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)

e:E.

first(e)

pred(e) <loc e & (

e':E.

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

By:	Assert (t:, i:Id. (first(<i,t>) ( (pred(<i,t>) <loc <i,t> & (e':E. (pred(<i,t>) <loc e' & e' <loc <i,t>)))

Generated subgoals:

1   t:, i:Id.
  first(<i,t>)

  pred(<i,t>) <loc <i,t> & (e':E. (pred(<i,t>) <loc e' & e' <loc <i,t>))
19 steps

2 5. t:, 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))
1 step

About:

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

1	t:, i:Id. first(<i,t>) pred(<i,t>) <loc <i,t> & (e':E. (pred(<i,t>) <loc e' & e' <loc <i,t>))	19 steps
2	5. t:, 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))	1 step