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]
Thm* E:TaggedEventStruct, tr:|E| List, ls:||tr||. switch_inv(E)(tr) (i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j]))	[switch_inv_rel_closure]
Thm* E:EventStruct, tr:|E| List, ls,i:||tr||. is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i])	[switch_inv_rel_closure_send]
Def adR(E) == (delayableR(E) asyncR(E))^*	[R_ad]
Def layerR(E) == ((asyncR(E) delayableR(E)) send-enabledR(E))^*	[layer_rel]
Def R(tg) == swap adjacent[tg(x) = tg(y) Label]^*	[tag_rel]

In prior sections: mb nat mb list 1 mb list 2

Try larger context: GenAutomata