克努斯测试使用克劳德十四行诗 4.6 问题 1.1.2
Knuth 测试使用 Claude Sonnet 4.6 问题 1.1.2
-----------------------------------------------------------------------
算法 E（欧几里得算法）。给定两个正整数 m 和 n，找出它们的最大公约数，即同时整除 m 和 n 的最大正整数。
E1 [找余数] 将 m 除以 n，r 为余数。（我们知道 0 ≤ r < n）
E2 [是否为零？] 如果 r = 0，算法终止，n 为答案。
E3 [简化] 设 m = n，然后 n = r，然后返回到步骤 E1。
-----------------------------------------------------------------------
证明在 E1 步骤开始时，m 总是大于 n，除了可能是第一次执行该步骤。
========================================================================
Claude Sonnet 4.6
========================================================================
证明
我们想要证明在每次迭代的 E1 开始时，m > n，除了可能是第一次。
第一次执行 E1
当第一次执行 E1 时，m 和 n 只是输入的任意正整数。没有保证 m > n，这就是存在例外的原因。例如，当 m = 2166 和 n = 6099 时，第一次调用时 m < n。
所有后续执行 E1
在第一次执行 E1 后，只有当 r ≠ 0（在 E2 中检查）时，我们才能到达 E3。在 E3 中，替换为：
m = n
n = r
然后我们返回到 E1。因此，在下一个 E1 的开始时，新值为：
m_new = n_old 和 n_new = r_old
根据 E1，我们知道 r 是 m 除以 n 的余数，因此根据定义：
0 ≤ r < n
由于 E3 只有在 r ≠ 0 时才会到达（否则 E2 会终止），我们可以进一步收紧为：
0 < r < n
因此：
n_new = r_old < n_old = m_new
这给我们：
m_new > n_new
结论
在第一次迭代后，新 m 始终是旧 n，而新 n 始终是余数 r，且严格小于旧 n。因此，m > n 在每次执行 E1 的开始时都成立，除了可能是第一次，这正是我们想要证明的。 □
查看原文
Knuth Tests using Claude Sonnet 4.6 problem 1.1.2<p>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.<p>E1 [Find remained] Divide m by n and r be the remainder. (We will
know that 0 <= r < n)<p>E2 [Is it zero?] If r = 0, the algorithm terminates, n is the answer<p>E3 [Reduce] Set m = n, then n = r, then go back to step E1
-----------------------------------------------------------------------<p>Prove that m is always greater than n at the beginning of step E1,
except possibly the first time this step occurs.<p>========================================================================
Claude Sonnet 4.6
========================================================================<p>Proof<p>We want to show that m > n at the start of E1, for every iteration
except possibly the first.<p>First Execution of E1<p>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.<p>All Subsequent Executions of E1<p>After the first execution of E1, we reach E3 only if r ≠ 0 (checked at
E2). At E3, the replacements are:<p>m = n
n = r<p>Then we return to E1. So at the start of the next E1, the new values
are:<p>m_new = n_old and n_new = r_old<p>From E1, we know r is the remainder when m is divided by n, so by
definition:<p>0 ≤ r < n<p>Since E3 is only reached when r ≠ 0 (E2 would have terminated
otherwise), we tighten this to:<p>0 < r < n<p>Therefore:<p>n_new = r_old < n_old = m_new<p>Which gives us:<p>m_new > n_new<p>Conclusion<p>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. □