At: P no dup strong 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[j] =msg=(E) x[i]) loc(E)(x[i]) = loc(E)(x[j]) i = j
5. f: ||y||
||x||
6. increasing(f;||y||)
7. j:||y||. y[j] = x[(f(j))]
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. f(i) = f(j)
15. y[j] = x[(f(j))]
16. y[i] = x[(f(i))]
i = j
By:
AllHyps
(
h.
FwdThru
Thm* k,m:, f:(km). increasing(f;k) Inj(k; m; f)
[h])
THEN
Unfold `inject` -1
THEN
BackThru -1
Generated subgoals:None
About:
