(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

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


By: AssertBY (||onlnk(l;m(source(l);t))||  )
(GenConclAtAddr [2;1;2] THEN Fold `w-Msg` -2 THEN Unfold `w-Msg` -1)
THEN
Unfold `fair-fifo` 3
THEN
Analyze 3
THEN
Analyze 4
THEN
Analyze 5
THEN
Analyze 0
THEN
Unfold `w-match` -1
THEN
RW assert_pushdownC -1


Generated subgoal:

1 3. i:Id, t:l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List
4. i:Id, t:.
4. isnull(a(i;t))
4. 
4. (x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List
5. i:Id, t:l:IdLnk.
5. isrcv(l;a(i;t))
5. 
5. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg
6. l:IdLnk, t:.
6. t':tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List
7. isrcv(kind(e))
8. n:. match(lnk(kind(e));n;time(e))
9. t : 
10. l : IdLnk
11. ||onlnk(l;m(source(l);t))||  
12. ||snds(l;t)||||rcvs(l;time(e))||
13. ||rcvs(l;time(e))||<||snds(l;t)||+||onlnk(l;m(source(l);t))||
  isnull(a(source(l);t))

2 steps

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