2. A : Type
3. a : Id
4. f : A
T
5. tg : Id
6. l : IdLnk
7. x : Id
8.
"done" = x
9. A
10. T
11. (
loc.
(send-once(loc;T;A;a;f;tg;l;x))) 
Dsys
12. D' : Dsys
13.
loc.(send-once(loc;T;A;a;f;tg;l;x)) 
D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. e : E
18. loc(e) = source(l)
19. kind(e) = locl(a)
20.
e:E.
20. loc(e) = source(l)
20.
20. (
e':E.
20. (loc(e') = source(l)
kind(e) = locl(a) kind(e') = locl(a) e = e')
21. @source(l): ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (
a,b. [(f(a))])
21. @source(l): ma-single-sends1()
21.
Dsys
22. vartype(source(l);x)
r A
23.
e:E. loc(e) = source(l) kind(e) = locl(a) (valtype(e) r Unit)
24.
e:E. kind(e) = rcv(l; tg) (valtype(e) r T)
25.
e:E.
25. loc(e) = source(l)
25.
25. kind(e) = locl(a)
25.
25. (
e':E.
25. (kind(e') = rcv(l; tg)
25. (& sender(e') = e
25. (& & (
e'':E. kind(e'') = rcv(l; tg) sender(e'') = e e'' = e')
25. (& & val(e') = f((x when e)))
26. e' : E
27. kind(e') = rcv(l; tg)
28. sender(e') = e
29.
e'':E. kind(e'') = rcv(l; tg) sender(e'') = e e'' = e'
30. val(e') = f((x when e))
31. e'@0 : E
32. kind(e'@0) = rcv(l; tg)
33. kind(sender(e'@0)) = locl(a)
sender(e'@0) = e E
