1. T : Type
2. A : Type
3. a : Id
4. f : AT
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)
  e'@0 = e'

1

sender(e'@0) = e  E

1 step

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