theorem Th2: :: AMI_4:2

for s being State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k being Nat st IC (Comput (P,s,k)) = 0 holds
( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) )