At: local deliver switchable 4 1 1 1
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. (x
f(p).(yg(q).(x =msg=(E) y))))
(p:Label. h(p) = ((f(p)) @ (g(p)))) P(f) P(g) P(h)
6. x: |E| List
7. y: |E| List
8. P(p.x delivered at p)
9. x@0: |E|
10. is-send(E)(x@0)
11. y = (x @ [x@0])
12. x1: Label
13. is-send(E)(x@0)
(filter(e.is-send(E)(e)
loc(E)(e) =
x1;x) @ nil)
=
filter(e.is-send(E)(e)loc(E)(e) = x1;x)
By: BackThru
Thm* as:T List. (as @ nil) = as
Generated subgoals:None
About:
