At: totalorder switchable0 2 2 1 2 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)))
10. filter(
b.
(b =(MS(E)) (msg(E)(a)));map(msg(E);f(p)))
=
map(msg(E);filter((
b.
(b =(MS(E)) (msg(E)(a)))) o msg(E);f(p)))
11. filter(
b.
(b =(MS(E)) (msg(E)(a)));map(msg(E);f(q)))
=
map(msg(E);filter((
b.
(b =(MS(E)) (msg(E)(a)))) o msg(E);f(q)))
agree_on_common(|MS(E)|;filter(
b.
(b =(MS(E)) (msg(E)(a)));map(msg(E);f(p)));filter(
b.

(b =(MS(E)) (msg(E)(a)));map(msg(E);f(q))))
By: BackThru
Thm*
P:(T

), as,bs:T List.
agree_on_common(T;as;bs) 
agree_on_common(T;filter(P;as);filter(P;bs))
Generated subgoals:None
About: