(x =msg=(E) y)
& (is-send(E)(x)) & (is-send(E)(y)) 
(is-send(E)(x)) & (is-send(E)(y))]
is mentioned by
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:EventStruct, x,y:|E| List.
(x delayableR(E) y) (y delayableR(E) x) | [R_delayable_symmetric] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P delayableR(E) preserves P | [permutable_implies_delayable] |
|
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E) | [no_duplicate_send_delayable] |
|
Def adR(E) == (delayableR(E) asyncR(E))^* | [R_ad] |
| Def switchable(E)(P) == safetyR(E) preserves P & memorylessR(E) preserves P & (ternary) composableR(E) preserves P & send-enabledR(E) preserves P & asyncR(E) preserves P & delayableR(E) preserves P & (P refines Causal(E)) & (P refines No-dup-deliver(E)) | [b_switchable] |
| Def switchable0(E)(P) == safetyR(E) preserves P & memorylessR(E) preserves P & (ternary) composableR(E) preserves P & send-enabledR(E) preserves P & asyncR(E) preserves P & delayableR(E) preserves P | [switchable0] |
|
Def layerR(E) == ((asyncR(E) delayableR(E)) send-enabledR(E))^* | [layer_rel] |
Try larger context: GenAutomata