| Rank | Theorem | Name |
| 3 |
Thm*  E:TaggedEventStruct, P,I:TraceProperty(E).
MCS(E)(P)   safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P) | [M_DASH_C_DASH_S_SPACE_induction] |
| cites |
| 0 |
Thm* l:T List. ||l|| = 0 l = nil | [length_zero] |
| 0 |
Thm* L:T List.  L = nil 0 < ||L|| | [non_nil_length] |
| 0 |
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |
| 0 |
Thm* P:(T   ), L2,L1:T List. L1  L2 filter(P;L1) filter(P;L2) | [filter_iseg] |
| 0 |
Thm* P:(T), L:T List. (x L.P(x)) (filter(P;L) ~ L) | [filter_trivial] |
| 1 |
Thm* msg:(AA), L1,L2:A List.
(x:A. (x L1) (x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nil | [remove_msgs_nil] |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
| 1 |
Thm* E:EventStruct, P:TraceProperty(E), L,L1:|E| List.
memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1)) | [memoryless_remove_msgs] |