E:EventStruct, tr:|E| List.
Causal(E)(tr) 
(tr':|E| List. tr' 
tr 
(x
tr'.(
ytr'.is-send(E)(y) & (y =msg=(E) x))))xL.P(x)) == x:T. (x L) & P(x)
is mentioned by
|
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] |
Try larger context: GenAutomata