is type checking in D undecidable?

[Ola Fosheim Grøstad]

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).