| Rank | Theorem | Name |
| 5 |
Thm*  E:TaggedEventStruct, P,I:((|E| List)  Prop).
(P refines (Causal(E)  No-dup-deliver(E)))  
((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P)
((I No-dup-send(E)) fuses P) | [no_DASH_dup_DASH_fusion] |
| cites |
| 4 |
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop).
(P refines Causal(E))
((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P) | [tag_by_msg_fusion_lemma] |
| 0 |
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
((I J) fuses P) (I fuses J) (P refines J) (I fuses P) | [fusion_simplification] |
| 0 |
Thm* E:TaggedEventStruct, I,P,Q:TraceProperty(E).
(I fuses P) (I fuses Q) (I fuses (P Q)) | [fusion_and] |
| 1 |
Thm* E:TaggedEventStruct. PTrue fuses Causal(E) | [causal_fusion] |
| 0 |
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
(J refines I) (I fuses P) (J fuses P) | [fusion_weakening] |
| 3 |
Thm* E:TaggedEventStruct. Tag-by-msg(E) fuses No-dup-deliver(E) | [no_dup_fusion] |