let s be State of SCM ; :: thesis: for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-Algorithm c= P holds
for k, i being Element of NAT st IC (Comput P,s,k) = 4 holds
Comput P,s,(k + i) = Comput P,s,k
let P be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( Euclide-Algorithm c= P implies for k, i being Element of NAT st IC (Comput P,s,k) = 4 holds
Comput P,s,(k + i) = Comput P,s,k )
assume A1: Euclide-Algorithm c= P ; :: thesis: for k, i being Element of NAT st IC (Comput P,s,k) = 4 holds
Comput P,s,(k + i) = Comput P,s,k
let k, i be Element of 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 AMI_1:89, NAT_1:11; :: thesis: verum