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
A being
IfWhileAlgebra of the
generators of
G for
I being
integer SortSymbol of
S for
m,
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
f being
ExecutionFunction of
A,
C -States the
generators of
G,
(\false C) -States ( the
generators of
G,
b) st
f in C -Execution (
A,
b,
(\false C)) &
G is
C -supported &
i <> m &
(s . (the_array_sort_of S)) . M <> {} holds
for
n being
Nat st
((f . (s,((m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))))) . I) . m = n holds
for
X being non
empty finite integer-membered set st
X = rng ((s . (the_array_sort_of S)) . M) holds
(M . (n,I)) value_at (
C,
s)
= max X