let s be State of SCM ; :: thesis: ( Euclide-Algorithm c= s implies for k, i being Element of NAT st IC (Comput (ProgramPart s),s,k) = 4 holds
Comput (ProgramPart s),s,(k + i) = Comput (ProgramPart s),s,k )
assume A1: Euclide-Algorithm c= s ; :: thesis: for k, i being Element of NAT st IC (Comput (ProgramPart s),s,k) = 4 holds
Comput (ProgramPart s),s,(k + i) = Comput (ProgramPart s),s,k
let k, i be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart s),s,k) = 4 implies Comput (ProgramPart s),s,(k + i) = Comput (ProgramPart s),s,k )
assume IC (Comput (ProgramPart s),s,k) = 4 ; :: thesis: Comput (ProgramPart s),s,(k + i) = Comput (ProgramPart s),s,k
then s halts_at IC (Comput (ProgramPart s),s,k) by A1, Lm3;
hence Comput (ProgramPart s),s,(k + i) = Comput (ProgramPart s),s,k by AMI_1:89, NAT_1:11; :: thesis: verum