E:TaggedEventStruct, x:|E| List, i:
(||x||-1).
switch_inv(E)(x) 
is-send(E)(x[(i+1)])
is-send(E)(x[i]) 
loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1))L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| 
k:, x,y,i:k. (y, x)((y, x)(i)) = i