let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis:
let X be non-empty ManySortedSet of the carrier of S; :: thesis:
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis:
let C be bool-correct 4,1 integer 11,1,1 -array image of T; :: thesis:
let G be basic GeneratorSystem over S,X,T; :: thesis:
let I be integer SortSymbol of S; :: thesis:
let m, i be pure Element of the generators of G . I; :: thesis:
let M be pure Element of the generators of G . (the_array_sort_of S); :: thesis:
let b be pure Element of the generators of G . the bool-sort of S; :: thesis:
let A be elementary IfWhileAlgebra of the generators of G; :: thesis:
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis:
assume A1: f in C -Execution (A,b,(\false C)) ; :: thesis:
assume A2: G is C -supported ; :: thesis:
assume A3: i <> m ; :: thesis:
set J = m := ((\0 (T,I)),A);
set K = i := ((\1 (T,I)),A);
set W = b gt ((length ((@ M),I)),(@ i),A);
set L = i := (((@ i) + (\1 (T,I))),A);
set N = b gt (((@ M) . (@ i)),((@ M) . (@ m)),A);
set O = m := ((@ i),A);
set a = the_array_sort_of S;
set P = { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ;
A4: ( the Sorts of C . the bool-sort of S = BOOLEAN & the Sorts of C . (the_array_sort_of S) = INT ^omega ) by Th74, AOFA_A00:def 32;
then A5: ( the bool-sort of S <> the_array_sort_of S & I <> the_array_sort_of S & the bool-sort of S <> I ) by Th73, AOFA_A00:53;
A6: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt m := ((\0 (T,I)),A),f

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then consider s1 being Element of C -States the generators of G such that
A7: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
((f . (s,(m := ((\0 (T,I)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, A2, A5, Th65;
hence f . (s,(m := ((\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A7; :: thesis:

end;

A8: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt i := ((\1 (T,I)),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then consider s1 being Element of C -States the generators of G such that
A9: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
((f . (s,(i := ((\1 (T,I)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, A2, A5, Th65;
hence f . (s,(i := ((\1 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A9; :: thesis:

end;

A10: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt b gt ((length ((@ M),I)),(@ i),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then consider s1 being Element of C -States the generators of G such that
A11: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, A2, A4, Th65;
hence f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A11; :: thesis:

end;

A12: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then consider s1 being Element of C -States the generators of G such that
A13: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
((f . (s,(i := (((@ i) + (\1 (T,I))),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, A2, A5, Th65;
hence f . (s,(i := (((@ i) + (\1 (T,I))),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A13; :: thesis:

end;

A14: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt b gt (((@ M) . (@ i)),((@ M) . (@ m)),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then consider s1 being Element of C -States the generators of G such that
A15: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, A2, A4, Th65;
hence f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A15; :: thesis:

end;

A16: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt m := ((@ i),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then consider s1 being Element of C -States the generators of G such that
A17: ( s = s1 & (s1 . (the_array_sort_of S)) . M <> {} ) ;
((f . (s,(m := ((@ i),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M by A1, A2, A5, Th65;
hence f . (s,(m := ((@ i),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A17; :: thesis:

end;

set ST = C -States the generators of G;
set TV = (\false C) -States ( the generators of G,b);
A18: f complies_with_if_wrt (\false C) -States ( the generators of G,b) by AOFA_000:def 32;
A19: { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis:
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis:
then A20: f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A14;

per cases ;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) ; :: thesis:

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 A18;
hence f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A20, A16; :: thesis:

end;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ; :: thesis:

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 A18;
hence f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A20, AOFA_000:def 28; :: thesis:

end;

A21: m := ((\0 (T,I)),A) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by AOFA_000:107;
for s being Element of C -States the generators of G holds
( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i & (length ((@ M),I)) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = (length ((@ M),I)) value_at (C,s) & (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),I)) value_at (C,s) )

proof

let s be Element of C -States the generators of G; :: thesis:

hereby :: thesis:

per cases ;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) ; :: thesis:

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 A18;
hence ((f . (s,(if-then ((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, A2, A3, Th65
.= (s . I) . i by A1, A2, A5, Th65 ;
:: thesis:

end;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ; :: thesis:

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 A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . i by AOFA_000:def 28
.= (s . I) . i by A1, A2, A5, Th65 ;
:: thesis:

end;

A22: now :: thesis:

per cases ;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) ; :: thesis:

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 A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M by A1, A2, A5, Th65
.= (s . (the_array_sort_of S)) . M by A1, A2, A4, Th65 ;
:: thesis:

end;

suppose f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) ; :: thesis:

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 A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = ((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M by AOFA_000:def 28
.= (s . (the_array_sort_of S)) . M by A1, A2, A4, Th65 ;
:: thesis:

end;

thus ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i by A1, A2, A5, Th65; :: thesis:
A23: ( (@ M) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = ((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 & (@ M) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M & (@ M) value_at (C,s) = (s . (the_array_sort_of S)) . M ) by Th61;
thus (length ((@ M),I)) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = length (((@ M) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A)))))),I) by Th81
.= len (((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M) by A23, Th74
.= len ((s . (the_array_sort_of S)) . M) by A1, A2, A4, Th65
.= length (((@ M) value_at (C,s)),I) by A23, Th74
.= (length ((@ M),I)) value_at (C,s) by Th81 ; :: thesis:
thus (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 (((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 A23, Th74
.= len (((f . ((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 AOFA_000:def 29
.= len (((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M) by A1, A2, A5, Th65
.= length (((@ M) value_at (C,s)),I) by A23, A22, Th74
.= (length ((@ M),I)) value_at (C,s) by Th81 ; :: thesis:

end;

then for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A1, A2, A8, A10, A12, A19, Th94, AOFA_000:107;
hence (m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } by A6, A21, AOFA_000:111; :: thesis: