Nuprl - Proof: world-event-system 2 1

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

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.

e' <loc e)

By:

Analyze 0

Generated subgoals:

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

2 4. e : E
5. e':E. e' <loc e
first(e)
3 steps

About:

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

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