mb
hybrid
Sections
GenAutomata
Doc
Def
swap(L;i;j) == (L o (i, j))
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]
Def
swap adjacent[P(x;y)](L1,L2) ==
i:
(||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1)
A List
[swap_adjacent]
In prior sections:
mb
list
2
Try larger context:
GenAutomata
mb
hybrid
Sections
GenAutomata
Doc