Nuprl - Pf local_deliver_switchable 1

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

At: local deliver switchable 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)

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

By: Unfolds [`preserved_by`;`R_safety`] 0 THEN Reduce 0 THEN BackThruHyp' 3 THEN Reduce 0 THEN Unfold `deliveries_at` 0 THEN BackThru Thm* P:(T), L2,L1:T List. L1 L2 filter(P;L1) filter(P;L2)

Generated subgoals:

None

About:

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