IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
send-once realizes1111 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'') = ee'' = 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'') = ee'' = e' 30. val(e') = f((x when e))
31. z : E
32. z = e (x when z) A