is mentioned by

Thm* E:EventStruct, a,b,c:|E|, tr:|E| List. a somewhere delivered before b a somewhere delivered before c c somewhere delivered before b	[delivered_before_somewhere_lemma]
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, x,y:|E|. Dec(x somewhere delivered before y)	[decidable__delivered_before_somewhere]
Def switchR(tr)(i,j) == (is-send(E)(tr[i])) & (is-send(E)(tr[j])) & i < j & tr[j] somewhere delivered before tr[i] j < i & tr[i] somewhere delivered before tr[j]	[switch_inv_rel]

Try larger context: GenAutomata