let s be State of SCM; :: thesis: 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)
let P be Instruction-Sequence of SCM; :: thesis: ( Euclid-Algorithm c= P implies for k, i being Nat st IC (Comput (P,s,k)) = 4 holds
Comput (P,s,(k + i)) = Comput (P,s,k) )
assume A1: Euclid-Algorithm c= P ; :: thesis: for k, i being Nat st IC (Comput (P,s,k)) = 4 holds
Comput (P,s,(k + i)) = Comput (P,s,k)
let k, i be Nat; :: thesis: ( IC (Comput (P,s,k)) = 4 implies Comput (P,s,(k + i)) = Comput (P,s,k) )
assume IC (Comput (P,s,k)) = 4 ; :: thesis: Comput (P,s,(k + i)) = Comput (P,s,k)
then P halts_at IC (Comput (P,s,k)) by A1, Lm3;
hence Comput (P,s,(k + i)) = Comput (P,s,k) by EXTPRO_1:20, NAT_1:11; :: thesis: verum