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

(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 2 1 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

first(e)

By:	RWO Thm* the_w:World, e:E. first(e) (t':. t'<time(e) isnull(a(loc(e);t'))) 0 THEN SupposeNot THEN InstHyp [<loc(e),t'>] -4

Generated subgoals:

1 6. t' :
7. t'<time(e)
8. isnull(a(loc(e);t'))
<loc(e),t'> E
1 step

2 6. t' :
7. t'<time(e)
8. isnull(a(loc(e);t'))
9. <loc(e),t'> <loc e
isnull(a(loc(e);t'))
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	6. t' : 7. t'<time(e) 8. isnull(a(loc(e);t')) <loc(e),t'> E	1 step
2	6. t' : 7. t'<time(e) 8. isnull(a(loc(e);t')) 9. <loc(e),t'> <loc e isnull(a(loc(e);t'))	1 step