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))

1	1. E: TaggedEventStruct 2. x: |E| List 3. i: (||x||-1) 4. switch_inv(E)(x) 5. is-send(E)(x[(i+1)]) 6. is-send(E)(x[i]) loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1))

About: