x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type.
  (rcv(l; tg) = k  T = B)
  
  (f:(ABT). 
  (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]))
  ( Dsys
  (& (D:Dsys. 
  (& (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))])
  (& (@source(l): ma-single-sends1()  D
  (& (
  (& (D 
  (& (realizes es.(vartype(source(l);x) r A)
  (& (realizes es.& (e:E. 
  (& (realizes es.& (loc(e) = source(l)  Id
  (& (realizes es.& (
  (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B))
  (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T))
  (& (realizes es.& (e:E. 
  (& (realizes es.& (loc(e) = source(l)  Id
  (& (realizes es.& (
  (& (realizes es.& (kind(e) = k  Knd
  (& (realizes es.& (
  (& (realizes es.& ((e':E. 
  (& (realizes es.& ((kind(e') = rcv(l; tg)  Knd
  (& (realizes es.& ((& sender(e') = e  E
  (& (realizes es.& ((& & (e'':E. 
  (& (realizes es.& ((& & (kind(e'') = rcv(l; tg)  Knd
  (& (realizes es.& ((& & (
  (& (realizes es.& ((& & (sender(e'') = e  E  e'' = e'  E)
  (& (realizes es.& ((& & val(e') = f((x when e),val(e))  T))))

By:

Inst Thm: s-sends-rule1 [] THEN RepeatFor 7 (ParallelOp -1 THEN Thin -3) THEN Analyze 0 THEN Analyze 0 THEN InstHyp [a,b. [(f(a,b))]] -3 THEN Thin -4 THEN Analyze -1 THEN Analyze 0 THEN Try Trivial THEN ParallelOp -2 THEN Thin -4 THEN ParallelOp -1 THEN ParallelOp -1 THEN ParallelOp -1 THEN Thin -3 THEN ParallelOp -1 THEN RepeatFor 2 (ParallelOp -1 THEN Thin -3) THEN ParallelOp -1 THEN ExRepD THEN BetterSplitAndConcl THEN Try Trivial THEN All Reduce

1

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  Knd  (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  Knd 22.  22. (L:{e':E| kind(e') = rcv(l; tg) } List.  22. ((e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = 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)))]  T List) 23. (vartype(source(l);x) r A) 23. & (e:E. loc(e) = source(l)  kind(e) = k  Knd  (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)

17 steps

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