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

At: totalorder switchable0 2 2

1. E: EventStruct
2. f: Label(|E| List)
3. g: Label(|E| List)
4. a:|E|. p:Label. g(p) = filter(b.(b =msg=(E) a);f(p))
5. p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
6. p: Label
7. q: Label

agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))

By:
ExRepD
THEN
InstHyp [p] -4
THEN
HypSubst -1 0
THEN
Thin -1
THEN
InstHyp [q] -4
THEN
HypSubst -1 0
THEN
Thin -1
THEN
InstHyp [p;q] -3


Generated subgoal:

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


About:
listlambdaapplyfunctionequalallexists

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