On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal wrote:
I dont think it is any easier to prove the "will increase faster" proposition than it is to prove the whole thing.
They probably just impose restrictions so that they prove that there is reduction and progress over time. One common for strategy for proving termination is that something is reduced every iteration (or at some points in the program that is passed through).
