(7steps 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-sender wf
  the_w:World, e:E. FairFifo  isrcv(kind(e))  sender(e)  E
By: Auto THEN Assert (n:. match(lnk(kind(e));n;time(e)))

Generated subgoals:

1 1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))
  n:. match(lnk(kind(e));n;time(e))
1 step
2 1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))
5. n:. match(lnk(kind(e));n;time(e))
  sender(e)  E
5 steps

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

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