Bounding derivation lengths with functions from the slow growing hierarchy

Let be a (finite) rewrite system over a (finite) signature. Let be a strict well-founded termination ordering on the set of terms in question so that the rules of are reducing under . Then is terminating. In this article it is proved for a certain class of far reaching termination orderings (of order type reaching up to the first subrecursively inaccessible ordinal, i.e. the proof-theoretic ordinal of ) that – under some reasonable assumptions which are met in current applications – the derivation lengths function for is bounded by a function from the slow growing hierarchy of level determined by the order type of the underlying termination ordering. This result is a (correction of the proof of and a) strong generalization of theorem 8.1 in Cichon's article Termination orderings and complexity characterisations. Leeds, Proof Theory 1990, (Aczel, Simmons, and Wainer, editors), Cambridge University Press 1992, 171-193. Received: 2 February 1996