theorem :: AMI_8:28

for I being Instruction of SCM
for A being Integer
for N being Nat
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P & I is sequential & I is 0 -dl.constant holds
for s being 0 -started State-consisting of <%1,N,A%> st (Comput (P,s,2)) . (dl. 1) = (Comput (P,s,1)) . (dl. 1) & ( for k being Nat holds (Comput (P,s,((4 * k) + 6))) . (dl. 1) = (Comput (P,s,((4 * k) + 5))) . (dl. 1) ) holds
( P halts_on s & IC (Comput (P,s,0)) = 0 & (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 ) ) ) ) )