(30steps 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-match-exists 2 1 1

1. the_w : World
2. e : E
3. i:Id, t:l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil
4. i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
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))
6. l:IdLnk, t:.
6. t':tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil
7. isrcv(kind(e))
8. isrcv(lnk(kind(e));a(loc(e);time(e)))
9. destination(lnk(kind(e))) = loc(e)
10. ||queue(lnk(kind(e));time(e))||1
10. & hd(queue(lnk(kind(e));time(e))) = msg(a(loc(e);time(e)))
  ||rcvs(lnk(kind(e));time(e))||<||snds(lnk(kind(e));time(e))||


By: ExRepD THEN Thin -1 THEN MoveToConcl -1 THEN Unfold `w-queue` 0
THEN
GenConcl (||rcvs(lnk(kind(e));time(e))|| = r)
THEN
GenConcl (snds(lnk(kind(e));time(e)) = L)


Generated subgoals:

1 10. L : Top List
11. snds(lnk(kind(e));time(e)) = L  Top List
  0||rcvs(lnk(kind(e));time(e))||

Auto
2 10. r : 
11. ||rcvs(lnk(kind(e));time(e))|| = r  
12. L : Top List
13. snds(lnk(kind(e));time(e)) = L  Top List
  ||nth_tl(r;L)|| r<||L||

1 step

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

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