is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List. switch_inv(E)(tr) (i,j:||tr||. (i switchR(tr) j) tag(E)(tr[i]) = tag(E)(tr[j]))	[switch_inv_rel_same_tag]
Thm* E:EventStruct, a,b:|E|, tr:|E| List. a somewhere delivered before b (k:||tr||. a delivered at time k (k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])))	[not_delivered_before_somewhere]
Thm* E:EventStruct, tr:|E| List. No-dup-deliver(E)(tr) (x,y:|E|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr))	[P_no_dup_iff]
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]

In prior sections: core fun 1 well fnd int 1 bool 1 rel 1 int 2 list 1 mb basic mb nat num thy 1 mb list 1 mb label mb list 2 mb structures mb collection mb automata 1

Try larger context: GenAutomata