1 | 6. x: |E| List 7. y: |E| List 8. P(p.x delivered at p) 9. x swap adjacent[(x =msg=(E) y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y 10. x1: Label 11. i: (||filter(e.is-send(E)(e)loc(E)(e) = x1;x)||-1) 12. (filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i] =msg=(E) filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)]) 13. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i]) 14. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)]) 15. filter(e.is-send(E)(e)loc(E)(e) = x1;y) = swap(filter(e.is-send(E)(e)loc(E)(e) = x1;x);i;i+1) 16. x@0:|E|. (x@0 filter(e.is-send(E)(e)loc(E)(e) = x1;x)) is-send(E)(x@0) & loc(E)(x@0) = x1 filter(e.is-send(E)(e)loc(E)(e) = x1;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x) |
2 | 6. x: |E| List 7. y: |E| List 8. P(p.x delivered at p) 9. x swap adjacent[(x =msg=(E) y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y 10. x1: Label 11. i: (||filter(e.is-send(E)(e)loc(E)(e) = x1;x)||-1) 12. (filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i] =msg=(E) filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)]) 13. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i]) 14. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)]) 15. filter(e.is-send(E)(e)loc(E)(e) = x1;y) = swap(filter(e.is-send(E)(e)loc(E)(e) = x1;x);i;i+1) 16. x@0:|E|. (x@0 filter(e.is-send(E)(e)loc(E)(e) = x1;x)) is-send(E)(x@0) & loc(E)(x@0) = x1 filter(e.is-send(E)(e)loc(E)(e) = x1;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x) |
About: