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 y 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 i1, i2 being pure Element of the generators of G . I
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)) & not T is array-degenerated & X is countable holds
for J being Algorithm of A st ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ( for D being array of (#INT,<=#) st D = (s . (the_array_sort_of S)) . M holds
( ( D <> {} implies ( ((f . (s,J)) . I) . i1 in dom D & ((f . (s,J)) . I) . i2 in dom D ) ) & ( inversions D <> {} implies [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions D ) & ( ((f . (s,J)) . the bool-sort of S) . b = TRUE implies inversions D <> {} ) & ( inversions D <> {} implies ((f . (s,J)) . the bool-sort of S) . b = TRUE ) ) ) ) ) holds
for D being finite 0 -based array of (#INT,<=#) st D = (s . (the_array_sort_of S)) . M & y <> i1 & y <> i2 holds
( ((f . (s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))))) . (the_array_sort_of S)) . M is ascending permutation of D & ( J is absolutely-terminating implies while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))) is_terminating_wrt f, { s1 where s1 is Element of C -States the generators of G : (s1 . (the_array_sort_of S)) . M <> {} } ) )