At: P causal switchable0 5 1 1 2 3 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. 
i:
||x||. 
j:||x||. j
i & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. i1: (||x||-1)
6. 
loc(E)(x[i1]) = loc(E)(x[(i1+1)])
7. is-send(E)(x[i1]) & is-send(E)(x[(i1+1)]) 
is-send(E)(x[i1]) & is-send(E)(x[(i1+1)])
8. y = swap(x;i1;i1+1)
9. i: ||y||
10. ||swap(x;i1;i1+1)|| = ||x|| 
11. ||y|| = ||x||
12. ||swap(y;i1;i1+1)|| = ||y||
13. (i1, i1+1) ||x||
||x||
14. is-send(E)(y[i])
15. j: ||x||
16. j(i1, i1+1)(i)
17. is-send(E)(x[j])
18. x[j] =msg=(E) x[((i1, i1+1)(i))]
swap(y;i1;i1+1) = x
By:
((Thin -3) THEN (Thin -1) THEN (HypSubstList 8 0)) THENA (AllHyps Thin)
THEN
BackThru
Thm* L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1
Generated subgoals:None
About:
