At: strong switch inv decomposable 1 2 1 1 2 2 1 2 1 1 2
1. E: TaggedEventStruct
2. tr: |E| List
3. 
i:
||tr||. 
j:||tr||. j
i & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])
4. AD-normal(E)(tr)
5. No-dup-deliver(E)(tr)
6. 
tr = nil
7. ls: ||tr||
8. is-send(E)(tr[ls])
9. j:||tr||. ls < j 
is-send(E)(tr[j])
10. i:||tr||. (i (switchR(tr)^*) ls) is-send(E)(tr[i])
11. EquivRel(|E|)(_1 =msg=(E) _2)
12. i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)
13. d: 
14. 0 < d
15. i,j:||tr||.
d-1 = j-i
(i (switchR(tr)^*) ls) ij (k:||tr||. (k (switchR(tr)^*) ls) & (tr[k] =msg=(E) tr[j]))
16. i: ||tr||
17. j: ||tr||
18. d = j-i
19. i (switchR(tr)^*) ls
20. ij
21. is-send(E)(tr[i])
22. is-send(E)(tr[j])
23. ij-1
24. is-send(E)(tr[(j-1)])
25. k: ||tr||
26. k (switchR(tr)^*) ls
27. tr[k] =msg=(E) tr[(j-1)]
28. j@0: ||tr||
29. j@0j
30. is-send(E)(tr[j@0])
31. tr[j@0] =msg=(E) tr[j]
32. j@0 < k
j@0 (switchR(tr)^*) ls
By: Using [`i',k] BackThruSomeHyp
Generated subgoals:None
About:
