2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. f : A
B(T List)
9. rcv(l; tg) = k
T = B
10. @source(l): ma-single-sends(x : A;
10. @source(l): ma-single-sends(k : B
rcv(l; tg) : T;
10. @source(l): ma-single-sends(k;
10. @source(l): ma-single-sends(l;
10. @source(l): ma-single-sends([<tg,
s,v. f(s(x),v)>])
10.
Dsys
11.
D:Dsys.
11. @source(l): ma-single-sends(x : A;
11. @source(l): ma-single-sends(k : B
rcv(l; tg) : T;
11. @source(l): ma-single-sends(k;
11. @source(l): ma-single-sends(l;
11. @source(l): ma-single-sends([<tg,
s,v. f(s(x),v)>]) 
D
11.
11. D
11. realizes es.(
x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
11. realizes es.& (
e:E.
11. realizes es.& (loc(e) = source(l)
11. realizes es.& (
11. realizes es.& ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
11. realizes es.& (
e:E.
11. realizes es.& (isrcv(e)
11. realizes es.& (
11. realizes es.& (lnk(e) = l
11. realizes es.& (
11. realizes es.& ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
11. realizes es.& (
e:E.
11. realizes es.& (loc(e) = source(l)
11. realizes es.& (
11. realizes es.& (kind(e) = k
11. realizes es.& (
11. realizes es.& ((
L:{e':E| isrcv(e') & lnk(e') = l } List.
11. realizes es.& (((
e':E.
11. realizes es.& ((((e'
L) 
isrcv(e') & lnk(e') = l & sender(e') = e)
11. realizes es.& ((& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
11. realizes es.& ((& map(
e'.<tag(e'),val(e')>;L)
11. realizes es.& ((& =
11. realizes es.& ((& tagged-list-messages(
z.(z when e);val(e);[<tg
11. realizes es.& ((& tagged-list-messages(
z.(z when e);val(e);[,s,v. f
11. realizes es.& ((& tagged-list-messages(
z.(z when e);val(e);[,s,v. (s(x)
11. realizes es.& ((& tagged-list-messages(
z.(z when e);val(e);[,s,v. ,v)>])))
12. @source(l): ma-single-sends(x : A;
12. @source(l): ma-single-sends(k : B
rcv(l; tg) : T;
12. @source(l): ma-single-sends(k;
12. @source(l): ma-single-sends(l;
12. @source(l): ma-single-sends([<tg,
s,v. f(s(x),v)>])
12.
Dsys
13. D : Dsys
14. @source(l): ma-single-sends(x : A;
14. @source(l): ma-single-sends(k : B
rcv(l; tg) : T;
14. @source(l): ma-single-sends(k;
14. @source(l): ma-single-sends(l;
14. @source(l): ma-single-sends([<tg,
s,v. f(s(x),v)>]) D
15.
D':Dsys.
15. D
D'
15.
15. (
w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (
15. ((
x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
15. (& (
e:E.
15. (& (loc(e) = source(l)
15. (& (
15. (& ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
15. (& (
e:E.
15. (& (isrcv(e)
15. (& (
15. (& (lnk(e) = l
15. (& (
15. (& ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
15. (& (
e:E.
15. (& (loc(e) = source(l)
15. (& (
15. (& (kind(e) = k
15. (& (
15. (& ((
L:{e':E| isrcv(e') & lnk(e') = l } List.
15. (& (((
e':E. (e' L) isrcv(e') & lnk(e') = l & sender(e') = e)
15. (& ((& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
15. (& ((& map(
e'.<tag(e'),val(e')>;L)
15. (& ((& =
15. (& ((& tagged-list-messages(
z.(z when e);val(e);[<tg,s,v. f(s(x),v)>]))))
16. D' : Dsys
17. D
D'
18.
w:World, p:FairFifo.
18. PossibleWorld(D';w)
18.
18. (
x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
18. & (
e:E.
18. & (loc(e) = source(l)
18. & (
18. & ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
18. & (
e:E.
18. & (isrcv(e)
18. & (
18. & (lnk(e) = l
18. & (
18. & ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
18. & (
e:E.
18. & (loc(e) = source(l)
18. & (
18. & (kind(e) = k
18. & (
18. & ((
L:{e':E| isrcv(e') & lnk(e') = l } List.
18. & (((
e':E. (e' L) isrcv(e') & lnk(e') = l & sender(e') = e)
18. & ((& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
18. & ((& map(
e'.<tag(e'),val(e')>;L)
18. & ((& =
18. & ((& tagged-list-messages(
z.(z when e);val(e);[<tg,s,v. f(s(x),v)>])))
19. w : World
20.
p:FairFifo.
20. PossibleWorld(D';w)
20.
20. (
x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
20. & (
e:E.
20. & (loc(e) = source(l)
20. & (
20. & ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
20. & (
e:E.
20. & (isrcv(e)
20. & (
20. & (lnk(e) = l
20. & (
20. & ((valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e))))
20. & (
e:E.
20. & (loc(e) = source(l)
20. & (
20. & (kind(e) = k
20. & (
20. & ((
L:{e':E| isrcv(e') & lnk(e') = l } List.
20. & (((
e':E. (e' L) isrcv(e') & lnk(e') = l & sender(e') = e)
20. & ((& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
20. & ((& map(
e'.<tag(e'),val(e')>;L)
20. & ((& =
20. & ((& tagged-list-messages(
z.(z when e);val(e);[<tg,s,v. f(s(x),v)>])))
21. p : FairFifo
22. PossibleWorld(D';w)
23.
x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top
24.
e:E.
24. loc(e) = source(l)
24.
24. (valtype(e)
r ma-valtype(k : B rcv(l; tg) : T; kind(e)))
25.
e:E.
25. isrcv(e)
25.
25. lnk(e) = l
(valtype(e) r ma-valtype(k : B rcv(l; tg) : T; kind(e)))
26.
e:E.
26. loc(e) = source(l)
26.
26. kind(e) = k
26.
26. (
L:{e':E| isrcv(e') & lnk(e') = l } List.
26. ((
e':E. (e' L) isrcv(e') & lnk(e') = l & sender(e') = e)
26. (& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
26. (& map(
e'.<tag(e'),val(e')>;L)
26. (& =
26. (& tagged-list-messages(
z.(z when e);val(e);[<tg,s,v. f(s(x),v)>]))
27. (vartype(source(l);x)
r A)
27. & (
e:E. loc(e) = source(l) kind(e) = k (valtype(e) r B))
27. & (
e:E. kind(e) = rcv(l; tg) (valtype(e) r T))
e:E.
loc(e) = source(l)
kind(e) = k Knd
(L:{e':E| kind(e') = rcv(l; tg) } List.
((e':E. (e' L) kind(e') = rcv(l; tg) & sender(e') = e E)
(& (e1,e2:E. e1 before e2 L (e1 <loc e2))
(& map(e'.val(e');L) = f((x when e),val(e)) T List)
ma-valtype(k : B 
