Thm*  E:EventStruct, P:TraceProperty(E), A:Type, evt:(A  |E|)
, tg:(ALabel), tr_u:Trace(E), tr_l:A List.
switchable(E)(P)  
No-dup-send(E)(tr_u)
full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u) | [switch_main_theorem] |
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:EventStruct, P:TraceProperty(E).
switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P asyncR(E) preserves P | [permutable_implies_async] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P delayableR(E) preserves P | [permutable_implies_delayable] |
|
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] |
Thm* E:EventStruct. totalorder(E)  TraceProperty(E) | [totalorder_wf] |
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:EventStruct, P:TraceProperty(E), L,L1:|E| List.
memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1)) | [memoryless_remove_msgs] |
|
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:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P memorylessR(E) preserves P | [strong_safety_implies_memoryless] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P safetyR(E) preserves P | [strong_safety_implies_safety] |
|
Thm* E:TaggedEventStruct, I,P,Q:TraceProperty(E).
(I fuses P) (I fuses Q) (I fuses (P Q)) | [fusion_and] |
|
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
(J refines I) (I fuses P) (J fuses P) | [fusion_weakening] |