E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop). switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f)

1	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. x,y:|E| List. P(x) (x safetyR(E) y) P(y) x,y:A List. P(map(f;x)) (x safetyR(induced_event_str(E;A;f)) y) P(map(f;y))
2	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. x,y:|E| List. P(x) (x memorylessR(E) y) P(y) x,y:A List. P(map(f;x)) (x memorylessR(induced_event_str(E;A;f)) y) P(map(f;y))
3	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. x,y,z:|E| List. P(x) P(y) composableR(E)(x,y,z) P(z) x,y,z:A List. P(map(f;x)) P(map(f;y)) composableR(induced_event_str(E;A;f))(x,y,z) P(map(f;z))
4	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. x,y:|E| List. P(x) (x send-enabledR(E) y) P(y) x,y:A List. P(map(f;x)) (x send-enabledR(induced_event_str(E;A;f)) y) P(map(f;y))
5	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. x,y:|E| List. P(x) (x asyncR(E) y) P(y) x,y:A List. P(map(f;x)) (x asyncR(induced_event_str(E;A;f)) y) P(map(f;y))
6	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. x,y:|E| List. P(x) (x delayableR(E) y) P(y) x,y:A List. P(map(f;x)) (x delayableR(induced_event_str(E;A;f)) y) P(map(f;y))
7	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. tr:|E| List. P(tr) Causal(E)(tr) tr:A List. P(map(f;tr)) Causal(induced_event_str(E;A;f))(tr)
8	1. E: EventStruct 2. A: Type 3. f: A|E| 4. P: (|E| List)Prop 5. tr:|E| List. P(tr) No-dup-deliver(E)(tr) tr:A List. P(map(f;tr)) No-dup-deliver(induced_event_str(E;A;f))(tr)

About: