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 V3() ManySortedSet of the carrier of S
for T being non-empty b1,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 m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let X be V3() 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 m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let G be basic GeneratorSystem over S,X,T; :: 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 A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let b be pure Element of the generators of G . the bool-sort of S; :: 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 f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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 implies (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 <> {} } )
assume A1: f in C -Execution (A,b,(\false C)) ; :: thesis: ( not G is C -supported or not i <> m or (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 <> {} } )
assume A2: G is C -supported ; :: thesis: ( not i <> m or (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 <> {} } )
assume A3: i <> m ; :: thesis: (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 <> {} }
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
proof
let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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: verum
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: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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: verum
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: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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: verum
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: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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: verum
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: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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: verum
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: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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: verum
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: ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or 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 <> {} } )
assume s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ; :: thesis: 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 <> {} }
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 ( 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))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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: 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))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
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: verum
end;
end;
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: ( ((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) )
hereby :: thesis: ( ((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) )
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)))))) . 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 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: 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)))))) . 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 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: verum
end;
end;
end;
A22: 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
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
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: 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
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: verum
end;
end;
end;
thus ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i by A1, A2, A5, Th65; :: thesis: ( (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) )
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: (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)
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: verum
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: verum