At: P no dup permutable 1 1
1. E: EventStruct
2. x: |E| List
3. 
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
4. i: (||x||-1)
5. True
6. i@0: ||swap(x;i;i+1)||
7. j: ||swap(x;i;i+1)||
8. is-send(E)(swap(x;i;i+1)[i@0])
9. is-send(E)(swap(x;i;i+1)[j])
10. swap(x;i;i+1)[j] =msg=(E) swap(x;i;i+1)[i@0]
11. loc(E)(swap(x;i;i+1)[i@0]) = loc(E)(swap(x;i;i+1)[j])
12. Bij(||x||; ||x||; (i, i+1))
13. ||swap(x;i;i+1)|| = ||x|| 
14. (i, i+1) ||x||
||x||
15. (i, i+1)(i@0) = (i, i+1)(j)
i@0 = j
By:
Unfold `biject` -4
THEN
Unfold `inject` -4
THEN
ExRepD
THEN
BackThruSomeHyp
THEN
HypSubstSq -1 0
Generated subgoals:None
About:
