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: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, 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]
Thm* E:EventStruct, x:|E| List, j,z:||x||. Dec(j switchR(x) z)	[decidable__switch_inv_rel]

Try larger context: GenAutomata