At: P causal switchable0 5 1 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4.
i:
||x||.
j:
||x||. j
i & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. i1:
(||x||-1)
6.
loc(E)(x[i1]) = loc(E)(x[(i1+1)])
7.
is-send(E)(x[i1]) &
is-send(E)(x[(i1+1)])
is-send(E)(x[i1]) & is-send(E)(x[(i1+1)])
8. y = swap(x;i1;i1+1)
9. i:
||y||
10. ||swap(x;i1;i1+1)|| = ||x||

11. ||y|| = ||x||

12. ||swap(y;i1;i1+1)|| = ||y||

13. (i1, i1+1)
||x||

||x||
14. is-send(E)(y[i])
j:
||y||. j
i & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])
By: InstConcl [i]
Generated subgoal:1 | y[i] =msg=(E) y[i] |
About: