At: P no dup send enabled 1 1 2 2 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4.
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
5. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
8. i:
||y||
9. j:
||y||
10.
is-send(E)(y[i])
11.
is-send(E)(y[j])
12. y[j] =msg=(E) y[i]
13. loc(E)(y[i]) = loc(E)(y[j])
14. ||y|| = ||x||+1
15.
i = ||x||
16.
j = ||x||
17. y[i] = x[i]
18. y[j] = x[j]
i = j
By:
BackThruSomeHyp
THEN
SubstFor x[i] 0
THEN
Try Trivial
THEN
SubstFor x[j] 0
THEN
Try Trivial
Generated subgoals:None
About: