E:TaggedEventStruct. Tag-by-msg(E) fuses No-dup-deliver(E)L1,L2:T List, P:(T
).
sublist(T;L2;filter(P;L1)) 
sublist(T;L2;L1) & (x
L2.P(x))E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)| Rank | Theorem | Name |
| 3 |
Thm* E:TaggedEventStruct. Tag-by-msg(E) fuses No-dup-deliver(E) | [no_dup_fusion] |
| cites | ||
| 0 |
Thm* L1,L2:T List, P:(T).
sublist(T;L2;filter(P;L1)) sublist(T;L2;L1) & (xL2.P(x)) | [sublist_filter] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |