Prove progress with lexicographic descent and an exact work count

Try

Two counters store natural numbers a and b, including zero. If b is positive, subtract one from b. Otherwise, if a is positive, replace the pair by (a−1,2a). The expression 2a uses the old value of a. Stop at (0,0). One application of either branch counts as one transition.

Start at (2,1). The next states are (2,0), (1,4), (1,3). Draw those arrows and label the branch used. The counters remain natural numbers, but their sum rises from two to five at the reset. Staying inside the permitted domain is a safety property. It does not yet explain why the process must finish.

Predict

Predict the number of transitions from (2,1) to (0,0). Does a+b decrease at every step? Could a alone serve as a strictly decreasing count? Neither works: the sum can rise, while a stays unchanged during drains. We need a measure that respects the different roles of the counters.

Compare pairs in lexicographic order: (c,d) is smaller than (a,b) if c is smaller than a, or if c=a and d is smaller than b. The first coordinate has priority, as the first differing letter does in dictionary order. Unlike ordinary dictionary words, our objects have exactly two coordinates, both natural numbers; those domain conditions matter for the proof.

Experiment

Choose (2,1) in the explorer. Predict each reset before stepping. Compare the pair, its sum and the displayed rank. Then try each faulty mode and identify a state or cycle that can repeat. The controls and retained trace are bounded demonstrations; a display limit is not a proof that a process stops.

Predict the next state, then inspect the trace

At b>0, subtract one from b. Otherwise, when a>0, the correct rule replaces (a,0) by (a−1,2a), using the old a. Only (0,0) is terminal. Count transitions, not seconds.

Initial a012345678 Initial b012345678910111213141516 Transition ruleCorrect: reduce a before the next phaseFault: stay unchanged when b=0Fault: refill b without reducing a Transition budget01520100

Before revealing, write the next two states and predict whether a+b must decrease. The candidate rank is R(a,b)=b+a²+2a; its interpretation as exact remaining transitions belongs only to the correct rule.

Reveal bounded traceReset counters

Trace not revealed. Changing any setting clears earlier results.

Temporary practice: no mastery or saved response is created. The tool permits a≤8, b≤16 and at most 100 transitions; the general mathematical proof has a wider domain. It uses exact integer arithmetic and has no automatic animation.

This separate worked trace makes the arithmetic inspectable even without interaction:

State	Next branch	Sum a+b	Rank R=b+a²+2a
(2,1)	Drain	3	9
(2,0)	Reset using old a=2	2	8
(1,4)	Drain	5	7
(1,0), after four further drains	Reset using old a=1	1	3
(0,2)	Drain	2	2
(0,0), after two further drains	Stop	0	0

Fill in the omitted states and their ranks. There are nine transitions, not six table rows or nine condition checks. The table compresses consecutive drains; your complete trace should not.

Understand

First prove safety. A drain is enabled only when b is positive, so b−1 is still natural. A reset is enabled only when a is positive, so a−1 and 2a are natural. Thus the natural-pair invariant holds initially and after every transition.

Next prove progress. A drain fixes a and strictly decreases b. A reset strictly decreases a, so the new pair is lexicographically smaller even if b grows. Why can this not continue forever? In a hypothetical infinite descent, a never increases and can strictly decrease at most its initial value times. After its last decrease, a would be constant forever. Every subsequent step would then strictly decrease the natural number b, which is impossible infinitely often. This proves the required well-foundedness rather than merely naming an order.

Every nonzero state has an enabled branch. Consequently an execution that always takes its enabled transition cannot stop anywhere except (0,0), and the descent proof says it cannot continue forever. Together, invariant preservation, the terminal-state argument and termination establish total correctness for this specification. Waiting forever without taking an enabled step is not an execution of the specified mathematical process; an interactive learner may pause without making a mathematical transition.

We can derive more: an exact remaining-work count. Initially drain b times. For each old value j=a,a−1,…,1, one reset creates 2j further drains. The total is

R(a,b)=b+Σ from j=1 to a of (1+2j)=b+a+a(a+1)=b+a²+2a.

For a drain, R falls by one immediately. For a reset, the new rank is 2a+(a−1)²+2(a−1)=a²+2a−1, again one below the old rank. All terms are nonnegative, and R=0 exactly at (0,0). Thus R counts remaining transitions, not just an upper bound. The formula relies on this reset rule; it is not a generic rank for every two-counter process.

Apply

Allowing a stutter transition that leaves a nonterminal pair unchanged preserves safety but permits an infinite constant execution. Merely requiring R never to increase does not exclude that behavior. A faulty refill (a,0)→(a,2a) creates the cycle (1,0)→(1,2)→(1,1)→(1,0). Write the rank at each state and locate the increase. A bounded screen trace cannot prove termination, but an explicitly repeatable cycle proves that the stated faulty execution does not terminate.

Now allow a correct reset to choose any finite natural N: (a,0)→(a−1,N). Lexicographic descent still proves termination for every choice sequence. Yet from (1,0), choosing N gives N+1 transitions, so there is no uniform finite bound over all such choices. The earlier scalar R can increase. A termination proof and an exact complexity formula are different achievements.

Finally change the numeric domain. Starting at rational x=1 and repeatedly halving while positive gives 1,1/2,1/4,… . Every step strictly decreases, and zero is a lower bound, but no finite step reaches zero. The missing hypothesis is well-foundedness, not boundedness alone. State the domain every time you propose a decreasing measure.

Continue

For an unfamiliar algorithm, retain separate records of its precondition, safety invariant, progress argument, postcondition and cost convention. The six tasks ask for traces, universal proofs, changed-rule counterexamples and a generalized reset argument. Counted transitions do not measure arithmetic bit cost, UI rendering or elapsed time. A saved written argument needs review; neither a stopped animation nor a completed worksheet automatically certifies total correctness.