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@source(l).kind(e) = locl(a)
17. & e@source(l).e'@source(l).kind(e) = locl(a)
17. & e@source(l).e'@source(l).
17. & kind(e') = locl(a)  e = e'
  (vartype(source(l);x) r A)
  & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
  & (e:E. 
  & (kind(e) = rcv(l; tg)
  & (& val(e) = f((x when sender(e)))  T
  & (& & kind(sender(e)) = locl(a)
  & (& & (e':E. 
  & (& & (kind(e') = rcv(l; tg)  kind(sender(e')) = locl(a)  e' = e))

By:	USendRule1 l locl(a) x tg A Unit T (a,b. f(a)) THENA MaAuto

1

17. e@source(l).kind(e) = locl(a) 18. e@source(l).e'@source(l).kind(e) = locl(a) 18. e@source(l).e'@source(l). 18. kind(e') = locl(a)  Knd  e = e'  E 19. @source(l): ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))]) 19. @source(l): ma-single-sends1() 19.  Dsys 20. vartype(source(l);x) r A 21. e:E. loc(e) = source(l)  kind(e) = locl(a)  (valtype(e) r Unit) 22. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T) 23. e:E.  23. loc(e) = source(l) 23.  23. kind(e) = locl(a) 23.  23. (e':E.  23. (kind(e') = rcv(l; tg) 23. (& sender(e') = e  E 23. (& & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e') 23. (& & val(e') = f((x when e))  T)   (vartype(source(l);x) r A)   & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))   & (e:E.    & (kind(e) = rcv(l; tg)   & (& val(e) = f((x when sender(e)))  T   & (& & kind(sender(e)) = locl(a)   & (& & (e':E.    & (& & (kind(e') = rcv(l; tg)  kind(sender(e')) = locl(a)  e' = e))

6 steps

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