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 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
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 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
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 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
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 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
let G be basic GeneratorSystem over S,X,T; :: thesis: 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
let A be IfWhileAlgebra of the generators of G; :: thesis: 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
let I be integer SortSymbol of S; :: thesis: 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
let m, i 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 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
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 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
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 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
let s be Element of C -States 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 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
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m & (s . (the_array_sort_of S)) . M <> {} implies 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 )
assume that
A1: ( f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m ) and
A2: (s . (the_array_sort_of S)) . M <> {} ; :: thesis: 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
let n be Nat; :: thesis: ( ((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 implies 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 )
assume A3: ((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 ; :: thesis: 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
let X be non empty finite integer-membered set ; :: thesis: ( X = rng ((s . (the_array_sort_of S)) . M) implies (M . (n,I)) value_at (C,s) = max X )
assume A4: X = rng ((s . (the_array_sort_of S)) . M) ; :: thesis: (M . (n,I)) value_at (C,s) = max X
set ST = C -States the generators of G;
set TV = (\false C) -States ( the generators of G,b);
defpred S₁[ Element of C -States the generators of G] means (s . (the_array_sort_of S)) . M = ($1 . (the_array_sort_of S)) . M;
reconsider sm = s as ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
reconsider z = (sm . (the_array_sort_of S)) . M as finite 0 -based array of INT ;
defpred S₂[ Element of C -States the generators of G] means ( S₁[$1] & ($1 . I) . i in NAT & ($1 . I) . m in NAT & ($1 . I) . i <= len z & ($1 . I) . m < ($1 . I) . i & ($1 . I) . m < len z & ( for mx being Integer st mx = ($1 . I) . m holds
for j being Nat st j < ($1 . I) . i holds
z . j <= z . mx ) );
defpred S₃[ Element of C -States the generators of G] means ( S₁[$1] & ($1 . I) . i < (length ((@ M),I)) value_at (C,s) );
set s0 = s;
set s1 = f . (s,(m := ((\0 (T,I)),A)));
set s2 = f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)));
set W = b gt ((length ((@ M),I)),(@ i),A);
set K = i := (((@ i) + (\1 (T,I))),A);
set s3 = f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A)));
set CJ = b gt (((@ M) . (@ i)),((@ M) . (@ m)),A);
set IJ = m := ((@ i),A);
set J = if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)));
set a = the_array_sort_of S;
A5: I <> the bool-sort of S by AOFA_A00:53;
A6: f complies_with_if_wrt (\false C) -States ( the generators of G,b) by AOFA_000:def 32;
A7: ((f . (s,(m := ((\0 (T,I)),A)))) . I) . m = (\0 (T,I)) value_at (C,s) by A1, Th65;
A8: (\0 (T,I)) value_at (C,s) = 0 by Th36;
A9: ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m = ((f . (s,(m := ((\0 (T,I)),A)))) . I) . m by A1, Th65;
A10: ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i = (\1 (T,I)) value_at (C,(f . (s,(m := ((\0 (T,I)),A))))) by A1, Th65
.= 1 by Th37 ;
A11: ((f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i by A1, A5, Th65;
consider J1, K1, L1 being Element of S such that
A12: ( L1 = 1 & K1 = 1 & J1 <> L1 & J1 <> K1 & the connectives of S . 11 is_of_type <*J1,K1*>,L1 & the connectives of S . (11 + 1) is_of_type <*J1,K1,L1*>,J1 & the connectives of S . (11 + 2) is_of_type <*J1*>,K1 & the connectives of S . (11 + 3) is_of_type <*K1,L1*>,J1 ) by AOFA_A00:def 51;
A13: ( the Sorts of C . (the_array_sort_of S) = INT ^omega & the Sorts of C . the bool-sort of S = BOOLEAN ) by Th74, AOFA_A00:def 32;
A14: the bool-sort of S <> I by AOFA_A00:53;
A15: the_array_sort_of S <> I by A12, Th71;
then A16: ((f . (s,(m := ((\0 (T,I)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, Th65;
A17: ((f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . (the_array_sort_of S)) . M by A13, A1, Th65;
A18: S₂[f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))]

proof

thus S₁[f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))] by A15, A1, Th65, A16; :: thesis: ( ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i in NAT & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m in NAT & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i <= len z & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m < len z & ( for mx being Integer st mx = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m holds
for j being Nat st j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i holds
z . j <= z . mx ) )
thus ( ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i in NAT & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m in NAT ) by A7, A8, A9, A10; :: thesis: ( ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i <= len z & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m < len z & ( for mx being Integer st mx = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m holds
for j being Nat st j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i holds
z . j <= z . mx ) )
( 0 < len z & 0 + 1 = 1 ) by A2, NAT_1:3;
hence ( ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i <= len z & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i & ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m < len z ) by A7, A8, A9, A10, NAT_1:13; :: thesis: for mx being Integer st mx = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m holds
for j being Nat st j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i holds
z . j <= z . mx
let mx be Integer; :: thesis: ( mx = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m implies for j being Nat st j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i holds
z . j <= z . mx )
assume A19: mx = ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . m ; :: thesis: for j being Nat st j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i holds
z . j <= z . mx
let j be Nat; :: thesis: ( j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i implies z . j <= z . mx )
assume A20: j < ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . I) . i ; :: thesis: z . j <= z . mx
1 = 0 + 1 ;
then ( j <= 0 & j >= 0 ) by A20, A10, NAT_1:13;
then A21: j = 0 ;
thus z . j <= z . mx by A21, A19, A8, A9, A1, Th65; :: thesis: verum

end;

deffunc H₁( Element of C -States the generators of G) -> Element of NAT = In (((len ((s . (the_array_sort_of S)) . M)) - (($1 . I) . i)),NAT);
A22: ( f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) iff S₃[f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A)))] )

proof

A23: ( (@ i) value_at (C,(f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A))))) < (length ((@ M),I)) value_at (C,(f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A))))) iff f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) by A1, Th66;
(length ((@ M),I)) value_at (C,(f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A))))) = length (((@ M) value_at (C,(f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))))),I) by Th81
.= len ((@ M) value_at (C,(f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))))) by Th74
.= len (((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))) . (the_array_sort_of S)) . M) by Th61
.= len ((s . (the_array_sort_of S)) . M) by A15, A1, Th65, A16
.= len ((@ M) value_at (C,s)) by Th61
.= length (((@ M) value_at (C,s)),I) by Th74
.= (length ((@ M),I)) value_at (C,s) by Th81 ;
hence ( f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) iff S₃[f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A)))] ) by A15, A1, Th65, A16, A17, A11, A23, Th61; :: thesis: verum

end;

A24: len ((@ M) value_at (C,s)) = length (((@ M) value_at (C,s)),I) by Th74
.= (length ((@ M),I)) value_at (C,s) by Th81 ;
A25: for s being Element of C -States the generators of G st S₃[s] holds
( ( S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] implies f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] ) & H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s) )

proof

let s be Element of C -States the generators of G; :: thesis: ( S₃[s] implies ( ( S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] implies f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] ) & H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s) ) )
assume A26: S₃[s] ; :: thesis: ( ( S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] implies f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] ) & H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s) )
A27: ( f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) = f . ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))),(b gt ((length ((@ M),I)),(@ i),A))) & f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))) = f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A))) ) by AOFA_000:def 29;

hereby :: thesis: H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s)

A28: ((f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) . I) . i = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i by A14, A27, A1, Th65;
A29: (s . (the_array_sort_of S)) . M = ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M by A13, A1, Th65;
A30: (s . I) . i = ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . i by A14, A1, Th65;

A31: now :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i )

per cases ( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) or f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ) ;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) ; :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i )

then f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(m := ((@ i),A))) by A6;
hence ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i ) by A15, A1, A29, A30, Th65; :: thesis: verum

end;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ; :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i )

then f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(EmptyIns A)) by A6;
hence ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i ) by A29, A30, AOFA_000:def 28; :: thesis: verum

end;

end;

end;

A32: ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A31, A27, A15, A1, Th65;
(length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = length (((@ M) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))))),I) by Th81
.= len ((@ M) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))))) by Th74
.= len (((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . (the_array_sort_of S)) . M) by Th61
.= len ((@ M) value_at (C,s)) by A32, A26, Th61 ;
then ( S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] iff (@ i) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) < (length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) ) by A26, A28, A24, A32, A27, A13, A1, Th65, Th61;
hence ( S₃[f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))] iff f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) in (\false C) -States ( the generators of G,b) ) by A1, A27, Th66; :: thesis: verum

end;

reconsider sJ = f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) as ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
reconsider a = (sJ . I) . i as Element of C,I ;
A33: ( (@ i) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))) = ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i & (\1 (T,I)) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))) = 1 ) by Th37, Th61;
f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)))) = f . ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))),(b gt ((length ((@ M),I)),(@ i),A))) by AOFA_000:def 29
.= f . ((f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A)))),(b gt ((length ((@ M),I)),(@ i),A))) by AOFA_000:def 29 ;
then A34: ((f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) . I) . i = ((f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A)))) . I) . i by A1, Th65, A14
.= ((@ i) + (\1 (T,I))) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))) by A1, Th65
.= ((@ i) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))))) + ((\1 (T,I)) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))))) by Th39
.= (((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i) + 1 by A33, AOFA_A00:55 ;
( (@ M) value_at (C,s) = (s . (the_array_sort_of S)) . M & (s . I) . i < (length ((@ M),I)) value_at (C,s) & (length ((@ M),I)) value_at (C,s) = length (((@ M) value_at (C,s)),I) ) by A26, Th61, Th81;
then A35: (s . I) . i < len ((s . (the_array_sort_of S)) . M) by Th74;
then A36: (len ((s . (the_array_sort_of S)) . M)) - ((s . I) . i) > 0 by XREAL_1:50;
(len ((s . (the_array_sort_of S)) . M)) - ((s . I) . i) >= 0 + 1 by A35, XREAL_1:50, INT_1:7;
then A37: ((len ((s . (the_array_sort_of S)) . M)) - ((s . I) . i)) - 1 >= 1 - 1 by XREAL_1:9;

per cases ( ((@ M) . (@ i)) value_at (C,s) > ((@ M) . (@ m)) value_at (C,s) or ((@ M) . (@ i)) value_at (C,s) <= ((@ M) . (@ m)) value_at (C,s) ) ;

suppose ((@ M) . (@ i)) value_at (C,s) > ((@ M) . (@ m)) value_at (C,s) ; :: thesis: H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s)

then ( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) & f complies_with_if_wrt (\false C) -States ( the generators of G,b) ) by A1, Th66, AOFA_000:def 32;
then A38: ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = ((f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(m := ((@ i),A)))) . I) . i
.= ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . i by A1, Th65
.= (s . I) . i by A14, A1, Th65 ;
H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) = ((len ((s . (the_array_sort_of S)) . M)) - ((s . I) . i)) - 1 by A34, A38, A37, INT_1:3, SUBSET_1:def 8;
then H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) = H₁(s) - 1 by A36, INT_1:3, SUBSET_1:def 8;
hence H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s) by XREAL_1:44; :: thesis: verum

end;

suppose ((@ M) . (@ i)) value_at (C,s) <= ((@ M) . (@ m)) value_at (C,s) ; :: thesis: H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s)

then ( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) & f complies_with_if_wrt (\false C) -States ( the generators of G,b) ) by A1, Th66, AOFA_000:def 32;
then f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(EmptyIns A))
.= f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) by AOFA_000:def 28 ;
then ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i by A1, Th65, A14;
then H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) = ((len ((s . (the_array_sort_of S)) . M)) - ((s . I) . i)) - 1 by A34, A37, INT_1:3, SUBSET_1:def 8
.= H₁(s) - 1 by A36, INT_1:3, SUBSET_1:def 8 ;
hence H₁(f . (s,(((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A))))) < H₁(s) by XREAL_1:44; :: thesis: verum

end;

end;

end;

A39: f iteration_terminates_for ((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt ((length ((@ M),I)),(@ i),A)),f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(b gt ((length ((@ M),I)),(@ i),A))) from AOFA_000:sch 3(A22, A25);
A40: for s being Element of C -States the generators of G st S₂[s] & s in (\false C) -States ( the generators of G,b) & S₃[s] holds
S₂[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))]

proof

let s be Element of C -States the generators of G; :: thesis: ( S₂[s] & s in (\false C) -States ( the generators of G,b) & S₃[s] implies S₂[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))] )
assume A41: S₂[s] ; :: thesis: ( not s in (\false C) -States ( the generators of G,b) or not S₃[s] or S₂[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))] )
assume s in (\false C) -States ( the generators of G,b) ; :: thesis: ( not S₃[s] or S₂[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))] )
assume A42: S₃[s] ; :: thesis: S₂[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))]
A43: (s . (the_array_sort_of S)) . M = ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M by A13, A1, Th65;
thus S₁[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))] :: thesis: ( ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i in NAT & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m in NAT & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i <= len z & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m holds
for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx ) )

proof

per cases ( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) or f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ) ;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) ; :: thesis: S₁[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))]

then f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(m := ((@ i),A))) by A6;
then A44: ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A41, A15, A1, A43, Th65;
f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))) = f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A))) by AOFA_000:def 29;
hence S₁[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))] by A44, A15, A1, Th65; :: thesis: verum

end;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ; :: thesis: S₁[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))]

then f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(EmptyIns A)) by A6;
then A45: ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A41, A43, AOFA_000:def 28;
f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))) = f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A))) by AOFA_000:def 29;
hence S₁[f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))] by A45, A15, A1, Th65; :: thesis: verum

end;

end;

end;

A46: ( (@ i) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))) = ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i & (@ i) value_at (C,s) = (s . I) . i & (@ m) value_at (C,s) = (s . I) . m & (\1 (T,I)) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))) = 1 ) by Th61, Th37;
A47: f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))) = f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A))) by AOFA_000:def 29;
then A48: ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i = ((@ i) + (\1 (T,I))) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))) by A1, Th65
.= ((@ i) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))))) + ((\1 (T,I)) value_at (C,(f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))))) by Th39
.= (((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i) + 1 by A46, AOFA_A00:55 ;
A49: ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m = ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m by A47, A1, Th65;
A50: ( ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . i = (s . I) . i & ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . m = (s . I) . m & ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M ) by A13, A14, A1, Th65;
A51: ( (s . I) . i is Nat & (@ M) value_at (C,s) = (s . (the_array_sort_of S)) . M & (@ M) value_at (C,s) = (s . (the_array_sort_of S)) . M ) by A41, Th61;
then A52: (@ i) value_at (C,s) in dom ((@ M) value_at (C,s)) by A46, A24, A42, AFINSQ_1:86;
A53: (@ m) value_at (C,s) in dom ((@ M) value_at (C,s)) by A51, A46, A41, AFINSQ_1:86;
A54: z . ((s . I) . i) = ((@ M) value_at (C,s)) . ((s . I) . i) by A41, Th61
.= ((@ M) value_at (C,s)) . ((@ i) value_at (C,s)) by Th61
.= ((@ M) value_at (C,s)) . ((@ i) value_at (C,s)) by A52, Th74
.= ((@ M) . (@ i)) value_at (C,s) by Th79 ;
A55: z . ((s . I) . m) = ((@ M) value_at (C,s)) . ((s . I) . m) by A41, Th61
.= ((@ M) value_at (C,s)) . ((@ m) value_at (C,s)) by Th61
.= ((@ M) value_at (C,s)) . ((@ m) value_at (C,s)) by A53, Th74
.= ((@ M) . (@ m)) value_at (C,s) by Th79 ;

A56: now :: thesis: ( ( z . ((s . I) . i) > z . ((s . I) . m) & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M ) or ( z . ((s . I) . i) <= z . ((s . I) . m) & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . m & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M ) )

per cases ( z . ((s . I) . i) > z . ((s . I) . m) or z . ((s . I) . i) <= z . ((s . I) . m) ) ;

case z . ((s . I) . i) > z . ((s . I) . m) ; :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M )

then f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) by A1, A54, A55, Th66;
then A57: f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(m := ((@ i),A))) by A6;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i by A50, A1, Th65; :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M )
thus ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (@ i) value_at (C,(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))))) by A57, A1, Th65
.= (s . I) . i by A50, Th61 ; :: thesis: ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
thus ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A57, A50, A1, A15, Th65; :: thesis: verum

end;

case z . ((s . I) . i) <= z . ((s . I) . m) ; :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . m & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M )

then f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) by A1, A54, A55, Th66;
then A58: f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) = f . ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),(EmptyIns A)) by A6;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i by A50, AOFA_000:def 28; :: thesis: ( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . m & ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M )
thus ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . m = (s . I) . m by A58, A50, AOFA_000:def 28; :: thesis: ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
thus ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A58, A50, AOFA_000:def 28; :: thesis: verum

end;

end;

end;

reconsider sIi = (s . I) . i as Element of NAT by A41;
A59: ( ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i = sIi + 1 & sIi + 1 in NAT ) by A48, A56, ORDINAL1:def 12;
thus ( ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i in NAT & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m in NAT ) by A56, A41, A47, A1, Th65, A48, ORDINAL1:def 12; :: thesis: ( ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i <= len z & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m holds
for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx ) )
len z = (length ((@ M),I)) value_at (C,s) by A24, Th61;
hence ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i <= len z by A56, A48, A42, INT_1:7; :: thesis: ( ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i & ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m holds
for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx ) )
thus ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i by A56, A48, A49, A41, NAT_1:13; :: thesis: ( ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m holds
for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx ) )
thus ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m < len z by A24, Th61, A56, A49, A41, A42; :: thesis: for mx being Integer st mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m holds
for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx
let mx be Integer; :: thesis: ( mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m implies for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx )
assume A60: mx = ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . m ; :: thesis: for j being Nat st j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i holds
z . j <= z . mx
let j be Nat; :: thesis: ( j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i implies z . j <= z . mx )
assume A61: j < ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i ; :: thesis: z . j <= z . mx

per cases ( ( j < (s . I) . i & z . ((s . I) . i) <= z . ((s . I) . m) ) or ( j < (s . I) . i & z . ((s . I) . i) > z . ((s . I) . m) ) or ( j = (s . I) . i & z . ((s . I) . i) <= z . ((s . I) . m) ) or ( j = (s . I) . i & z . ((s . I) . i) > z . ((s . I) . m) ) ) by A61, A59, NAT_1:22;

suppose ( j < (s . I) . i & z . ((s . I) . i) <= z . ((s . I) . m) ) ; :: thesis: z . j <= z . mx

hence z . j <= z . mx by A60, A41, A56, A49; :: thesis: verum

end;

suppose ( j < (s . I) . i & z . ((s . I) . i) > z . ((s . I) . m) ) ; :: thesis: z . j <= z . mx

then z . j <= z . ((s . I) . m) by A41;
hence z . j <= z . mx by A60, A56, A49, XXREAL_0:2; :: thesis: verum

end;

suppose ( j = (s . I) . i & z . ((s . I) . i) <= z . ((s . I) . m) ) ; :: thesis: z . j <= z . mx

hence z . j <= z . mx by A60, A56, A47, A1, Th65; :: thesis: verum

end;

suppose ( j = (s . I) . i & z . ((s . I) . i) > z . ((s . I) . m) ) ; :: thesis: z . j <= z . mx

hence z . j <= z . mx by A60, A56, A47, A1, Th65; :: thesis: verum

end;

end;

end;

A62: for s being Element of C -States the generators of G st S₂[s] holds
( S₂[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )

proof

let s be Element of C -States the generators of G; :: thesis: ( S₂[s] implies ( S₂[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) ) )
assume A63: S₂[s] ; :: thesis: ( S₂[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )
thus S₁[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] by A63, A1, A13, Th65; :: thesis: ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i in NAT & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m in NAT & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i <= len z & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m holds
for j being Nat st j < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i holds
z . j <= z . mx ) & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )
A64: ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m = (s . I) . m ) by A1, A14, Th65;
thus ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i in NAT & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m in NAT ) by A63, A1, A14, Th65; :: thesis: ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i <= len z & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m holds
for j being Nat st j < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i holds
z . j <= z . mx ) & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )
thus ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i <= len z & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i ) by A64, A63; :: thesis: ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < len z & ( for mx being Integer st mx = ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m holds
for j being Nat st j < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i holds
z . j <= z . mx ) & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )
thus ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m < len z by A1, A14, Th65, A63; :: thesis: ( ( for mx being Integer st mx = ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m holds
for j being Nat st j < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i holds
z . j <= z . mx ) & ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )
thus for mx being Integer st mx = ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . m holds
for j being Nat st j < ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i holds
z . j <= z . mx by A64, A63; :: thesis: ( ( f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) implies S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ) & ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ) )
A65: (length ((@ M),I)) value_at (C,s) = length (((@ M) value_at (C,s)),I) by Th81
.= len ((@ M) value_at (C,s)) by Th74
.= len ((s . (the_array_sort_of S)) . M) by Th61
.= len ((@ M) value_at (C,s)) by A63, Th61 ;

hereby :: thesis: ( S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] implies f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) )

assume f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) ; :: thesis: S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))]
then ( (@ i) value_at (C,s) < (length ((@ M),I)) value_at (C,s) & (s . I) . i = (@ i) value_at (C,s) ) by A1, Th66, Th61;
hence S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] by A63, A1, A14, Th65, A13, A24, A65; :: thesis: verum

end;

assume S₃[f . (s,(b gt ((length ((@ M),I)),(@ i),A)))] ; :: thesis: f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b)
then (@ i) value_at (C,s) < (length ((@ M),I)) value_at (C,s) by A64, A24, A65, Th61;
hence f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in (\false C) -States ( the generators of G,b) by A1, Th66; :: thesis: verum

end;

A66: ( S₂[f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(while ((b gt ((length ((@ M),I)),(@ i),A)),((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))))] & not S₃[f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(while ((b gt ((length ((@ M),I)),(@ i),A)),((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))))] ) from AOFA_000:sch 5(A18, A39, A40, A62);
A67: 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)))))))) = f . ((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))))))) by AOFA_000:def 29
.= f . ((f . ((f . (s,(m := ((\0 (T,I)),A)))),(i := ((\1 (T,I)),A)))),(while ((b gt ((length ((@ M),I)),(@ i),A)),((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) by AOFA_000:def 29 ;
then A68: n in dom z by A66, A3, AFINSQ_1:86;
A69: (^ (n,T,I)) value_at (C,s) = n by Th90;
A70: z = (@ M) value_at (C,s) by Th61;
A71: z . (((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) = ((@ M) value_at (C,s)) . ((^ (n,T,I)) value_at (C,s)) by A68, A70, A69, Th74, A3
.= ((@ M) . (^ (n,T,I))) value_at (C,s) by Th79 ;
A72: (M . (n,I)) value_at (C,s) is UpperBound of X

proof

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not x in X or x <= (M . (n,I)) value_at (C,s) )
assume x in X ; :: thesis: x <= (M . (n,I)) value_at (C,s)
then consider j being object such that
A73: ( j in dom z & x = z . j ) by A4, FUNCT_1:def 3;
reconsider j = j as Nat by A73;
( ((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) . i <= len z & ((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) . i >= len z ) by A24, Th61, A66, A67;
then ( ((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) . i = len z & j < len z ) by A73, AFINSQ_1:86, XXREAL_0:1;
hence x <= (M . (n,I)) value_at (C,s) by A71, A73, A66, A67; :: thesis: verum

end;

for x being UpperBound of X holds (M . (n,I)) value_at (C,s) <= x

proof

let x be UpperBound of X; :: thesis: (M . (n,I)) value_at (C,s) <= x
( n in dom z & (M . (n,I)) value_at (C,s) = z . n ) by A66, A67, A71, A3, AFINSQ_1:86;
then (M . (n,I)) value_at (C,s) in X by A4, FUNCT_1:def 3;
hence (M . (n,I)) value_at (C,s) <= x by XXREAL_2:def 1; :: thesis: verum

end;

hence (M . (n,I)) value_at (C,s) = max X by A72, XXREAL_2:def 3; :: thesis: verum