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

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

1. the_w : World
2. FairFifo
3. e : E
4. e' : E
5. loc(e) = loc(e')
6. e <c e'

e <loc e'
7. e' <c e

e' <loc e

e <loc e'

e = e'

e' <loc e

By:	Unfold `w-locl` 0 THEN Decide (time(e)<time(e')) THENL [OrLeft;OrRight] THEN Decide (time(e')<time(e)) THENL [OrRight;OrLeft]

Generated subgoal:

1 6. e <c e'  e <loc e'
7. e <c e'  e <loc e'
8. e' <c e  e' <loc e
9. e' <c e  e' <loc e
10. time(e)<time(e')
11. time(e')<time(e)
  e = e'
2 steps

About:

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