ch:size-change-termination: ch:size-change-termination

Writing strict, weak, and unknown as temporarily, For entry $(1,1)$ the intermediate first parameter of $f$ witnesses . For $(2,1)$ the same intermediate parameter witnesses . Every path to column $2$ contains an unknown entry. Squaring the result preserves the matrix, so it is idempotent and its first diagonal entry is strict.

The one-by-one matrix is idempotent and has a strict diagonal, so the finite test accepts. But the concrete call preserves $x$, so the strict label is false: truthfulness, the execution-to-graph hypothesis of theorem 83.8, fails. The strongest truthful matrix is $M=({\Downarrow }^{=})$; it is idempotent with no strict diagonal and is rejected.

With rows callee and columns caller, the two branch matrices are Here $A$ is the branch and $B$ the branch. Saturation has four idempotent diagonal patterns: For example $A;A$ has pattern and $B;B$ has . Mixed products strengthen the first or third entries and give the remaining two patterns. Every idempotent has a strict second diagonal, so the criterion accepts.

For false truthfulness, use $h(n)=h(n)$ but label the self-edge strict over the well-founded natural order; the test accepts a lie. For a non-well-founded order, use integers with the usual and $h(z)=h(z-1)$; the label is truthful and strict, but the calls descend forever. For failure of the strict-diagonal condition, use $h(n)=h(n)$ with the truthful weak matrix. The order is well founded and the graph truthful, but the idempotent has no strict diagonal and the execution is infinite.

The direct matrices are those of the chapter. Closure contains two self-matrices at $f$, one at $g$, and their typed cross-edges. The idempotent self-matrix at either function is the weaker self-composite at $f$ squares to it and is not idempotent. Thus every idempotent self-cycle has a strict first diagonal.

After both positivity guards are erased from the abstraction, the two direct strict entries become weak. Composing the mutated edges gives Its square is itself and neither diagonal is strict, so it is the requested bad idempotent. Weakening only the $f\to g$ edge would not suffice: the strict $g\to f$ edge would still force descent around every alternating cycle.

Suppose an infinite multipath has no descending thread. One function name $f$ occurs infinitely often; this is the first use of finiteness. Color each pair of selected occurrences by the composite matrix between them. There are finitely many such matrices; this is the second use. Infinite Ramsey for pairs yields an infinite homogeneous subsequence with color $M:f\to f$. For three members , the segment $i\to k$ has color $M$ and is the composition of the two color-$M$ segments, hence $M;M=M$. If $M_{rr}$ were strict, choosing parameter $r$ through every homogeneous segment would give an infinitely descending thread, contrary to the assumption. Therefore $M$ is an idempotent in the closure with no strict diagonal.

Associate each callee variable with its source expression. A projection or unchanged variable gives a weak edge to that caller variable; a syntactic predecessor $\mathsf{pred}(x)$ under a positive guard gives a strict edge; a variable permutation merely relocates that edge. All other entries are unknown. The call $(x,y)\mapsto (x,x+y)$ therefore records only the weak edge from the new first component to $x$, even when a surrounding invariant implies a useful decrease of some arithmetic measure. Missing that semantic fact can make a terminating program fail the test, but every recorded edge remains true, so soundness is unchanged.