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

At: local deliver switchable 6

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)

delayableR(E) preserves tr.P(p.tr delivered at p)

By:
Unfolds [`preserved_by`;`R_delayable`] 0
THEN
Reduce 0
THEN
Subst ((p.y delivered at p) = (p.x delivered at p)) 0
THEN
Ext
THEN
Reduce 0
THEN
Unfold `deliveries_at` 0
THEN
Using [`f',(e.is-send(E)(e)loc(E)(e) = x1)] (FwdThru Thm* P:(AAProp), f:(A), L1,L2:A List. (L1 swap adjacent[P(x,y)] L2) (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) filter(f;L1) = filter(f;L2) [-2])
THEN
Analyze -1
THEN
Unfold `swap_adjacent` -1
THEN
Reduce -1
THEN
ExRepD
THEN
Inst Thm* P:(T), L:T List. (xfilter(P;L).P(x)) [|E|;e.is-send(E)(e)loc(E)(e) = x1;x]
THEN
Unfold `l_all` -1
THEN
Reduce -1
THEN
RW assert_pushdownC -1
THEN
Analyze -3
THEN
ExRepD


Generated subgoals:

16. x: |E| List
7. y: |E| List
8. P(p.x delivered at p)
9. x swap adjacent[(x =msg=(E) y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y
10. x1: Label
11. i: (||filter(e.is-send(E)(e)loc(E)(e) = x1;x)||-1)
12. (filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i] =msg=(E) filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)])
13. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i])
14. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)])
15. filter(e.is-send(E)(e)loc(E)(e) = x1;y) = swap(filter(e.is-send(E)(e)loc(E)(e) = x1;x);i;i+1)
16. x@0:|E|. (x@0 filter(e.is-send(E)(e)loc(E)(e) = x1;x)) is-send(E)(x@0) & loc(E)(x@0) = x1
filter(e.is-send(E)(e)loc(E)(e) = x1;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x)
26. x: |E| List
7. y: |E| List
8. P(p.x delivered at p)
9. x swap adjacent[(x =msg=(E) y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y
10. x1: Label
11. i: (||filter(e.is-send(E)(e)loc(E)(e) = x1;x)||-1)
12. (filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i] =msg=(E) filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)])
13. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i])
14. is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)])
15. filter(e.is-send(E)(e)loc(E)(e) = x1;y) = swap(filter(e.is-send(E)(e)loc(E)(e) = x1;x);i;i+1)
16. x@0:|E|. (x@0 filter(e.is-send(E)(e)loc(E)(e) = x1;x)) is-send(E)(x@0) & loc(E)(x@0) = x1
filter(e.is-send(E)(e)loc(E)(e) = x1;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x)


About:
listassertlambdaapplyfunctionequalpropimpliesallexists

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