theorem
for
S being non
empty non
void 1-1-connectives bool-correct 4,1
integer 11,1,1
-array 11
array-correct BoolSignature for
X being
non-empty ManySortedSet of the
carrier of
S for
T being
non-empty b2,
b1 -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over
S for
C being
bool-correct 4,1
integer 11,1,1
-array image of
T for
G being
basic GeneratorSystem over
S,
X,
T for
I being
integer SortSymbol of
S for
M being
pure Element of the
generators of
G . (the_array_sort_of S) for
s being
Element of
C -States the
generators of
G for
j being
Integer st
j in dom ((s . (the_array_sort_of S)) . M) &
M . (
j,
I)
in the
generators of
G . I holds
((s . (the_array_sort_of S)) . M) . j = (s . I) . (M . (j,I))