Knuth Tests using Claude Sonnet 4.6 problem 1.1.2

Knuth Art Of Computer Programming V1 p9 ----------------------------------------------------------------------- Algorithm E (Euclid's algorithm). Given two positive integers m and n, find their greatest common divisor, that is, the largest positive integer that evenly divides both m and n.

E1 [Find remained] Divide m by n and r be the remainder. (We will know that 0 <= r < n)

E2 [Is it zero?] If r = 0, the algorithm terminates, n is the answer

E3 [Reduce] Set m = n, then n = r, then go back to step E1 -----------------------------------------------------------------------

Prove that m is always greater than n at the beginning of step E1, except possibly the first time this step occurs.

======================================================================== Claude Sonnet 4.6 ========================================================================

Proof

We want to show that m > n at the start of E1, for every iteration except possibly the first.

First Execution of E1

When E1 is executed the first time, m and n are simply whatever positive integers were given as input. There is no guarantee that m > n, which is why the exception exists. For example, with m = 2166 and n = 6099, we have m < n on the first call.

All Subsequent Executions of E1

After the first execution of E1, we reach E3 only if r ≠ 0 (checked at E2). At E3, the replacements are:

m = n n = r

Then we return to E1. So at the start of the next E1, the new values are:

m_new = n_old and n_new = r_old

From E1, we know r is the remainder when m is divided by n, so by definition:

0 ≤ r < n

Since E3 is only reached when r ≠ 0 (E2 would have terminated otherwise), we tighten this to:

0 < r < n

Therefore:

n_new = r_old < n_old = m_new

Which gives us:

m_new > n_new

Conclusion

After the first iteration, the new m is always the old n, and the new n is always the remainder r, which is strictly less than the old n. Therefore m > n holds at the beginning of every execution of E1 except possibly the first, which is what we wanted to prove. □