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

1. the_w : World
2. FairFifo
3. e : E
4. e' : E
5. isrcv(kind(e'))
6. e = sender(e')
7. n : time(e')
8. match(lnk(kind(e'));n;time(e'))
9. match(lnk(kind(e'));mu(t.match(lnk(kind(e'));t;time(e')));time(e'))
10. i:
10. i<mu(t.match(lnk(kind(e'));t;time(e')))  match(lnk(kind(e'));i;time(e'))
11. time(sender(e'))n
  n<mu(t.match(lnk(kind(e'));t;time(e')))


By: Unfolds [`w-sender`;`w-time`] -1 THEN Reduce -1


Generated subgoal:

1 11. mu(t.match(lnk(kind(e'));t;time(e')))n
  n:. (t.match(lnk(kind(e'));t;time(e')))(n)

1 step

About:
assertnatural_numberless_thanlambdaapplyequalimpliesallexists
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