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. e:E. 
22. loc(e) = source(l)
22. 
22. kind(e) = k
22. 
22. (L:{e':E| kind(e') = rcv(l; tg) } List. 
22. ((e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e)
22. (& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
22. (& map(e'.val(e');L) = [(f((x when e),val(e)))])
23. (vartype(source(l);x) r A)
23. & (e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B))
23. & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
  e:E. 
  loc(e) = source(l)
  
  kind(e) = k  Knd
  
  (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

22. (vartype(source(l);x) r A) 22. & (e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)) 22. & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)) 23. e : E 24. loc(e) = source(l) 25. kind(e) = k  Knd 26. L:{e':E| kind(e') = rcv(l; tg) } List.  26. (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e  E) 26. & (e1,e2:E. e1 before e2  L  (e1 <loc e2)) 26. & map(e'.val(e');L) = [(f((x when e),val(e)))]  T List   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

16 steps

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