for s being State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k, i being Nat st IC (Comput (P,s,k)) = 4 holds
Comput (P,s,(k + i)) = Comput (P,s,k)