| Rank | Theorem | Name |
| 4 |
Thm*  E:EventStruct. switchable0(E)(Causal(E)) | [P_causal_switchable0] |
| cites |
| 0 |
Thm* P:(T   ), L_1,L_2:T List.
L_2  filter(P;L_1)   ( L_3:T List. L_3 L_1 & L_2 = filter(P;L_3)) | [iseg_filter] |
| 0 |
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
| 0 | Thm* k: , i,j:k. (i, j)  kk | [flip_wf] |
| 2 |
Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  | [swap_length] |
| 3 |
Thm* L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1 | [swap_swap] |