theorem Th22: :: AMI_8:22

for s being State of SCM
for I being Instruction of SCM
for P being Instruction-Sequence of SCM st IterativeAlgorithm I c= P holds
for k being Nat st IC (Comput (P,s,k)) = 3 holds
( IC (Comput (P,s,(k + 1))) = 4 & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 1)) - ((Comput (P,s,k)) . (dl. 0)) & ( for j being Nat st j <> 1 holds
(Comput (P,s,(k + 1))) . (dl. j) = (Comput (P,s,k)) . (dl. j) ) )