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

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

delayableR(E) preserves No-dup-deliver(E)
By:
BackThru Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P delayableR(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