At: P no dup composable 1 1
1. E: EventStruct
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
By: Decide (i < j)
Generated subgoals:1 | 15. i < j i = j |
2 | 15. i < j i = j |
About: