A recursive function terminates if in each recursive call the argument is decreased wrt. a given measure in a well-founded domain. That can easily be proven constructively by wellfounded induction over the measure of the argument. Straightforward extension of this criterion ("each call is decreasing") to mutually recursive functions is too strict. It is sufficient that whenever the same function appears in a call sequence, then the argument is decreased. The classical proof for the latter statement is still simple, but the constructive proof requires an additional wellordering on the function symbols.
First the notions of a call graph and its goodness are introduced for mutually recursive functions with one argument, then the harder case for functions with several arguments. A constructive proof is given for the first case and a sketch for the second.
The results are applicable for all pure functional programming languages and also for term rewriting systems and implementations of type-theory.