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

At: totalorder switchable0 2 1 1
1. E: EventStruct
2. f: Label(|E| List)
3. g: Label(|E| List)
4. 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)))
By:
BackThruLemma' Thm* as2,bs2,as1,bs1:T List. as1 as2 bs1 bs2 agree_on_common(T;as2;bs2) agree_on_common(T;as1;bs1)
THEN
BackThru Thm* f:(AB), L1,L2:A List. L1 L2 map(f;L1) map(f;L2)
Generated subgoals:

None

About:
listapplyfunction

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