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
V3()
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,
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
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
f in C -Execution (
A,
b,
(\false C)) &
G is
C -supported &
i <> m holds
(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)))))) is_terminating_wrt f,
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }