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

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