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

At: local deliver switchable 4 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. (xf(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])

P(p.x @ [x@0] delivered at p)

By:
Subst ((p.x @ [x@0] delivered at p) = (p.x delivered at p)) 0
THEN
Ext
THEN
Reduce 0


Generated subgoal:

112. x1: Label
x @ [x@0] delivered at x1 = x delivered at x1


About:
listconsnilassertlambdaapplyfunction
equalpropimpliesallexists

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