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

At: P no dup switchable0

E:EventStruct. switchable0(E)(No-dup-deliver(E))
By:
Unfold `switchable0` 0
THEN
Reduce 0
Generated subgoals:

11. E: EventStruct
safetyR(E) preserves No-dup-deliver(E)
21. E: EventStruct
memorylessR(E) preserves No-dup-deliver(E)
31. E: EventStruct
(ternary) composableR(E) preserves No-dup-deliver(E)
41. E: EventStruct
send-enabledR(E) preserves No-dup-deliver(E)
51. E: EventStruct
asyncR(E) preserves No-dup-deliver(E)
61. E: EventStruct
delayableR(E) preserves No-dup-deliver(E)

About:
listapplyall

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