E:EventStruct, L:|E| List.
L = nil 
Causal(E)(L) (
i:
||L||. is-send(E)(L[i]))L:T List. L = nil (x:T. (x 
L))| Theorem | Name |
|
Thm* E:EventStruct, L:|E| List.
L = nil Causal(E)(L) (i:||L||. is-send(E)(L[i])) | [P_causal_non_nil] |
| cites | |
|
Thm* L:T List. L = nil (x:T. (x L)) | [member_exists] |