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) |
2 | 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) memorylessR(E) preserves tr.P(p.tr delivered at p) |
3 | 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) (ternary) composableR(E) preserves tr.P(p.tr delivered at p) |
4 | 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) send-enabledR(E) preserves tr.P(p.tr delivered at p) |
5 | 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) asyncR(E) preserves tr.P(p.tr delivered at p) |
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) |
About: