Total functional programming is a paradigm of non-Turing-complete programming languages where any program that type checks is proven to halt.
Well-founded recursion is a recursive definition of a function such that the definition of $f(x)$ only ever makes a recursive call $f(y)$ when $y<x$ for some well-founded relation $<$.
But the wikipedia page of Total functional programming refers also to other types of provably-terminating recursion:
[Termination is guaranteed by] a restricted form of recursion, which operates only upon 'reduced' forms of its arguments, such as Walther recursion, substructural recursion, or "strongly normalizing" as proven by abstract interpretation of code.
Are there any ways that one can do better than well-founded recursion, for practical total functional programming? I've always thought of well-founded recursion as "the most general provably terminating recursion"