Many termination checkers support lexicographic (structural) recursion.  The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases.  Connections with nested recursion and ordinals discussed.