x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type.
  (rcv(l; tg) = k  T = B)
  
  (f:(ABT), c:(AB).
  (@source(l): ma-single-sends1(A;
  (@source(l): ma-single-sends1(B;
  (@source(l): ma-single-sends1(T;
  (@source(l): ma-single-sends1(x;
  (@source(l): ma-single-sends1(k;
  (@source(l): ma-single-sends1(l;
  (@source(l): ma-single-sends1(tg;
  (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi))
  ( Dsys
  (& (D:Dsys. 
  (& (@source(l): ma-single-sends1(A;
  (& (@source(l): ma-single-sends1(B;
  (& (@source(l): ma-single-sends1(T;
  (& (@source(l): ma-single-sends1(x;
  (& (@source(l): ma-single-sends1(k;
  (& (@source(l): ma-single-sends1(l;
  (& (@source(l): ma-single-sends1(tg;
  (& (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi)
  (& (@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.& ((c((x when e),val(e))
  (& (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))
  (& (realizes es.& (& (c((x when e),val(e))
  (& (realizes es.& (& (
  (& (realizes es.& (& ((e':E. 
  (& (realizes es.& (& ((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E)))))

By:

Inst Thm: s-sends-rule1 [] THEN RepeatFor 7 (ParallelOp -1 THEN Thin -3) THEN RepeatFor 3 (Analyze 0) THEN InstHyp [a,b. if c(a,b) [(f(a,b))] else nil fi] -4 THEN Thin -5 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 THEN ParallelOp -2 THEN Thin -4 THEN ParallelLast THEN ParallelLast THEN ThinHypsMentioning [`ma-single-sends1`]

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. c : AB 11. D : Dsys 12. D' : Dsys 13. D  D' 14. w : World 15. p : FairFifo 16. PossibleWorld(D';w) 17. vartype(source(l);x) r A 18. e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B) 19. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T) 20. (vartype(source(l);x) r A) 20. & (e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)) 20. & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)) 21. e : E 22. loc(e) = source(l) 23. kind(e) = k  Knd 24. L:{e':E| kind(e') = rcv(l; tg) } List.  24. (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e  E) 24. & (e1,e2:E. e1 before e2  L  (e1 <loc e2)) 24. & map(e'.val(e');L) 24. & = 24. & if c((x when e),val(e)) [(f((x when e),val(e)))] else nil fi   (c((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))   & (c((x when e),val(e))   & (   & ((e':E. kind(e') = rcv(l; tg) & sender(e') = e  E))

23 steps

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