E:EventStruct, x,y:|E| List. (x delayableR(E) y) (y delayableR(E) x)

Fold `sym` 0
THEN
Unfold `R_delayable` 0
THEN
BackThru Thm* P:(AAProp). Sym x,y:A. P(x,y) Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2
THEN
Unfold `sym` 0
THEN
Try (Complete (SplitOrHyps THEN ExRepD THEN SimpConcl))

1	1. E: EventStruct 2. a: |E| 3. b: |E| 4. (a =msg=(E) b) 5. is-send(E)(a) & is-send(E)(b) is-send(E)(a) & is-send(E)(b) (b =msg=(E) a)

About: