let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
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 i being pure Element of the generators of G . I
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
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 i being pure Element of the generators of G . I
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let I be integer SortSymbol of S; :: thesis: for i being pure Element of the generators of G . I
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let i be pure Element of the generators of G . I; :: 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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
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 holds
for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
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 implies for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
assume A1: ( f in C -Execution (A,b,(\false C)) & G is C -supported ) ; :: thesis: for t0, t1 being Element of T,I
for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let t0, t1 be Element of T,I; :: thesis: for J being Algorithm of A
for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let J be Algorithm of A; :: thesis: for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds
for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
let P be set ; :: thesis: ( P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) implies for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
assume A2: P is_invariant_wrt i := (t0,A),f ; :: thesis: ( not P is_invariant_wrt b gt (t1,(@ i),A),f or not P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f or not P is_invariant_wrt J,f or not J is_terminating_wrt f,P or ex s being Element of C -States the generators of G st
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) implies not t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) or for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
assume A3: P is_invariant_wrt b gt (t1,(@ i),A),f ; :: thesis: ( not P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f or not P is_invariant_wrt J,f or not J is_terminating_wrt f,P or ex s being Element of C -States the generators of G st
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) implies not t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) or for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
assume A4: P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f ; :: thesis: ( not P is_invariant_wrt J,f or not J is_terminating_wrt f,P or ex s being Element of C -States the generators of G st
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) implies not t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) or for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
assume A5: P is_invariant_wrt J,f ; :: thesis: ( not J is_terminating_wrt f,P or ex s being Element of C -States the generators of G st
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) implies not t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) or for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
assume A6: J is_terminating_wrt f,P ; :: thesis: ( ex s being Element of C -States the generators of G st
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) implies not t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) or for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P )
set W = b gt (t1,(@ i),A);
set L = i := (((@ i) + (\1 (T,I))),A);
set K = i := (t0,A);
set ST = C -States the generators of G;
set TV = (\false C) -States ( the generators of G,b);
assume A7: for s being Element of C -States the generators of G holds
( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ; :: thesis: for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P
A8: i := (t0,A) is_terminating_wrt f,P by AOFA_000:107;
i := (((@ i) + (\1 (T,I))),A) is_terminating_wrt f,P by AOFA_000:107;
then A9: ( b gt (t1,(@ i),A) is_terminating_wrt f & J \; (i := (((@ i) + (\1 (T,I))),A)) is_terminating_wrt f,P ) by A5, A6, AOFA_000:104, AOFA_000:111;
A10: for s being Element of C -States the generators of G st s in P & f . ((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))),(b gt (t1,(@ i),A))) in (\false C) -States ( the generators of G,b) holds
f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))) in P by A5, A4, AOFA_000:109, AOFA_000:def 39;
for s being Element of C -States the generators of G st f . (s,(b gt (t1,(@ i),A))) in P holds
f iteration_terminates_for (J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)),f . (s,(b gt (t1,(@ i),A)))

proof

let s be Element of C -States the generators of G; :: thesis: ( f . (s,(b gt (t1,(@ i),A))) in P implies f iteration_terminates_for (J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)),f . (s,(b gt (t1,(@ i),A))) )
assume f . (s,(b gt (t1,(@ i),A))) in P ; :: thesis: f iteration_terminates_for (J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)),f . (s,(b gt (t1,(@ i),A)))
defpred S₁[ Element of C -States the generators of G] means ($1 . I) . i < t1 value_at (C,$1);
deffunc H₁( Element of C -States the generators of G) -> Element of NAT = In (((t1 value_at (C,$1)) - (($1 . I) . i)),NAT);
( (@ i) value_at (C,s) = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) ) by A7, Th61;
then A11: ( f . (s,(b gt (t1,(@ i),A))) in (\false C) -States ( the generators of G,b) iff S₁[f . (s,(b gt (t1,(@ i),A)))] ) by A1, Th66;
A12: for s being Element of C -States the generators of G st S₁[s] holds
( ( S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] implies f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] ) & H₁(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) < H₁(s) )

proof

let s be Element of C -States the generators of G; :: thesis: ( S₁[s] implies ( ( S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] implies f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] ) & H₁(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) < H₁(s) ) )
assume A13: S₁[s] ; :: thesis: ( ( S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] implies f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] ) & H₁(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) < H₁(s) )
A14: f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) = f . ((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))),(b gt (t1,(@ i),A))) by AOFA_000:def 29;
then ( (@ i) value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = ((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i & ((f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) . I) . i = ((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i & t1 value_at (C,(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))))) = t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) ) by A7, Th61;
hence ( S₁[f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))] iff f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)))) in (\false C) -States ( the generators of G,b) ) by A14, A1, Th66; :: thesis: H₁(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) < H₁(s)
A15: ((s . I) . i) + 1 <= t1 value_at (C,s) by A13, INT_1:7;
A16: ((@ i) value_at (C,(f . (s,J)))) + ((\1 (T,I)) value_at (C,(f . (s,J)))) = ((@ i) value_at (C,(f . (s,J)))) + ((\1 (T,I)) value_at (C,(f . (s,J)))) by AOFA_A00:55;
H₁(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) = In (((t1 value_at (C,(f . ((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))),(b gt (t1,(@ i),A)))))) - (((f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) . I) . i)),NAT) by AOFA_000:def 29
.= In (((t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))))) - (((f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) . I) . i)),NAT) by A7
.= In (((t1 value_at (C,s)) - (((f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) . I) . i)),NAT) by A7
.= In (((t1 value_at (C,s)) - (((f . ((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))),(b gt (t1,(@ i),A)))) . I) . i)),NAT) by AOFA_000:def 29
.= In (((t1 value_at (C,s)) - (((f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A))))) . I) . i)),NAT) by A7
.= In (((t1 value_at (C,s)) - (((f . ((f . (s,J)),(i := (((@ i) + (\1 (T,I))),A)))) . I) . i)),NAT) by AOFA_000:def 29
.= In (((t1 value_at (C,s)) - (((@ i) + (\1 (T,I))) value_at (C,(f . (s,J))))),NAT) by A1, Th65
.= In (((t1 value_at (C,s)) - (((@ i) value_at (C,(f . (s,J)))) + ((\1 (T,I)) value_at (C,(f . (s,J)))))),NAT) by A16, Th39
.= In (((t1 value_at (C,s)) - ((((f . (s,J)) . I) . i) + ((\1 (T,I)) value_at (C,(f . (s,J)))))),NAT) by Th61
.= In (((t1 value_at (C,s)) - (((s . I) . i) + ((\1 (T,I)) value_at (C,(f . (s,J)))))),NAT) by A7
.= In (((t1 value_at (C,s)) - (((s . I) . i) + 1)),NAT) by Th37
.= ((t1 value_at (C,s)) - ((s . I) . i)) - 1 by A15, INT_1:5, SUBSET_1:def 8
.= H₁(s) - 1 by A13, INT_1:5, SUBSET_1:def 8 ;
hence H₁(f . (s,((J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A))))) < H₁(s) by XREAL_1:44; :: thesis: verum

end;

thus f iteration_terminates_for (J \; (i := (((@ i) + (\1 (T,I))),A))) \; (b gt (t1,(@ i),A)),f . (s,(b gt (t1,(@ i),A))) from AOFA_000:sch 3(A11, A12); :: thesis: verum

end;

then while ((b gt (t1,(@ i),A)),(J \; (i := (((@ i) + (\1 (T,I))),A)))) is_terminating_wrt f,P by A3, A9, A10, AOFA_000:118;
hence for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P by A2, A8, AOFA_000:111; :: thesis: verum