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

At: totalorder switchable0 2 2 1 2

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 =(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))))

By:
Inst Thm* f:(T1T2), Q:(T2), L:T1 List. filter(Q;map(f;L)) = map(f;filter(Q o f;L)) [|E|;|MS(E)|;msg(E);b.(b =(MS(E)) (msg(E)(a)));f(p)]
THEN
RevHypSubst -1 0
THEN
Inst Thm* f:(T1T2), Q:(T2), L:T1 List. filter(Q;map(f;L)) = map(f;filter(Q o f;L)) [|E|;|MS(E)|;msg(E);b.(b =(MS(E)) (msg(E)(a)));f(q)]
THEN
RevHypSubst -1 0


Generated subgoal:

110. 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))))


About:
listlambdaapplyfunctionequalall

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