E:EventStruct, A:Type, f:(A
|E|), P:((|E| List)Prop).
switchable(E)(P) 
switchable(induced_event_str(E;A;f))(P o f)P:(AAProp), f:(BA), x,y:B List.
(x swap adjacent[P(f(x),f(y))] y) (map(f;x) swap adjacent[P(x,y)] map(f;y))| Rank | Theorem | Name |
| 2 |
Thm* E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop).
switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f) | [switchable_induced] |
| cites | ||
| 1 |
Thm* P:(AAProp), f:(BA), x,y:B List.
(x swap adjacent[P(f(x),f(y))] y) (map(f;x) swap adjacent[P(x,y)] map(f;y)) | [swap_adjacent_map] |