At: switch inv swap 1 1 2 1 2
1. E: TaggedEventStruct
2. x: |E| List
3. i: 
(||x||-1)
4. 
is-send(E)(x[(i+1)])
5. is-send(E)(x[i]) 
loc(E)(x[i]) = loc(E)(x[(i+1)])
6. ||swap(x;i;i+1)|| = ||x|| 
7. 
i,j,k:||x||.
i < j 
is-send(E)(x[i])
is-send(E)(x[j])
tag(E)(x[i]) = tag(E)(x[j])
(x[j] =msg=(E) x[k]) & is-send(E)(x[k])
(
k':||x||. k' < k & (x[i] =msg=(E) x[k']) & is-send(E)(x[k']) & loc(E)(x[k']) = loc(E)(x[k]))
8. i@0: ||swap(x;i;i+1)||
9. j: ||swap(x;i;i+1)||
10. k: ||swap(x;i;i+1)||
11. f: ||x||
||x||
12. (i, i+1) = f ||x||||x||
13. i@0 < j
14. is-send(E)(x[(f(i@0))])
15. is-send(E)(x[(f(j))])
16. tag(E)(x[(f(i@0))]) = tag(E)(x[(f(j))])
17. x[(f(j))] =msg=(E) x[(f(k))]
18. is-send(E)(x[(f(k))])
19. k': ||x||
20. k' < f(k)
21. x[(f(i@0))] =msg=(E) x[k']
22. is-send(E)(x[k'])
23. loc(E)(x[k']) = loc(E)(x[(f(k))])
f(k') < k & (x[(f(i@0))] =msg=(E) x[k']) & is-send(E)(x[k']) & loc(E)(x[k']) = loc(E)(x[(f(k))])
By: SimpConcl
Generated subgoal:| 1 | f(k') < k |
About:
