|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) i
j C(Q)(j)))k:||L||. Q(k) & (L[k] =msg=(E) L[i])
is mentioned by
|
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] |
Try larger context: GenAutomata