mb hybrid Sections GenAutomata Doc

Def memorylessR(E)(L_1,L_2) == a:|E|. L_2 = filter(b.(b =msg=(E) a);L_1) |E| List

is mentioned by

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:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P memorylessR(E) preserves P[strong_safety_implies_memoryless]
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 MCS(E)(P) == memorylessR(E) preserves P & (ternary) composableR(E) preserves P & safetyR(E) preserves P[memoryless_composable_safety]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc