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)) = 1 holds
( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) )