| 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. □ |