At: P no dup composable 1 1 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.(yy.(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])
15. i < j
16. j < ||x||
i = j
By: Assert (z[i] = x[i])
Generated subgoals:| 1 | z[i] = x[i] |
| 2 | 17. z[i] = x[i]
i = j |
About:
