1 | 1. E: EventStruct 2. P: (|E| List)![](FONT/dash.png) Prop 3. x,y:|E| List. P(x) ![](FONT/eq.png) (x swap adjacent[True] y) ![](FONT/eq.png) P(y) 4. x: |E| List 5. y: |E| List 6. P(x) 7. x swap adjacent[ (x =msg=(E) y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y x swap adjacent[True] y |