Nuprl - Proof: w-causl-time 1

(17steps 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: w-causl-time 1

1. the_w : World
2. e : E
3. e' : E
4. FairFifo
5. e <c e'

time(e)<time(e')

By:	Unfold `w-causl` -1 THEN Unfold `rel_plus` -1 THEN Reduce -1 THEN Assert (n:, e,e':E. ((e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e')^n e') ( (time(e)<time(e'))

Generated subgoals:

1 5. n:. e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n e'
  n:, e,e':E.
  (e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n e')

  time(e)<time(e')
14 steps

2 5. n:. e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n e'
6. n:, e,e':E.
6. (e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n e')
6.
6. time(e)<time(e')
  time(e)<time(e')
1 step

About:

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

(17steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

1	5. n:. e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^n e' n:, e,e':E. (e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^n e') time(e)<time(e')	14 steps
2	5. n:. e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^n e' 6. n:, e,e':E. 6. (e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^n e') 6. 6. time(e)<time(e') time(e)<time(e')	1 step