is mentioned by

Thm* E:EventStruct, x:|E| List, j,z:||x||. Dec(j switchR(x) z)	[decidable__switch_inv_rel]
Thm* E:EventStruct, tr:|E| List, x,y:|E|. Dec(x somewhere delivered before y)	[decidable__delivered_before_somewhere]
Thm* E:TaggedEventStruct, tr:|E| List, x,y:|E|. Dec(R_ad_normal(tr)(x,y))	[decidable__R_ad_normal]
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]

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

Try larger context: GenAutomata