\begin{frame} \frametitle{A non-simply terminating TRS: $f(f(x)) \to f(g(f(x)))$} \begin{example}[$S = \{f(f(x)) \to f(g(f(x)))\}$] We choose the $\Sigma$-algebra $(\nat^2,\interpret{\cdot})$ with: \begin{align*} {\rm [f]}(\vec{x}) &= \left(\begin{array}{cc} \emph{1} & 1\\ 0 & 0\\ \end{array} \right) \cdot \vec{x} + \left(\begin{array}{c} 0\\ 1\\ \end{array} \right) & {\rm [g]}(\vec{x}) &= \left(\begin{array}{cc} \emph{1} & 0\\ 0 & 0\\ \end{array} \right) \cdot \vec{x} + \left(\begin{array}{c} 0\\ 0\\ \end{array} \right) \end{align*} \vspace{-0.5em} \pause where $>$ on $\nat^2$ is defined as follows: \begin{align*} \left(\begin{array}{c} x_1\\ x_2\\ \end{array} \right) > \left(\begin{array}{c} y_1\\ y_2\\ \end{array} \right) \Longleftrightarrow x_1 > y_1 \text{ and } x_2 \ge y_2 \end{align*} \vspace{-0.5em} \pause Let $\alpha{:}\ {\cal X} \to A$ be arbitrary; write $\vec{x} = \alpha(x)$. We obtain \begin{align*} [f(f(x))] = \left(\begin{array}{cc} 1 & 1\\ 0 & 0\\ \end{array} \right) \cdot \vec{x} + \left(\begin{array}{c} \emph{1}\\ 1\\ \end{array} \right) &> \left(\begin{array}{cc} 1 & 1\\ 0 & 0\\ \end{array} \right) \cdot \vec{x} + \left(\begin{array}{c} \emph{0}\\ 1\\ \end{array} \right) = [f(g(f(x)))] \end{align*} \vspace{-0.5em} \pause Hence $S$ is terminating. \end{example} \end{frame}