Nuprl - Proof: better-w-match-exists 2 1 2 1 1 1 1 2 2 1 4

(43steps 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: better-w-match-exists 2 1 2 1 1 1 1 2 2 1 4

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':

. t

t' & 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. r :

11. ||rcvs(lnk(kind(e));time(e))|| = r
12. ms : Msg
13. msg(a(loc(e);time(e))) = ms
14. l : IdLnk
15. lnk(kind(e)) = l
16. t' :

17. time(e) = t'
18. r<||snds(l;t')||
19. concat(map(

t1.m(l;t1);upto(t')))[r] = ms
20. m :

||map(

t1.m(l;t1);upto(t'))||
21. ||snds(l;m)||

r
22. r-||snds(l;m)||<||map(

t1.m(l;t1);upto(t'))[m]||
23. snds(l;t')[r] = map(

t1.m(l;t1);upto(t'))[m][(r-||snds(l;m)||)]
24. m<t'
25. t :

t'
26. (||snds(l;t)||

(r<

||snds(l;t)||+||onlnk(l;m(source(l);t))||)
27. m(source(l);t) = m(source(l);t)
28. {m:Msg(the_w.M)| source(mlnk(m)) = source(l) } List
29. {m:Msg(the_w.M)| source(mlnk(m)) = source(l) } List
30. u : {m:Msg(the_w.M)| source(mlnk(m)) = source(l) }