| Rank | Theorem | Name |
| 3 |
Thm*  E:EventStruct, tr:|E| List, ls: ||tr||.
is-send(E)(tr[ls])  
(j:||tr||. ls < j  is-send(E)(tr[j]))
(i,j:||tr||. i j is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)) | [switch_inv_rel_closure_lemma1] |
| cites |
| 0 |
Thm* x,y:T, R:(T  TProp). x = y (x (R^*) y) | [rel_star_weakening] |
| 0 |
Thm* E:EventStruct, a,b,c:|E|, tr:|E| List.
a somewhere delivered before b a somewhere delivered before c  c somewhere delivered before b | [delivered_before_somewhere_lemma] |
| 2 |
Thm* R:(TTProp), x,y,z:T. (x R y) (y (R^*) z) (x (R^*) z) | [rel_star_trans] |
| 1 |
Thm* E:EventStruct, tr:|E| List, ls,i:||tr||.
is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i]) | [switch_inv_rel_closure_send] |