| Rank | Theorem | Name |
| 3 |
Thm*  E:TaggedEventStruct.
(switch-decomposable(E)  Tag-by-msg(E) Causal(E) No-dup-send(E))
refines single-tag-decomposable(E) | [switch_decomp_implies_single_tag_decomp] |
| cites |
| 1 |
Thm* L:T List, P:( ||L||  Prop).
(x:||L||. Dec(P(x)))  
(i,j:||L||. P(i) i < j P(j))
( L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1|| i)) | [append_split2] |
| 0 |
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |
| 0 |
Thm* L:T List, x:T. (x  L)  null(L) | [member_null] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |