(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
  the_w:World, e:E.
  FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))
By: Auto THEN Unfold `fair-fifo` 3 THEN Assert isrcv(lnk(kind(e));a(loc(e);time(e)))

Generated subgoals:

1 1. the_w : World
2. e : E
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))
  isrcv(lnk(kind(e));a(loc(e);time(e)))
3 steps
2 1. the_w : World
2. e : E
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. isrcv(lnk(kind(e));a(loc(e);time(e)))
  t:time(e). match(lnk(kind(e));t;time(e))
26 steps

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