Nuprl - Proof: w-causl-time 1 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

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

. e

e,e'. e <loc e'

isrcv(kind(e')) & e = sender(e')^n e'

, e,e':E.

e,e'. e <loc e'

isrcv(kind(e')) & e = sender(e')

E^n e')

time(e)<time(e')

By:	Thin -1 THEN Thin -2 THEN Thin -2 THEN Assert (e,z:E. e <loc z isrcv(kind(z)) & e = sender(z) time(e)<time(z))

Generated subgoals:

1 2. FairFifo
  e,z:E. e <loc z  isrcv(kind(z)) & e = sender(z)  E  time(e)<time(z)
8 steps

2 2. FairFifo
3. e,z:E. e <loc z  isrcv(kind(z)) & e = sender(z)  E  time(e)<time(z)
  n:, e,e':E.
  (e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n e')

  time(e)<time(e')
5 steps

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	2. FairFifo e,z:E. e <loc z isrcv(kind(z)) & e = sender(z) E time(e)<time(z)	8 steps
2	2. FairFifo 3. e,z:E. e <loc z isrcv(kind(z)) & e = sender(z) E time(e)<time(z) n:, e,e':E. (e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^n e') time(e)<time(e')	5 steps