is mentioned by

Thm* E:EventStruct, tr:|E| List, ls:||tr||. is-send(E)(tr[ls]) (j:||tr||. ls < j is-send(E)(tr[j])) (i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls))	[switch_inv_rel_closure_lemma1]
Def switch-decomposable(E)(L) == L = nil |E| List (Q:(||L||Prop). (i:||L||. Dec(Q(i))) & (i:||L||. Q(i)) & (i:||L||. Q(i) (is-send(E)(L[i]))) & (i,j:||L||. Q(i) Q(j) tag(E)(L[i]) = tag(E)(L[j])) & (i,j:||L||. Q(i) ij C(Q)(j)))	[switch_decomposable]
Def x somewhere delivered before y == k:||tr||. x delivered at time k & (k':||tr||. y delivered at time k' loc(E)(tr[k']) = loc(E)(tr[k]) kk')	[delivered_before_somewhere]
Def Causal(E)(tr) == i:||tr||. j:||tr||. ji & (is-send(E)(tr[j])) & (tr[j] =msg=(E) tr[i])	[P_causal]

In prior sections: int 1 bool 1 int 2 list 1 mb nat num thy 1 mb list 1 core

Try larger context: GenAutomata