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

At: totalorder switchable0 2 1

1. E: EventStruct
2. f: Label(|E| List)
3. g: Label(|E| List)
4. p:Label. g(p) 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:
InstHyp [p] 4
THEN
InstHyp [q] 4
THEN
Thin 4
THEN
InstHyp [p;q] 4
THEN
Thin 4


Generated subgoal:

14. p: Label
5. q: Label
6. g(p) f(p)
7. g(q) f(q)
8. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))


About:
listapplyfunctionall

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