mb hybrid Sections GenAutomata Doc

Def MCS(E)(P) == memorylessR(E) preserves P & (ternary) composableR(E) preserves P & safetyR(E) preserves P

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: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, 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]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc