At: strong switch inv decomposable12112212111112121211 1. E: TaggedEventStruct 2. tr: |E| List 3. ... 4. i:(||tr||-1).
(is-send(E)(tr[i]) is-send(E)(tr[(i+1)]) (tr[i] =msg=(E) tr[(i+1)]))
& ((x,y:||tr||.
x < y
& is-send(E)(tr[x])
& is-send(E)(tr[y])
& tr[x] delivered at time i+1
& tr[y] delivered at time i)
loc(E)(tr[i]) = loc(E)(tr[(i+1)])) 5. i,j:||tr||.
is-send(E)(tr[i]) is-send(E)(tr[j]) (tr[j] =msg=(E) tr[i]) loc(E)(tr[i]) = loc(E)(tr[j]) i = j 6. tr = nil 7. ls: ||tr|| 8. is-send(E)(tr[ls]) 9. ... 10. ... 11. EquivRel(|E|)(_1 =msg=(E) _2) 12. ... 13. d: 14. 0 < d 15. ... 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 33. k': ||tr|| 34. tr[j@0] =msg=(E) tr[k'] 35. is-send(E)(tr[k']) 36. loc(E)(tr[k']) = loc(E)(tr[(j-1)]) 37. j-1k'
x,y:||tr||.
x < y
& is-send(E)(tr[x])
& is-send(E)(tr[y])
& tr[x] delivered at time j
& tr[y] delivered at time j-1 By: Unfold `delivered_at` 0
THEN
InstConcl [j@0;k] Generated subgoal:
is-send(E)(tr[k])
i:
(||tr||-1).
(is-send(E)(tr[i]) 
is-send(E)(tr[(i+1)]) 
x,y:
j
