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 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 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 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))) 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