| Rank | Theorem | Name |
| 7 |
Thm*  E:EventStruct. switchable0(E)(totalorder(E)) | [totalorder_switchable0] |
| cites |
| 6 |
Thm* E:EventStruct, P:((Label  (|E| List))Prop).
(f,g:(Label(|E| List)). (p:Label. g(p)  f(p))   P(f) P(g))
(f,g:(Label(|E| List)).
( a:|E|. p:Label. g(p) = filter( b.  (b =msg=(E) a);f(p))) P(f) P(g))
(f,g,h:(Label(|E| List)).
(p,q:Label. (x f(p).(yg(q).(x =msg=(E) y))))
(p:Label. h(p) = ((f(p)) @ (g(p)))) P(f) P(g) P(h))
switchable0(E)(local_deliver_property(E;P)) | [local_deliver_switchable] |
| 0 |
Thm* f:(AB), L1,L2:A List. L1 L2 map(f;L1) map(f;L2) | [iseg_map] |
| 1 |
Thm* as2,bs2,as1,bs1:T List.
as1 as2 bs1 bs2 agree_on_common(T;as2;bs2) agree_on_common(T;as1;bs1) | [agree_on_common_iseg] |
| 0 |
Thm* f:(T1T2), Q:(T2 ), L:T1 List. filter(Q;map(f;L)) = map(f;filter(Q o f;L)) | [filter_map] |
| 2 |
Thm* P:(T), as,bs:T List.
agree_on_common(T;as;bs) agree_on_common(T;filter(P;as);filter(P;bs)) | [agree_on_common_filter] |
| 2 |
Thm* as,bs,cs,ds:T List.
(xcs.(x bs))
(xas.(x ds))
agree_on_common(T;as;cs) agree_on_common(T;bs;ds) agree_on_common(T;as @ bs;cs @ ds) | [agree_on_common_append] |
| 1 |
Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) | [msg_eq_equiv] |