is mentioned by

Thm* E:TaggedEventStruct, x:|E| List, i:(||x||-1). switch_inv(E)(x) is-send(E)(x[(i+1)]) is-send(E)(x[i]) loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1))	[switch_inv_swap]
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]
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]
Def asyncR(E) == swap adjacent[loc(E)(x) = loc(E)(y) & (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))]	[R_async]
Def delayableR(E) == swap adjacent[(x =msg=(E) y) & (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))]	[R_delayable]
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 Macro x R_del(E) y == (x =msg=(E) y) & is-deliver(E)(x) & (is-send(E)(y)) (is-send(E)(x)) & is-deliver(E)(y)	[R_del]

In prior sections: core bool 1 rel 1 sqequal 1 int 2 list 1 prog 1 mb nat num thy 1 mb list 1 mb list 2 mb collection mb automata 1

Try larger context: GenAutomata