| Rank | Theorem | Name |
| 5 |
Thm*  E:TaggedEventStruct.
(switch_inv(E)  Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) | [strong_switch_inv_decomposable] |
| cites |
| 1 |
Thm* E:EventStruct, L:|E| List.
 L = nil   Causal(E)(L) ( i: ||L||. is-send(E)(L[i])) | [P_causal_non_nil] |
| 4 |
Thm* L:T List, P:(||L||  Prop).
(x:||L||. Dec(P(x))) (i:||L||. P(i)) (i:||L||. P(i) & (j:||L||. i < j P(j))) | [last_with_property] |
| 0 |
Thm* x,y:T, R:(TTProp). x = y (x (R^*) y) | [rel_star_weakening] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
| 1 |
Thm* E:TaggedEventStruct, tr:|E| List, ls:||tr||.
switch_inv(E)(tr)
(i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j])) | [switch_inv_rel_closure] |
| 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] |
| 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] |
| 2 |
Thm* R:(TTProp), x,y,z:T. (x R y) (y (R^*) z) (x (R^*) z) | [rel_star_trans] |