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
s being
Element of
C -States the
generators of
G for
t1,
t2 being
Element of
T,
I holds
(init.array (t1,t2)) value_at (
C,
s)
= init.array (
(t1 value_at (C,s)),
(t2 value_at (C,s)))