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

At: totalorder switchable0 2 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)))

agree_on_common(|MS(E)|;map(msg(E);filter(b.(b =msg=(E) a);f(p)));map(msg(E);filter(b. (b =msg=(E) a);f(q))))
By: Subst ((b.(b =msg=(E) a)) = (b.(b =(MS(E)) (msg(E)(a)))) o msg(E)) 0
Generated subgoals:

1 (b.(b =msg=(E) a)) = (b.(b =(MS(E)) (msg(E)(a)))) o msg(E)
2 agree_on_common(|MS(E)|;map(msg(E);filter((b.(b =(MS(E)) (msg(E)(a)))) o msg(E);f(p)));map(msg(E);filter((b.(b =(MS(E)) (msg(E)(a)))) o msg(E);f(q))))

About:
listboollambdaapplyfunctionequalall

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