E:EventStruct, x,y:|E| List.
(x delayableR(E) y) 
(y delayableR(E) x)P:(A
AProp).
Sym x,y:A. P(x,y) Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)| Rank | Theorem | Name |
| 5 |
Thm* E:EventStruct, x,y:|E| List.
(x delayableR(E) y) (y delayableR(E) x) | [R_delayable_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] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |