| Rank | Theorem | Name |
| 6 |
Thm*  E:TaggedEventStruct, tr:Trace(E).
(switch_inv(E)  No-dup-send(E))(tr)  
( tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')) | [switch_normal_exists] |
| cites |
| 5 |
Thm* L:T List, P:(T  TProp).
(x,y:T. Dec(P(x,y)))
(x,y:T.  P(x,y) P(y,x))
(L':T List. (L (swap adjacent[P(x,y)]^*) L') & (i: (||L'||-1). P(L'[i],L'[(i+1)]))) | [partial_sort] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
| 3 |
Thm* E:TaggedEventStruct, x:|E| List, i:(||x||-1).
switch_inv(E)(x)
is-send(E)(x[(i+1)])
is-send(E)(x[i])  loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1)) | [switch_inv_swap] |
| 0 |
Thm* P:(TProp), R:(TTProp). R preserves P R^* preserves P | [preserved_by_star] |
| 3 |
Thm* L:T List, i:(||L||-1), a,b:T.
a before b  swap(L;i;i+1) a before b L a = L[(i+1)] & b = L[i] | [l_before_swap] |
| 2 |
Thm* R1,R2:(TTProp), x,y:T. R1 = > R2 (x (R1^*) y) (x (R2^*) y) | [rel_star_monotonic] |