theorem Th19:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
really-closed MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ( for
k being
Nat holds
I is_halting_on (StepWhile>0 (a,I,P,s)) . k,
P +* (while>0 (a,I)) ) & ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
while>0 (
a,
I)
is_halting_on s,
P