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