1: \begin{definition}

2: Let $\RS$ be a TRS whose termination is shown via Theorem~\ref{t:termination}, and $\PT$

3: the proof tree employed by the theorem. Let $k$ be the maximum number of SCCs in any

4: dependency graph employed by any instance of $\PhiDG$ occurring in $\PT$, and let

5: $g \colon \N \to \N$ denote a monotone function such that:

6: %

7: \begin{align*}

8:   g(n) &\geqslant \max (\{k\} \cup \{ \dheight(t^\sharp,\rsrew{(\PP \setminus \QQ) / (\RS \cup \QQ)}) \mid

9:   \text{there exists an edge from $(\PP,\RS)$ to $(\QQ,\RS)$} \\

10:   &\qquad \text{in $\PT$ labelled by an instance of $\PhiRP$

11:   and $\size{t} \leqslant n$}\}) \tpkt

12: \end{align*}

13: %

14: Then $g$ is called a \emph{reduction pair function} of $\RS$ with respect to $\PT$.

15: \end{definition}

16: