Thm*  E:TaggedEventStruct, P:TraceProperty(E).
switchable(E)(P)   ((switch_inv(E)  No-dup-send(E)) fuses P) | [switch_inv_theorem2] |
|
Thm* E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P)
asyncR(E) preserves P
delayableR(E) preserves P
(P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P) | [switch_inv_theorem] |
|
Thm* E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P)
(P refines (Causal(E) No-dup-deliver(E)))
(((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P) | [switch_inv_plus_normal] |
Thm* E:TaggedEventStruct, tr:Trace(E).
(switch_inv(E) No-dup-send(E))(tr)
( tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')) | [switch_normal_exists] |
|
Thm* E:TaggedEventStruct.
(switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) | [strong_switch_inv_decomposable] |
|
Thm* E:EventStruct.
switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E)) | [totalorder_switchable] |
|
Thm* E:EventStruct, P:TraceProperty(E).
switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |
|
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] |
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] |
|
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] |
|
Thm* E:TaggedEventStruct, P,I,J,K:TraceProperty(E)
, R:(Trace(E)Trace(E)Prop).
tag_splitable(E;R)
(tr_1,tr_2:Trace(E). (tr_1 R tr_2) (tr_2 R tr_1))
R preserves P
R preserves K
(tr:Trace(E). (I K)(tr) (tr':Trace(E). I(tr') & J(tr') & (tr R tr')))
(((I J) K) fuses P) ((I K) fuses P) | [normal_form_fusion] |
|
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
((I J) fuses P) (I fuses J) (P refines J) (I fuses P) | [fusion_simplification] |
|
Thm* E:TaggedEventStruct, I,P,Q:TraceProperty(E).
(I fuses P) (I fuses Q) (I fuses (P Q)) | [fusion_and] |
|
Thm* E:Structure, P,Q_1,Q_2:((|E| List)Prop).
(P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2)) | [tr_refines_and] |