1 | 2. x: |E| List 3. y: |E| List 4. z: |E| List 5. i,j: ||x||.
is-send(E)(x[i]) 
is-send(E)(x[j])  (x[j] =msg=(E) x[i])  loc(E)(x[i]) = loc(E)(x[j])  i = j 6. i,j: ||y||.
is-send(E)(y[i]) 
is-send(E)(y[j])  (y[j] =msg=(E) y[i])  loc(E)(y[i]) = loc(E)(y[j])  i = j 7. ( x x.( y y. (x =msg=(E) y))) 8. z = (x @ y) 9. i: ||z|| 10. j: ||z|| 11. is-send(E)(z[i]) 12. is-send(E)(z[j]) 13. z[j] =msg=(E) z[i] 14. loc(E)(z[i]) = loc(E)(z[j]) i = j |