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

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

e':E.

e' <loc e
6. t' :

7. t'<time(e)
8.

isnull(a(loc(e);t'))
9.

<loc(e),t'> <loc e

isnull(a(loc(e);t'))

By:	Analyze -1 THEN Unfold `w-locl` 0 THEN All (Unfolds [`w-time`;`w-loc`]) THEN Analyze 4 THEN Analyze 4 THEN All Reduce

Generated subgoals:

None

About:

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