Nuprl - Proof: world-event-system 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: world-event-system 2

1. the_w : World
2. FairFifo
3.

e,e':E. loc(e) = loc(e')

e <c e'

e = e'

e' <c e

e:E. first(e)

(

e':E. loc(e') = loc(e)

e' <c e)

By:	Assert (e:E. first(e) (e':E. e' <loc e))

Generated subgoals:

1   e:E. first(e)  (e':E. e' <loc e)
6 steps

2 4. e:E. first(e)  (e':E. e' <loc e)
  e:E. first(e)  (e':E. loc(e') = loc(e)  Id  e' <c e)
3 steps

About:

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

1	e:E. first(e) (e':E. e' <loc e)	6 steps
2	4. e:E. first(e) (e':E. e' <loc e) e:E. first(e) (e':E. loc(e') = loc(e) Id e' <c e)	3 steps