良序单调量终止定理

**第一步($k$ 步后的递推界)。** 设 $s_0 \to s_1 \to s_2 \to \cdots \to s_k$ 为任意一条长为 $k$ 的合法转移序列。对 $i = 1, 2, \dots, k$ 应用条件 $M(s_{i}) \le M(s_{i-1}) - 1$ 并累加消去中间项,得 $M(s_k) \le M(s_0) - k$。

**第二步($k$ 的上界)。** 由于对每个可达状态 $s_k \in \mathcal{S}$ 都有 $M(s_k) \ge 0$,联立两式得 $0 \le M(s_k) \le M(s_0) - k$,移项即得 $k \le M(s_0)$。因此不存在长度 $k > M(s_0)$ 的合法轨迹,过程必在至多 $M(s_0)$ 步内终止。