At: totalorder switchable0 1
1. 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
By:
Ext
THEN
Try (Fold `trace_property` 0)
THEN
Unfolds [`totalorder`;`local_deliver_property`] 0
THEN
Reduce 0
Generated subgoals:None
About:
