1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. rcv(l; tg) = k  T = B
9. f : ABT
10. @source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]))
10.  Dsys
11. @source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]))
11.  Dsys
12. D : Dsys
13. @source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]))  D
14. D' : Dsys
15. D  D'
16. w : World
17. p : FairFifo
18. PossibleWorld(D';w)
19. vartype(source(l);x) r A
20. e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B)
21. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
22. vartype(source(l);x) r A
23. e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B)
24. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
25. e : E
26. loc(e) = source(l)
27. kind(e) = k
28. u : {e':E| kind(e') = rcv(l; tg) }
29. e':E. (e'  [u])  kind(e') = rcv(l; tg) & sender(e') = e
30. [val(u)] = [(f((x when e),val(e)))]
  e':E. 
  kind(e') = rcv(l; tg)
  & sender(e') = e  E
  & & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e')
  & & val(e') = f((x when e),val(e))  T

1	kind(u) = rcv(l; tg)	1 step
2	sender(u) = e  E	1 step
3	31. e'' : E 32. kind(e'') = rcv(l; tg) 33. sender(e'') = e  E   e'' = u	1 step
4	31. e'' : E 32. kind(e'') = rcv(l; tg)   isrcv(e'')	1 step
5	val(u) = f((x when e),val(e))  T	3 steps
6	31. e' : E 32. kind(e') = rcv(l; tg)   isrcv(e')	1 step
7	31. e' : E 32. kind(e') = rcv(l; tg) 33. e'' : E 34. kind(e'') = rcv(l; tg)   isrcv(e'')	1 step
8	31. e' : E 32. kind(e') = rcv(l; tg)   val(e')  T	1 step
9	31. e' : E 32. kind(e') = rcv(l; tg)   (x when e)  A	1 step
10	31. e' : E 32. kind(e') = rcv(l; tg)   val(e)  B	1 step

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