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

1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))
5. n:. match(lnk(kind(e));n;time(e))
6. match(lnk(kind(e));mu(t.match(lnk(kind(e));t;time(e)));time(e))
7. i:
7. i<mu(t.match(lnk(kind(e));t;time(e)))  match(lnk(kind(e));i;time(e))
  isnull(a(source(lnk(kind(e)));mu(t.match(lnk(kind(e));t;time(e)))))


By: Thin -1 THEN MoveToConcl -1
THEN
GenConcl (mu(t.match(lnk(kind(e));t;time(e))) = t)
THENA
(Auto THEN Reduce 0)
THEN
Thin -1
THEN
GenConcl (lnk(kind(e)) = l)
THEN
Thin -1


Generated subgoal:

1 6. t : 
7. l : IdLnk
  match(l;t;time(e))  isnull(a(source(l);t))

3 steps

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