theorem Th29: :: AMI_8:29

for I being Instruction of SCM
for A being Integer
for N being Nat
for P being Instruction-Sequence of SCM st ( I = AddTo ((dl. 2),(dl. 1)) or I = SubFrom ((dl. 2),(dl. 1)) or I = MultBy ((dl. 2),(dl. 1)) ) & IterativeAlgorithm I c= P holds
for s being 0 -started State-consisting of <%1,N,A%> holds
( P halts_on s & (Comput (P,s,1)) . (dl. 2) = A & ( for k being Nat st 0 < k & k < N holds
IC (Comput (P,s,(4 * k))) = 5 ) & ( for k being Nat st k < N holds
( IC (Comput (P,s,((4 * k) + 1))) = 2 & IC (Comput (P,s,((4 * k) + 2))) = 3 & IC (Comput (P,s,((4 * k) + 3))) = 4 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 2))) . (dl. 1) = N - k & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (N - k) - 1 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 1))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 2))) . (dl. 1) > 0 ) ) & ( N <> 0 implies ( LifeSpan (P,s) = 4 * N & ( for k, j being Nat st k >= N holds
( IC (Comput (P,s,((4 * k) + j))) = 1 & (Comput (P,s,(((4 * k) + 1) + j))) . (dl. 1) = 0 ) ) ) ) )