(7steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: P no dup switchable0 2
1. E: EventStruct

memorylessR(E) preserves No-dup-deliver(E)
By:
BackThru Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P memorylessR(E) preserves P
THEN
Try (Unfold `trace_property` 0)
THEN
Easy
Generated subgoals:

None

About:
list

(7steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc