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

At: local deliver switchable 3
1. E: EventStruct
2. P: (Label(|E| List))Prop
3. f,g:(Label(|E| List)). (p:Label. g(p) f(p)) P(f) P(g)
4. f,g:(Label(|E| List)). (a:|E|. p:Label. g(p) = filter(b.(b =msg=(E) a);f(p))) P(f) P(g)
5. 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)

(ternary) composableR(E) preserves tr.P(p.tr delivered at p)
By:
Unfolds [`preserved_by2`;`R_composable`] 0
THEN
Reduce 0
THEN
SubstFor z 0
THEN
BackThruHyp' 5
THEN
Reduce 0
Generated subgoals:

15. x: |E| List
6. y: |E| List
7. z: |E| List
8. (xx.(yy.(x =msg=(E) y)))
9. z = (x @ y)
10. 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)
11. p: Label
12. q: Label
(xx delivered at p.(yy delivered at q.(x =msg=(E) y)))
25. x: |E| List
6. y: |E| List
7. z: |E| List
8. (xx.(yy.(x =msg=(E) y)))
9. z = (x @ y)
10. 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)
11. p: Label
x @ y delivered at p = (x delivered at p @ y delivered at p)

About:
listassertlambdaapplyfunctionequalpropimpliesallexists

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