CMP.2:4.4 - Supply base cases and a decreasing measure

Give a direct result for each case on which recursion stops. Then show that every recursive call reaches such a case after finitely many steps. A nonnegative integer that strictly decreases is often enough. A finite input constructor or a well-founded ordering can supply the same argument when one numerical size is awkward.

For the segment procedure, a singleton v returns (v,v,v,v). Split every longer interval into two nonempty shorter intervals. Its length decreases along every call path. This also explains why an empty interval needs its own convention or must be excluded before calling the procedure.

For nonnegative integers with b>0, Euclid’s call (a,b) → (b,a mod b) decreases the second component because 0≤a mod b<b. The first component may increase relative to its old value; it is the selected measure that must decrease. At b=0, return a, with the intended convention for (0,0) fixed separately.

When a termination checker fails, inspect which decrease is absent from its account. A supplied difference, lexicographic measure or invariant may express the progress already present in the procedure. If progress is genuinely missing, repair the procedure or weaken its claimed result. A small successful run alone does not establish return on every allowed input.