PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: totalorder switchable

E:EventStruct. switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E))
By:
Auto
THEN
BackThru Thm* E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E))
THEN
BackThru Thm* E:EventStruct. switchable0(E)(totalorder(E))
Generated subgoals:

None

About:
applyall

PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc