E:EventStruct, tr:|E| List.
No-dup-deliver(E)(tr)
(x,y:|E|.
is-send(E)(x) 
is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr))E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)| Rank | Theorem | Name |
| 3 |
Thm* E:EventStruct, tr:|E| List.
No-dup-deliver(E)(tr)
(x,y:|E|.
is-send(E)(x)
is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr)) | [P_no_dup_iff] |
| cites | ||
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |