Nuprl - Pf local_deliver_switchable 2 1

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

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

a1:|E|. p:Label. (p.filter(b.(b =msg=(E) a);x) delivered at p)(p) = filter(b.(b =msg=(E) a1);(p.x delivered at p)(p)) |E| List

By: Reduce 0 THEN InstConcl [a] THEN Unfold `deliveries_at` 0 THEN RW FilterFilterC 0 THEN Reduce 0

Generated subgoal:

1 7. p: Label
filter(t.(is-send(E)(t)loc(E)(t) = p)(t =msg=(E) a);x) = filter(t.(t =msg=(E) a)is-send(E)(t)loc(E)(t) = p;x)

About:

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