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

At: totalorder switchable0 2
1. E: EventStruct

switchable0(E) (local_deliver_property(E;f.p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))))
By:
BackThru Thm* E:EventStruct, P:((Label(|E| List))Prop). (f,g:(Label(|E| List)). (p:Label. g(p) f(p)) P(f) P(g)) (f,g:(Label(|E| List)). (a:|E|. p:Label. g(p) = filter(b.(b =msg=(E) a);f(p))) P(f) P(g)) (f,g,h:(Label(|E| List)). (p,q:Label. (xf(p).(yg(q).(x =msg=(E) y)))) (p:Label. h(p) = ((f(p)) @ (g(p)))) P(f) P(g) P(h)) switchable0(E)(local_deliver_property(E;P))
THEN
Reduce 0
Generated subgoals:

12. 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)))
22. 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)))
32. f: Label(|E| List)
3. g: Label(|E| List)
4. h: Label(|E| List)
5. p,q:Label. (xf(p).(yg(q).(x =msg=(E) y)))
6. p:Label. h(p) = ((f(p)) @ (g(p)))
7. p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
8. p,q:Label. agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))
9. p: Label
10. q: Label
agree_on_common(|MS(E)|;map(msg(E);h(p));map(msg(E);h(q)))

About:
lambdaapplyall

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