By: |
THEN All (Unfolds [`alle-at`;`existse-at`]) THEN ExRepD THEN AllHyps ( ![]() (InstHyp [e] h THENA Complete Auto THEN ParallelOp -1 THEN ExRepD THEN MaAuto) |
1 |
18. loc(e) = source(l) 19. kind(e) = locl(a) 20. ![]() 20. loc(e) = source(l) 20. ![]() ![]() 20. ( ![]() 20. (loc(e') = source(l) ![]() ![]() ![]() ![]() ![]() ![]() 21. @source(l): ma-single-sends1(A; Unit; T; x; locl(a); l; tg; ( ![]() 21. @source(l): ma-single-sends1() 21. ![]() 22. vartype(source(l);x) ![]() 23. ![]() ![]() ![]() ![]() ![]() ![]() 24. ![]() ![]() ![]() ![]() 25. ![]() 25. loc(e) = source(l) 25. ![]() ![]() 25. kind(e) = locl(a) 25. ![]() ![]() 25. ( ![]() 25. (kind(e') = rcv(l; tg) 25. (& sender(e') = e ![]() 25. (& & ( ![]() ![]() ![]() ![]() ![]() ![]() 25. (& & val(e') = f((x when e)) ![]() 26. e' : E 27. kind(e') = rcv(l; tg) 28. sender(e') = e ![]() 29. ![]() ![]() ![]() ![]() ![]() ![]() 30. val(e') = f((x when e)) ![]() ![]() ![]() ![]() | 3 steps |
2 |
18. loc(e) = source(l) 19. kind(e) = locl(a) 20. ![]() 20. loc(e) = source(l) 20. ![]() ![]() 20. ( ![]() 20. (loc(e') = source(l) ![]() ![]() ![]() ![]() ![]() ![]() 21. @source(l): ma-single-sends1(A; Unit; T; x; locl(a); l; tg; ( ![]() 21. @source(l): ma-single-sends1() 21. ![]() 22. vartype(source(l);x) ![]() 23. ![]() ![]() ![]() ![]() ![]() ![]() 24. ![]() ![]() ![]() ![]() 25. ![]() 25. loc(e) = source(l) 25. ![]() ![]() 25. kind(e) = locl(a) 25. ![]() ![]() 25. ( ![]() 25. (kind(e') = rcv(l; tg) 25. (& sender(e') = e ![]() 25. (& & ( ![]() ![]() ![]() ![]() ![]() ![]() 25. (& & val(e') = f((x when e)) ![]() 26. e' : E 27. kind(e') = rcv(l; tg) 28. sender(e') = e ![]() 29. ![]() ![]() ![]() ![]() ![]() ![]() 30. val(e') = f((x when e)) ![]() 31. e'@0 : E 32. kind(e'@0) = rcv(l; tg) 33. kind(sender(e'@0)) = locl(a) ![]() ![]() | 2 steps |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |