E:EventStruct.
switchable(E)(totalorder(E) 
Causal(E) No-dup-deliver(E))E:EventStruct. switchable0(E)(totalorder(E))E:EventStruct, P:TraceProperty(E).
switchable0(E)(P) 
switchable(E)(P Causal(E) No-dup-deliver(E))| Rank | Theorem | Name |
| 8 |
Thm* E:EventStruct.
switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E)) | [totalorder_switchable] |
| cites | ||
| 7 |
Thm* E:EventStruct. switchable0(E)(totalorder(E)) | [totalorder_switchable0] |
| 5 |
Thm* E:EventStruct, P:TraceProperty(E).
switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |