At: totalorder switchable0 2 2 1 1
1. E: EventStruct
2. f: Label
(|E| List)
3. g: Label(|E| List)
4. a: |E|
5. 
p:Label. g(p) = filter(
b.
(b =msg=(E) a);f(p))
6. p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
7. p: Label
8. q: Label
9. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
(b.(b =msg=(E) a)) = (b.(b =(MS(E)) (msg(E)(a)))) o msg(E)
By:
Unfold `event_msg_eq` 0
THEN
Reduce 0
THEN
Ext
THEN
Reduce 0
Generated subgoals:None
About:
