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

At: totalorder switchable0

E:EventStruct. switchable0(E)(totalorder(E))
By:
Auto
THEN
Subst (totalorder(E) = local_deliver_property(E;f.p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q))))) 0
Generated subgoals:

11. E: EventStruct
totalorder(E) = local_deliver_property(E;f.p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))) (|E| List)Prop
21. E: EventStruct
switchable0(E) (local_deliver_property(E;f.p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))))

About:
listlambdaapplyfunctionequalpropall

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