| Rank | Theorem | Name |
| 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] |
| cites |
| 0 |
Thm* P:(T ), L2,L1:T List. L1 L2 filter(P;L1) filter(P;L2) | [filter_iseg] |
| 0 |
Thm* as:T List. (as @ nil) = as | [append_back_nil] |
| 0 |
Thm* P:(T), L:T List. (xfilter(P;L).P(x)) | [l_all_filter] |
| 5 |
Thm* P:(AAProp), f:(A), L1,L2:A List.
(L1 swap adjacent[P(x,y)] L2)
(filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))  filter(f;L1) = filter(f;L2) | [filter_swap_adjacent] |