theorem Th94:
for
S being non
empty non
void 1-1-connectives bool-correct 4,1
integer 11,1,1
-array 11
array-correct BoolSignature for
X being
V3()
ManySortedSet of the
carrier of
S for
T being
non-empty b2,
b1 -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