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

At: no duplicate send layer

E:EventStruct. layerR(E)^-1 preserves No-dup-send(E)
By:
Auto
THEN
Unfold `layer_rel` 0
THEN
Assert ((asyncR(E) delayableR(E)) send-enabledR(E)^-1)^* preserves No-dup-send(E)
Generated subgoals:

11. E: EventStruct
((asyncR(E) delayableR(E)) send-enabledR(E)^-1)^* preserves No-dup-send(E)
21. E: EventStruct
2. ((asyncR(E) delayableR(E)) send-enabledR(E)^-1)^* preserves No-dup-send(E)
((asyncR(E) delayableR(E)) send-enabledR(E))^*^-1 preserves No-dup-send(E)

About:
listall

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