At: no duplicate send safety 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[i] =msg=(E) x[j]) i = j
5. y 
x
6. i: ||y||
7. j: ||y||
8. is-send(E)(y[i])
9. is-send(E)(y[j])
10. y[i] =msg=(E) y[j]
11. ||y||||x||
12. i:. i < ||y|| y[i] = x[i]
i = j
By:
AllHyps (InstHyp [i])
THEN
AllHyps (
h.(InstHyp [j] h) THENA (Complete Auto))
THEN
BackThruSomeHyp
THEN
Try (SubstFor x[i] 0)
THEN
Try (SubstFor x[j] 0)
Generated subgoals:None
About:
