let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₁,S -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 <> {} } ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -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 <> {} } ) )
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: 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 <> {} } ) )
let C be bool-correct 4,1 integer 11,1,1 -array image of T; :: thesis: 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 <> {} } ) )
let G be basic GeneratorSystem over S,X,T; :: thesis: 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 <> {} } ) )
let I be integer SortSymbol of S; :: thesis: 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 <> {} } ) )
let y be pure Element of the generators of G . I; :: thesis: 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 <> {} } ) )
let M be pure Element of the generators of G . (the_array_sort_of S); :: thesis: 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 <> {} } ) )
let b be pure Element of the generators of G . the bool-sort of S; :: thesis: 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 <> {} } ) )
let s be Element of C -States the generators of G; :: thesis: 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 <> {} } ) )
let i1, i2 be pure Element of the generators of G . I; :: thesis: 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 <> {} } ) )
let A be elementary IfWhileAlgebra of the generators of G; :: thesis: 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 <> {} } ) )
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & not T is array-degenerated & X is countable implies 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 <> {} } ) ) )
assume A1: G is integer-array ; :: thesis: ( not G is C -supported or not f in C -Execution (A,b,(\false C)) or T is array-degenerated or not X is countable or 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 <> {} } ) ) )
assume A2: G is C -supported ; :: thesis: ( not f in C -Execution (A,b,(\false C)) or T is array-degenerated or not X is countable or 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 <> {} } ) ) )
assume A3: f in C -Execution (A,b,(\false C)) ; :: thesis: ( T is array-degenerated or not X is countable or 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 <> {} } ) ) )
assume A4: not T is array-degenerated ; :: thesis: ( not X is countable or 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 <> {} } ) ) )
assume A5: X is countable ; :: thesis: 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 <> {} } ) )
let J be Algorithm of A; :: thesis: ( ( 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 ) ) ) ) ) implies 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 <> {} } ) ) )
assume A6: 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 ) ) ) ) ; :: thesis: 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 <> {} } ) )
let D be finite 0 -based array of (#INT,<=#); :: thesis: ( D = (s . (the_array_sort_of S)) . M & y <> i1 & y <> i2 implies ( ((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 <> {} } ) ) )
assume A7: D = (s . (the_array_sort_of S)) . M ; :: thesis: ( not y <> i1 or not y <> i2 or ( ((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 <> {} } ) ) )
assume A8: ( y <> i1 & y <> i2 ) ; :: thesis: ( ((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 <> {} } ) )
deffunc H₁( Nat, Element of C -States the generators of G) -> Element of C -States the generators of G = f . ($2,(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))));
set ST = C -States the generators of G;
A9: the_array_sort_of S <> I by Th73;
consider g being Function of NAT,(C -States the generators of G) such that
A10: ( g . 0 = s & ( for i being Nat holds g . (i + 1) = H₁(i,g . i) ) ) from NAT_1:sch 12();
A11: the carrier of (#INT,<=#) = INT by LFUZZY_0:def 3;
deffunc H₂( object ) -> set = ((g . (In ($1,NAT))) . (the_array_sort_of S)) . M;
A12: for x being object st x in NAT holds
H₂(x) in INT ^omega by AFINSQ_1:def 7;
consider h being Function of NAT,(INT ^omega) such that
A13: for i being object st i in NAT holds
h . i = H₂(i) from FUNCT_2:sch 2(A12);
A14: ( dom h = NAT & dom g = NAT ) by FUNCT_2:def 1;
then A15: h is non empty Sequence by ORDINAL1:def 7;
then A16: base- h = 0 by EXCHSORT:24;
then A17: h . (base- h) = ((g . (In (0,NAT))) . (the_array_sort_of S)) . M by A13
.= D by A7, A10 ;
A18: for a being Ordinal st a in dom g holds
h . a is array of (#INT,<=#)

proof

let a be Ordinal; :: thesis: ( a in dom g implies h . a is array of (#INT,<=#) )
assume a in dom g ; :: thesis: h . a is array of (#INT,<=#)
then a in NAT by FUNCT_2:def 1;
then h . a in INT ^omega by FUNCT_2:5;
hence h . a is array of (#INT,<=#) by A11; :: thesis: verum

end;

set TV = (\false C) -States ( the generators of G,b);

hereby :: thesis: ( 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 <> {} } )

per cases ( D = {} or D <> {} ) ;

suppose A19: D = {} ; :: thesis: ((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

then inversions D = {} ;
then ((f . (s,J)) . the bool-sort of S) . b <> TRUE by A6, A7;
then A20: ((f . (s,J)) . the bool-sort of S) . b = FALSE by XBOOLEAN:def 3
.= \false C by Th10 ;
f . (s,J) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
then ( f . (s,J) nin (\false C) -States ( the generators of G,b) & f complies_with_while_wrt (\false C) -States ( the generators of G,b) ) by A20, AOFA_000:def 32, AOFA_A00:def 20;
then A21: f . (s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))))) = f . (s,J) ;
((f . (s,J)) . (the_array_sort_of S)) . M = D by A6, A7;
hence ((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 by A19, A21, EXCHSORT:38; :: thesis: verum

end;

suppose A22: D <> {} ; :: thesis: ((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

defpred S₁[ Nat] means h . $1 <> {} ;
A23: S₁[ 0 ] by A22, A17, A15, EXCHSORT:24;
A24: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A25: S₁[i] ; :: thesis: S₁[i + 1]
A26: I <> the_array_sort_of S by Th73;
A27: h . i = ((g . (In (i,NAT))) . (the_array_sort_of S)) . M by A13
.= ((g . i) . (the_array_sort_of S)) . M ;
reconsider R = h . i as array of (#INT,<=#) by A18, A14, ORDINAL1:def 12;
A28: h . (i + 1) = ((g . (In ((i + 1),NAT))) . (the_array_sort_of S)) . M by A13
.= ((f . ((g . i),(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))) . (the_array_sort_of S)) . M by A10
.= ((f . ((f . ((g . i),((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 29
.= ((f . ((f . ((f . ((g . i),(J \; (y := (((@ M) . (@ i1)),A))))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 29
.= ((f . ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 29 ;
(@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . I) . i1 by Th61
.= ((f . ((g . i),J)) . I) . i1 by A2, A3, A8, Th65 ;
then A29: (@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) in dom R by A6, A25, A27;
A30: (@ M) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M by Th61;
((f . ((g . i),J)) . (the_array_sort_of S)) . M = ((g . i) . (the_array_sort_of S)) . M by A6;
then A31: ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M = ((g . i) . (the_array_sort_of S)) . M by A2, A3, A26, Th65;
((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M = ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . (the_array_sort_of S)) . M by A1, A2, A3, A4, A5, Th99
.= (((@ M),(@ i1)) <- ((@ M) . (@ i2))) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))))),((@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))))) <- (((@ M) . (@ i2)) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))))) by Th80
.= (((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M) +* (((@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))))),(((@ M) . (@ i2)) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))))) by A29, A31, A27, A30, Th74 ;
then A32: dom (((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M) = dom (((g . i) . (the_array_sort_of S)) . M) by A31, FUNCT_7:30;
A33: (@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) = ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M by Th61;
(@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) = ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . I) . i2 by Th61
.= ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . i2 by A1, A2, A3, A4, A5, Th99
.= ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 by A2, A3, Th73, Th65
.= ((f . ((g . i),J)) . I) . i2 by A2, A3, A8, Th65 ;
then A34: (@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) in dom R by A6, A25, A27;
A35: ((f . ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M = ((f . ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A)))) . (the_array_sort_of S)) . M by A1, A2, A3, A4, A5, Th99
.= (((@ M),(@ i2)) <- (@ y)) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))),((@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))))) <- ((@ y) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))) by Th80
.= ((@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))) +* (((@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))),((@ y) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))))) by A32, A33, A34, A27, Th74 ;
dom (((@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))) +* (((@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))),((@ y) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))))) = dom (((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M) by A33, FUNCT_7:30;
hence h . (i + 1) <> {} by A35, A28, A27, A25, A32; :: thesis: verum

end;

A36: for i being Nat holds S₁[i] from NAT_1:sch 2(A23, A24);
A37: for a being Nat
for R being array of (#INT,<=#) st R = h . a holds
for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )

proof

let a be Nat; :: thesis: for R being array of (#INT,<=#) st R = h . a holds
for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )
let R be array of (#INT,<=#); :: thesis: ( R = h . a implies for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) ) )
assume A38: R = h . a ; :: thesis: for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )
let s1 be Element of C -States the generators of G; :: thesis: ( g . a = s1 implies ex x, y being set st
( x = ((f . (s1,J)) . I) . i1 & y = ((f . (s1,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) ) )
assume A39: g . a = s1 ; :: thesis: ex x, y being set st
( x = ((f . (s1,J)) . I) . i1 & y = ((f . (s1,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )
reconsider i = a as Element of NAT by ORDINAL1:def 12;
reconsider s = g . i as Element of C -States the generators of G ;
set y1 = ((f . (s,J)) . I) . i1;
set y2 = ((f . (s,J)) . I) . i2;
take ((f . (s,J)) . I) . i1 ; :: thesis: ex y being set st
( ((f . (s,J)) . I) . i1 = ((f . (s1,J)) . I) . i1 & y = ((f . (s1,J)) . I) . i2 & ((f . (s,J)) . I) . i1 in dom R & y in dom R & h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),y) )
take ((f . (s,J)) . I) . i2 ; :: thesis: ( ((f . (s,J)) . I) . i1 = ((f . (s1,J)) . I) . i1 & ((f . (s,J)) . I) . i2 = ((f . (s1,J)) . I) . i2 & ((f . (s,J)) . I) . i1 in dom R & ((f . (s,J)) . I) . i2 in dom R & h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
thus ( ((f . (s,J)) . I) . i1 = ((f . (s1,J)) . I) . i1 & ((f . (s,J)) . I) . i2 = ((f . (s1,J)) . I) . i2 ) by A39; :: thesis: ( ((f . (s,J)) . I) . i1 in dom R & ((f . (s,J)) . I) . i2 in dom R & h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
In (i,NAT) = i ;
then A40: h . i = ((g . i) . (the_array_sort_of S)) . M by A13;
R <> {} by A36, A38;
hence A41: ( ((f . (s,J)) . I) . i1 in dom R & ((f . (s,J)) . I) . i2 in dom R ) by A40, A6, A38; :: thesis: h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2))
A42: ( succ (Segm a) = Segm (i + 1) & In ((i + 1),NAT) = i + 1 ) by NAT_1:38;
then A43: h . (succ a) = ((g . (i + 1)) . (the_array_sort_of S)) . M by A13;
A44: g . (i + 1) = f . (s,(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))) by A10
.= f . ((f . (s,((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A))) by AOFA_000:def 29
.= f . ((f . ((f . (s,(J \; (y := (((@ M) . (@ i1)),A))))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A))) by AOFA_000:def 29
.= f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A))) by AOFA_000:def 29
.= f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A))) by A1, A2, A3, A4, A5, Th99
.= f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A))) by A1, A2, A3, A4, A5, Th99 ;
set s1 = f . (s,J);
set s2 = f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)));
set s3 = f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)));
set s4 = f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A)));
A45: (@ i1) value_at (C,(f . (s,J))) = ((f . (s,J)) . I) . i1 by Th61;
A46: ((f . (s,J)) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A6;
A47: (@ M) value_at (C,(f . (s,J))) = ((f . (s,J)) . (the_array_sort_of S)) . M by Th61
.= (s . (the_array_sort_of S)) . M by A6 ;
A48: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . y = ((@ M) . (@ i1)) value_at (C,(f . (s,J))) by A2, A3, Th65
.= ((@ M) value_at (C,(f . (s,J)))) . ((@ i1) value_at (C,(f . (s,J)))) by Th79
.= R . (((f . (s,J)) . I) . i1) by A38, A41, A45, A40, A47, Th74 ;
A49: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i1 = ((f . (s,J)) . I) . i1 by A2, A3, A8, Th65;
A50: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 = ((f . (s,J)) . I) . i2 by A2, A3, A8, Th65;
A51: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M = ((f . (s,J)) . (the_array_sort_of S)) . M by A2, A3, A9, Th65;
A52: ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . y = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . y by A2, A3, Th73, Th65;
A53: ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . i2 = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 by A2, A3, Th73, Th65;
A54: (@ M) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M by Th61;
A55: (@ i1) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i1 by Th61;
A56: (@ i2) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 by Th61;
A57: ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . (the_array_sort_of S)) . M = (((@ M),(@ i1)) <- ((@ M) . (@ i2))) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))),((@ i1) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))))) <- (((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))) by Th80
.= R +* (((@ i1) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))),(((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))))) by A38, A54, A55, A46, A51, A49, A41, A40, Th74 ;
A58: (@ M) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) = ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . (the_array_sort_of S)) . M by Th61;
A59: (@ i2) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) = ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . i2 by Th61;
A60: (@ y) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) = ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . y by Th61;
A61: dom R = dom (R +* ((((f . (s,J)) . I) . i1),(((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))))) by FUNCT_7:30;
A62: ((f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A)))) . (the_array_sort_of S)) . M = (((@ M),(@ i2)) <- (@ y)) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))))),((@ i2) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))))) <- ((@ y) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))))) by Th80
.= (R +* ((((f . (s,J)) . I) . i1),(((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))))) +* ((((f . (s,J)) . I) . i2),((@ y) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))))) by A58, A59, A61, A55, A41, A57, A49, A53, A50, Th74 ;
((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((@ M) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))) . ((@ i2) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))) by Th79
.= R . (((f . (s,J)) . I) . i2) by A38, A41, A54, A56, A50, A51, A46, A40, Th74 ;
hence h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) by A42, A43, A44, A41, A60, A62, A52, A48, FUNCT_7:def 12; :: thesis: verum

end;

defpred S₂[ Nat] means h . $1 is permutation of D;
A63: S₂[ 0 ] by A17, A16, EXCHSORT:38;

A64: now :: thesis: for i being Nat st S₂[i] holds
S₂[i + 1]

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A65: S₂[i] ; :: thesis: S₂[i + 1]
thus S₂[i + 1] :: thesis: verum

proof

reconsider R = h . i as array of (#INT,<=#) by A18, A14, ORDINAL1:def 12;
reconsider s = g . i as Element of C -States the generators of G ;
consider x, y being set such that
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 ) and
A66: ( x in dom R & y in dom R & h . (i + 1) = Swap (R,x,y) ) by A37;
thus h . (i + 1) is permutation of D by A65, A66, EXCHSORT:44; :: thesis: verum

end;

end;

A67: for i being Nat holds S₂[i] from NAT_1:sch 2(A63, A64);
defpred S₃[ Nat] means ((g . $1) . (the_array_sort_of S)) . M is ascending permutation of D;
A68: ex i being Nat st S₃[i]

proof

assume A69: for i being Nat holds not S₃[i] ; :: thesis: contradiction
for a being Ordinal st a in dom h & succ a in dom h holds
ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) )

proof

let a be Ordinal; :: thesis: ( a in dom h & succ a in dom h implies ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) ) )
assume A70: a in dom h ; :: thesis: ( not succ a in dom h or ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) ) )
assume succ a in dom h ; :: thesis: ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) )
reconsider i = a as Element of NAT by A70, FUNCT_2:def 1;
reconsider R = h . i as array of (#INT,<=#) by A11;
reconsider s = g . i as Element of C -States the generators of G ;
set y1 = ((f . (s,J)) . I) . i1;
set y2 = ((f . (s,J)) . I) . i2;
take R ; :: thesis: ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) )
take ((f . (s,J)) . I) . i1 ; :: thesis: ex y being set st
( [(((f . (s,J)) . I) . i1),y] in inversions R & h . a = R & h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),y) )
take ((f . (s,J)) . I) . i2 ; :: thesis: ( [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions R & h . a = R & h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
In (i,NAT) = i ;
then A71: ( S₂[i] & not S₃[i] & h . i = ((g . i) . (the_array_sort_of S)) . M ) by A67, A69, A13;
then inversions R <> {} by EXCHSORT:48;
hence [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions R by A71, A6; :: thesis: ( h . a = R & h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
thus h . a = R ; :: thesis: h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2))
A72: succ (Segm i) = Segm (i + 1) by NAT_1:38;
consider x, y being set such that
A73: ( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (i + 1) = Swap (R,x,y) ) by A37;
thus h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) by A73, A72; :: thesis: verum

end;

then h is 0 -based arr_computation of D by A15, A14, A17, A18, EXCHSORT:def 14;
then h is finite by EXCHSORT:76;
hence contradiction by A14; :: thesis: verum

end;

consider B being Nat such that
A74: ( S₃[B] & ( for i being Nat st S₃[i] holds
B <= i ) ) from NAT_1:sch 5(A68);
reconsider h = h as Sequence of INT ^omega by A14, ORDINAL1:def 7;
reconsider c = h | (succ B) as array of INT ^omega ;
deffunc H₃( Nat) -> set = f . ((g . ($1 - 1)),J);
consider r being FinSequence such that
A75: ( len r = B + 1 & ( for i being Nat st i in dom r holds
r . i = H₃(i) ) ) from FINSEQ_1:sch 2();
rng r c= C -States the generators of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng r or x in C -States the generators of G )
assume x in rng r ; :: thesis: x in C -States the generators of G
then consider y being object such that
A76: ( y in dom r & x = r . y ) by FUNCT_1:def 3;
reconsider y = y as Nat by A76;
consider i being Nat such that
A77: y = 1 + i by A76, FINSEQ_3:25, NAT_1:10;
x = H₃(y) by A75, A76
.= f . ((g . i),J) by A77 ;
hence x in C -States the generators of G ; :: thesis: verum

end;

then reconsider r = r as non empty FinSequence of C -States the generators of G by A75, FINSEQ_1:def 4;
A78: 1 <= B + 1 by NAT_1:11;
A79: r . 1 = f . ((g . (1 - 1)),J) by A75, A78, FINSEQ_3:25
.= f . (s,J) by A10 ;
A80: r . (len r) = f . ((g . ((B + 1) - 1)),J) by A75, A78, FINSEQ_3:25
.= f . ((g . B),J) ;
reconsider R = ((g . B) . (the_array_sort_of S)) . M as ascending permutation of D by A74;
A81: ((f . ((g . B),J)) . (the_array_sort_of S)) . M = R by A6;
A82: f . ((g . B),J) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
inversions R = {} by EXCHSORT:48;
then ((f . ((g . B),J)) . the bool-sort of S) . b <> TRUE by A6;
then ((f . ((g . B),J)) . the bool-sort of S) . b = FALSE by XBOOLEAN:def 3
.= \false C by Th10 ;
then A83: r . (len r) nin (\false C) -States ( the generators of G,b) by A80, A82, AOFA_A00:def 20;
for i being Nat st 1 <= i & i < len r holds
( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) )

proof

let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) ) )
assume A84: 1 <= i ; :: thesis: ( not i < len r or ( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) ) )
assume A85: i < len r ; :: thesis: ( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) )
consider j being Nat such that
A86: i = 1 + j by A84, NAT_1:10;
A87: r . i = H₃(i) by A75, A84, A85, FINSEQ_3:25
.= f . ((g . j),J) by A86 ;
In (j,NAT) = j ;
then h . j = ((g . j) . (the_array_sort_of S)) . M by A13;
then reconsider R = ((g . j) . (the_array_sort_of S)) . M as permutation of D by A67;
A88: f . ((g . j),J) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
i <= B by A75, A85, NAT_1:13;
then not R is ascending by A74, A86, NAT_1:13;
then inversions R <> {} by EXCHSORT:48;
then ( ((f . ((g . j),J)) . the bool-sort of S) . b <> FALSE & FALSE = \false C ) by A6, Th10;
hence r . i in (\false C) -States ( the generators of G,b) by A87, A88, AOFA_A00:def 20; :: thesis: r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J))
( 1 <= i + 1 & i + 1 <= len r ) by A85, NAT_1:11, NAT_1:13;
hence r . (i + 1) = H₃(i + 1) by A75, FINSEQ_3:25
.= f . ((f . ((g . j),(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))),J) by A10, A86
.= f . ((f . ((f . ((g . j),((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((f . ((g . j),(J \; (y := (((@ M) . (@ i1)),A))))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((f . ((f . ((g . j),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((f . ((g . j),J)),((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((g . j),J)),(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))),J) by AOFA_000:def 29
.= f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) by A87, AOFA_000:def 29 ;
:: thesis: verum

end;

hence ((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 by A80, A81, A79, A83, AOFA_000:86; :: thesis: verum

end;

end;

end;

assume A89: J is absolutely-terminating ; :: thesis: 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 <> {} }
let s be Element of C -States the generators of G; :: according to AOFA_000:def 38 :: thesis: ( not s in { s1 where s1 is Element of C -States the generators of G : (s1 . (the_array_sort_of S)) . M <> {} } or [s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))))] in TerminatingPrograms (A,(C -States the generators of G),((\false C) -States ( the generators of G,b)),f) )
assume s in { s1 where s1 is Element of C -States the generators of G : (s1 . (the_array_sort_of S)) . M <> {} } ; :: thesis: [s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))))] in TerminatingPrograms (A,(C -States the generators of G),((\false C) -States ( the generators of G,b)),f)
then consider s1 being Element of C -States the generators of G such that
A90: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
A91: the carrier of (#INT,<=#) = INT by LFUZZY_0:def 3;
reconsider D = (s . (the_array_sort_of S)) . M as non empty finite 0 -based array of (#INT,<=#) by A91, A90;
consider g being Function of NAT,(C -States the generators of G) such that
A92: ( g . 0 = s & ( for i being Nat holds g . (i + 1) = H₁(i,g . i) ) ) from NAT_1:sch 12();
deffunc H₃( object ) -> set = ((g . (In ($1,NAT))) . (the_array_sort_of S)) . M;
A93: for x being object st x in NAT holds
H₃(x) in INT ^omega by AFINSQ_1:def 7;
consider h being Function of NAT,(INT ^omega) such that
A94: for i being object st i in NAT holds
h . i = H₃(i) from FUNCT_2:sch 2(A93);
A95: ( dom h = NAT & dom g = NAT ) by FUNCT_2:def 1;
then A96: h is non empty Sequence by ORDINAL1:def 7;
then A97: base- h = 0 by EXCHSORT:24;
then A98: h . (base- h) = ((g . (In (0,NAT))) . (the_array_sort_of S)) . M by A94
.= D by A92 ;
A99: for a being Ordinal st a in dom g holds
h . a is array of (#INT,<=#)

proof

let a be Ordinal; :: thesis: ( a in dom g implies h . a is array of (#INT,<=#) )
assume a in dom g ; :: thesis: h . a is array of (#INT,<=#)
then a in NAT by FUNCT_2:def 1;
then h . a in INT ^omega by FUNCT_2:5;
hence h . a is array of (#INT,<=#) by A91; :: thesis: verum

end;

defpred S₁[ Nat] means h . $1 <> {} ;
A100: S₁[ 0 ] by A98, A96, EXCHSORT:24;
A101: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A102: S₁[i] ; :: thesis: S₁[i + 1]
A103: I <> the_array_sort_of S by Th73;
A104: h . i = ((g . (In (i,NAT))) . (the_array_sort_of S)) . M by A94
.= ((g . i) . (the_array_sort_of S)) . M ;
reconsider R = h . i as array of (#INT,<=#) by A99, A95, ORDINAL1:def 12;
A105: h . (i + 1) = ((g . (In ((i + 1),NAT))) . (the_array_sort_of S)) . M by A94
.= ((f . ((g . i),(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))) . (the_array_sort_of S)) . M by A92
.= ((f . ((f . ((g . i),((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 29
.= ((f . ((f . ((f . ((g . i),(J \; (y := (((@ M) . (@ i1)),A))))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 29
.= ((f . ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 29 ;
(@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . I) . i1 by Th61
.= ((f . ((g . i),J)) . I) . i1 by A2, A3, A8, Th65 ;
then A106: (@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) in dom R by A6, A102, A104;
A107: (@ M) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M by Th61;
((f . ((g . i),J)) . (the_array_sort_of S)) . M = ((g . i) . (the_array_sort_of S)) . M by A6;
then A108: ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M = ((g . i) . (the_array_sort_of S)) . M by A2, A3, A103, Th65;
((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M = ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . (the_array_sort_of S)) . M by A1, A2, A3, A4, A5, Th99
.= (((@ M),(@ i1)) <- ((@ M) . (@ i2))) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))))),((@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))))) <- (((@ M) . (@ i2)) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))))) by Th80
.= (((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M) +* (((@ i1) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))))),(((@ M) . (@ i2)) value_at (C,(f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A))))))) by A106, A108, A104, A107, Th74 ;
then A109: dom (((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M) = dom (((g . i) . (the_array_sort_of S)) . M) by A108, FUNCT_7:30;
A110: (@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) = ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M by Th61;
(@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) = ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . I) . i2 by Th61
.= ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . i2 by A1, A2, A3, A4, A5, Th99
.= ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 by A2, A3, Th73, Th65
.= ((f . ((g . i),J)) . I) . i2 by A2, A3, A8, Th65 ;
then A111: (@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) in dom R by A6, A102, A104;
A112: ((f . ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))) . (the_array_sort_of S)) . M = ((f . ((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A)))) . (the_array_sort_of S)) . M by A1, A2, A3, A4, A5, Th99
.= (((@ M),(@ i2)) <- (@ y)) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))),((@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))))) <- ((@ y) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))) by Th80
.= ((@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))) +* (((@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))),((@ y) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))))) by A109, A110, A111, A104, Th74 ;
dom (((@ M) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))) +* (((@ i2) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))),((@ y) value_at (C,(f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))))))) = dom (((f . ((f . ((f . ((g . i),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))) . (the_array_sort_of S)) . M) by A110, FUNCT_7:30;
hence h . (i + 1) <> {} by A112, A105, A109, A104, A102; :: thesis: verum

end;

A113: for i being Nat holds S₁[i] from NAT_1:sch 2(A100, A101);
A114: for a being Nat
for R being array of (#INT,<=#) st R = h . a holds
for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )

proof

let a be Nat; :: thesis: for R being array of (#INT,<=#) st R = h . a holds
for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )
let R be array of (#INT,<=#); :: thesis: ( R = h . a implies for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) ) )
assume A115: R = h . a ; :: thesis: for s being Element of C -States the generators of G st g . a = s holds
ex x, y being set st
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )
let s1 be Element of C -States the generators of G; :: thesis: ( g . a = s1 implies ex x, y being set st
( x = ((f . (s1,J)) . I) . i1 & y = ((f . (s1,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) ) )
assume A116: g . a = s1 ; :: thesis: ex x, y being set st
( x = ((f . (s1,J)) . I) . i1 & y = ((f . (s1,J)) . I) . i2 & x in dom R & y in dom R & h . (a + 1) = Swap (R,x,y) )
reconsider i = a as Element of NAT by ORDINAL1:def 12;
reconsider s = g . i as Element of C -States the generators of G ;
set y1 = ((f . (s,J)) . I) . i1;
set y2 = ((f . (s,J)) . I) . i2;
take ((f . (s,J)) . I) . i1 ; :: thesis: ex y being set st
( ((f . (s,J)) . I) . i1 = ((f . (s1,J)) . I) . i1 & y = ((f . (s1,J)) . I) . i2 & ((f . (s,J)) . I) . i1 in dom R & y in dom R & h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),y) )
take ((f . (s,J)) . I) . i2 ; :: thesis: ( ((f . (s,J)) . I) . i1 = ((f . (s1,J)) . I) . i1 & ((f . (s,J)) . I) . i2 = ((f . (s1,J)) . I) . i2 & ((f . (s,J)) . I) . i1 in dom R & ((f . (s,J)) . I) . i2 in dom R & h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
thus ( ((f . (s,J)) . I) . i1 = ((f . (s1,J)) . I) . i1 & ((f . (s,J)) . I) . i2 = ((f . (s1,J)) . I) . i2 ) by A116; :: thesis: ( ((f . (s,J)) . I) . i1 in dom R & ((f . (s,J)) . I) . i2 in dom R & h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
In (i,NAT) = i ;
then A117: h . i = ((g . i) . (the_array_sort_of S)) . M by A94;
R <> {} by A115, A113;
hence A118: ( ((f . (s,J)) . I) . i1 in dom R & ((f . (s,J)) . I) . i2 in dom R ) by A117, A6, A115; :: thesis: h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2))
A119: ( succ (Segm i) = Segm (i + 1) & In ((i + 1),NAT) = i + 1 ) by NAT_1:38;
then A120: h . (succ a) = ((g . (i + 1)) . (the_array_sort_of S)) . M by A94;
A121: g . (i + 1) = f . (s,(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))) by A92
.= f . ((f . (s,((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A))) by AOFA_000:def 29
.= f . ((f . ((f . (s,(J \; (y := (((@ M) . (@ i1)),A))))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A))) by AOFA_000:def 29
.= f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A))) by AOFA_000:def 29
.= f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A))) by A1, A2, A3, A4, A5, Th99
.= f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A))) by A1, A2, A3, A4, A5, Th99 ;
set s1 = f . (s,J);
set s2 = f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)));
set s3 = f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)));
set s4 = f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A)));
A122: (@ i1) value_at (C,(f . (s,J))) = ((f . (s,J)) . I) . i1 by Th61;
A123: ((f . (s,J)) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A6;
A124: (@ M) value_at (C,(f . (s,J))) = ((f . (s,J)) . (the_array_sort_of S)) . M by Th61
.= (s . (the_array_sort_of S)) . M by A6 ;
A125: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . y = ((@ M) . (@ i1)) value_at (C,(f . (s,J))) by A2, A3, Th65
.= ((@ M) value_at (C,(f . (s,J)))) . ((@ i1) value_at (C,(f . (s,J)))) by Th79
.= R . (((f . (s,J)) . I) . i1) by A115, A118, A122, A117, A124, Th74 ;
A126: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i1 = ((f . (s,J)) . I) . i1 by A2, A3, A8, Th65;
A127: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 = ((f . (s,J)) . I) . i2 by A2, A3, A8, Th65;
A128: ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M = ((f . (s,J)) . (the_array_sort_of S)) . M by A2, A3, A9, Th65;
A129: ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . y = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . y by A2, A3, Th73, Th65;
A130: ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . i2 = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 by A2, A3, Th73, Th65;
A131: (@ M) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . (the_array_sort_of S)) . M by Th61;
A132: (@ i1) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i1 by Th61;
A133: (@ i2) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))) . I) . i2 by Th61;
A134: ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . (the_array_sort_of S)) . M = (((@ M),(@ i1)) <- ((@ M) . (@ i2))) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))),((@ i1) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))))) <- (((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))) by Th80
.= R +* (((@ i1) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))),(((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))))) by A115, A131, A132, A123, A128, A126, A118, A117, Th74 ;
A135: (@ M) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) = ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . (the_array_sort_of S)) . M by Th61;
A136: (@ i2) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) = ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . i2 by Th61;
A137: (@ y) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) = ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))) . I) . y by Th61;
A138: dom R = dom (R +* ((((f . (s,J)) . I) . i1),(((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))))) by FUNCT_7:30;
A139: ((f . ((f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))),(M := ((((@ M),(@ i2)) <- (@ y)),A)))) . (the_array_sort_of S)) . M = (((@ M),(@ i2)) <- (@ y)) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))) by A2, A3, Th65
.= (((@ M) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))))),((@ i2) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))))) <- ((@ y) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A)))))) by Th80
.= (R +* ((((f . (s,J)) . I) . i1),(((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))))) +* ((((f . (s,J)) . I) . i2),((@ y) value_at (C,(f . ((f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))),(M := ((((@ M),(@ i1)) <- ((@ M) . (@ i2))),A))))))) by A135, A136, A138, A132, A118, A134, A126, A130, A127, Th74 ;
((@ M) . (@ i2)) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A))))) = ((@ M) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))) . ((@ i2) value_at (C,(f . ((f . (s,J)),(y := (((@ M) . (@ i1)),A)))))) by Th79
.= R . (((f . (s,J)) . I) . i2) by A115, A118, A131, A133, A127, A128, A123, A117, Th74 ;
hence h . (a + 1) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) by A119, A120, A121, A118, A137, A139, A129, A125, FUNCT_7:def 12; :: thesis: verum

end;

defpred S₂[ Nat] means h . $1 is permutation of D;
A140: S₂[ 0 ] by A98, A97, EXCHSORT:38;

A141: now :: thesis: for i being Nat st S₂[i] holds
S₂[i + 1]

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A142: S₂[i] ; :: thesis: S₂[i + 1]
thus S₂[i + 1] :: thesis: verum

proof

reconsider R = h . i as array of (#INT,<=#) by A99, A95, ORDINAL1:def 12;
reconsider s = g . i as Element of C -States the generators of G ;
consider x, y being set such that
( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 ) and
A143: ( x in dom R & y in dom R & h . (i + 1) = Swap (R,x,y) ) by A114;
thus h . (i + 1) is permutation of D by A142, A143, EXCHSORT:44; :: thesis: verum

end;

end;

A144: for i being Nat holds S₂[i] from NAT_1:sch 2(A140, A141);
defpred S₃[ Nat] means ((g . $1) . (the_array_sort_of S)) . M is ascending permutation of D;
A145: ex i being Nat st S₃[i]

proof

assume A146: for i being Nat holds not S₃[i] ; :: thesis: contradiction
for a being Ordinal st a in dom h & succ a in dom h holds
ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) )

proof

let a be Ordinal; :: thesis: ( a in dom h & succ a in dom h implies ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) ) )
assume A147: a in dom h ; :: thesis: ( not succ a in dom h or ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) ) )
assume succ a in dom h ; :: thesis: ex R being array of (#INT,<=#) ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) )
reconsider i = a as Element of NAT by A147, FUNCT_2:def 1;
reconsider R = h . i as array of (#INT,<=#) by A91;
reconsider s = g . i as Element of C -States the generators of G ;
set y1 = ((f . (s,J)) . I) . i1;
set y2 = ((f . (s,J)) . I) . i2;
take R ; :: thesis: ex x, y being set st
( [x,y] in inversions R & h . a = R & h . (succ a) = Swap (R,x,y) )
take ((f . (s,J)) . I) . i1 ; :: thesis: ex y being set st
( [(((f . (s,J)) . I) . i1),y] in inversions R & h . a = R & h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),y) )
take ((f . (s,J)) . I) . i2 ; :: thesis: ( [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions R & h . a = R & h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
In (i,NAT) = i ;
then A148: ( S₂[i] & not S₃[i] & h . i = ((g . i) . (the_array_sort_of S)) . M ) by A144, A146, A94;
then inversions R <> {} by EXCHSORT:48;
hence [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions R by A148, A6; :: thesis: ( h . a = R & h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) )
thus h . a = R ; :: thesis: h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2))
consider x, y being set such that
A149: ( x = ((f . (s,J)) . I) . i1 & y = ((f . (s,J)) . I) . i2 & x in dom R & y in dom R & h . (i + 1) = Swap (R,x,y) ) by A114;
succ (Segm i) = Segm (i + 1) by NAT_1:38;
hence h . (succ a) = Swap (R,(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)) by A149; :: thesis: verum

end;

then h is 0 -based arr_computation of D by A96, A95, A98, A99, EXCHSORT:def 14;
then h is finite by EXCHSORT:76;
hence contradiction by A95; :: thesis: verum

end;

consider B being Nat such that
A150: ( S₃[B] & ( for i being Nat st S₃[i] holds
B <= i ) ) from NAT_1:sch 5(A145);
reconsider h = h as Sequence of INT ^omega by A95, ORDINAL1:def 7;
reconsider c = h | (succ B) as array of INT ^omega ;
set TV = (\false C) -States ( the generators of G,b);
deffunc H₄( Nat) -> set = f . ((g . ($1 - 1)),J);
consider r being FinSequence such that
A151: ( len r = B + 1 & ( for i being Nat st i in dom r holds
r . i = H₄(i) ) ) from FINSEQ_1:sch 2();
rng r c= C -States the generators of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng r or x in C -States the generators of G )
assume x in rng r ; :: thesis: x in C -States the generators of G
then consider y being object such that
A152: ( y in dom r & x = r . y ) by FUNCT_1:def 3;
reconsider y = y as Nat by A152;
consider i being Nat such that
A153: y = 1 + i by A152, FINSEQ_3:25, NAT_1:10;
x = H₄(y) by A151, A152
.= f . ((g . i),J) by A153 ;
hence x in C -States the generators of G ; :: thesis: verum

end;

then reconsider r = r as non empty FinSequence of C -States the generators of G by A151, FINSEQ_1:def 4;
A154: 1 <= B + 1 by NAT_1:11;
A155: r . 1 = f . ((g . (1 - 1)),J) by A151, A154, FINSEQ_3:25
.= f . (s,J) by A92 ;
A156: r . (len r) = f . ((g . ((B + 1) - 1)),J) by A151, A154, FINSEQ_3:25
.= f . ((g . B),J) ;
reconsider R = ((g . B) . (the_array_sort_of S)) . M as ascending permutation of D by A150;
A157: f . ((g . B),J) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
inversions R = {} by EXCHSORT:48;
then ((f . ((g . B),J)) . the bool-sort of S) . b <> TRUE by A6;
then ((f . ((g . B),J)) . the bool-sort of S) . b = FALSE by XBOOLEAN:def 3
.= \false C by Th10 ;
then A158: r . (len r) nin (\false C) -States ( the generators of G,b) by A156, A157, AOFA_A00:def 20;
for i being Nat st 1 <= i & i < len r holds
( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) )

proof

let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) ) )
assume A159: 1 <= i ; :: thesis: ( not i < len r or ( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) ) )
assume A160: i < len r ; :: thesis: ( r . i in (\false C) -States ( the generators of G,b) & r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) )
consider j being Nat such that
A161: i = 1 + j by A159, NAT_1:10;
A162: r . i = H₄(i) by A151, A159, A160, FINSEQ_3:25
.= f . ((g . j),J) by A161 ;
In (j,NAT) = j ;
then h . j = ((g . j) . (the_array_sort_of S)) . M by A94;
then reconsider R = ((g . j) . (the_array_sort_of S)) . M as permutation of D by A144;
A163: f . ((g . j),J) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
i <= B by A151, A160, NAT_1:13;
then not R is ascending by A150, A161, NAT_1:13;
then inversions R <> {} by EXCHSORT:48;
then ( ((f . ((g . j),J)) . the bool-sort of S) . b <> FALSE & FALSE = \false C ) by A6, Th10;
hence r . i in (\false C) -States ( the generators of G,b) by A162, A163, AOFA_A00:def 20; :: thesis: r . (i + 1) = f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J))
( 1 <= i + 1 & i + 1 <= len r ) by A160, NAT_1:11, NAT_1:13;
hence r . (i + 1) = H₄(i + 1) by A151, FINSEQ_3:25
.= f . ((f . ((g . j),(((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))),J) by A92, A161
.= f . ((f . ((f . ((g . j),((J \; (y := (((@ M) . (@ i1)),A))) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((f . ((g . j),(J \; (y := (((@ M) . (@ i1)),A))))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((f . ((f . ((g . j),J)),(y := (((@ M) . (@ i1)),A)))),(((@ M) . (@ i1)) := (((@ M) . (@ i2)),A)))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((f . ((g . j),J)),((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))))),(((@ M) . (@ i2)) := ((@ y),A)))),J) by AOFA_000:def 29
.= f . ((f . ((f . ((g . j),J)),(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))),J) by AOFA_000:def 29
.= f . ((r . i),((((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))) \; J)) by A162, AOFA_000:def 29 ;
:: thesis: verum

end;

hence [s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))))] in TerminatingPrograms (A,(C -States the generators of G),((\false C) -States ( the generators of G,b)),f) by A89, A155, A158, AOFA_000:def 33, AOFA_000:101; :: thesis: verum