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

tr = nil

||tr||

||tr||

||tr||

ij

is-send(E)(tr[j])

ij-1

is-send(E)(tr[(j-1)])

||tr||

||tr||

j@0j

||tr||

is-send(E)(tr[k'])

j-1k'

AllHyps (h.(Unfold `switch_normal` h) THEN (Reduce h) THEN (InstHyp [j-1] h))
THEN
Subst' (j-1+1 = j) -1
THEN
SimpHyp -1

1

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' 38. (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) loc(E)(tr[(j-1)]) = loc(E)(tr[j]) loc(E)(tr[j]) = loc(E)(tr[k'])

About: