Well-founded monovariant termination theorem

**Step 1 (inductive bound after $k$ moves).** Let $s_0 \to s_1 \to s_2 \to \cdots \to s_k$ be any sequence of $k$ valid moves. Applying the hypothesis $M(s_{i}) \le M(s_{i-1}) - 1$ for $i = 1, 2, \dots, k$ and summing telescopes the inequality to $M(s_k) \le M(s_0) - k$.

**Step 2 (upper bound on $k$).** Since $M(s_k) \ge 0$ for every reachable state $s_k \in \mathcal{S}$, combining the two inequalities gives $0 \le M(s_k) \le M(s_0) - k$, which rearranges immediately to $k \le M(s_0)$. Therefore no valid trajectory can have length $k > M(s_0)$, and the process must terminate in at most $M(s_0)$ steps.