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 V3() ManySortedSet of the carrier of S
for T being non-empty b₂,b₁ -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 i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for s being Element of C -States the generators of G
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))