E:EventStruct, x,y:|E| List. (x asyncR(E) y) 
(y asyncR(E) x)P:(A
AProp).
Sym x,y:A. P(x,y) Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2| Rank | Theorem | Name |
| 5 |
Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x) | [R_async_symmetric] |
| cites | ||
| 4 |
Thm* P:(AAProp).
Sym x,y:A. P(x,y) Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2 | [symmetric_swap_adjacent] |