E:EventStruct, tr:|E| List.
Causal(E)(tr) 
(tr':|E| List. tr' 
tr 
(x
tr'.(
ytr'.is-send(E)(y) & (y =msg=(E) x))))l1,l2:T List. l1 l2 ||l1||||l2||| Theorem | Name |
|
Thm* E:EventStruct, tr:|E| List.
Causal(E)(tr) (tr':|E| List. tr' tr (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))) | [P_causal_iff] |
| cites | |
|
Thm* l1,l2:T List. l1 l2 ||l1||||l2|| | [iseg_length] |