\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)))\}$] There exists no monotone $\Sigma$-algebra ${\cal A}$ with $A = \nat$ proving $\SN(S)$.\\[.5em] \pause Assume contrary it would exist. Let $\alpha : {\cal X} \to A$, then: \vspace{-.7em} \begin{align*} \interpret{f(f(x)),\alpha} > \interpret{f(g(f(x))),\alpha}\;. \end{align*} \vspace{-2em} \pause But then also \vspace{-.7em} \begin{align*} \interpret{f(x),\alpha} > \interpret{g(f(x)),\alpha} \end{align*} \vspace{-2em} since otherwise: \begin{itemize} \item $\interpret{f(x),\alpha} = \interpret{g(f(x)),\alpha}$ implies $\interpret{f(f(x)),\alpha} = \interpret{f(g(f(x))),\alpha}$, \item $\interpret{f(x),\alpha} < \interpret{g(f(x)),\alpha}$ implies $\interpret{f(f(x)),\alpha} < \interpret{f(g(f(x))),\alpha}$ \end{itemize} by monotonicity.\\[.5em] \pause But then ${\cal A}$ would also prove termination of $f(x) \to g(f(x))$.\\[.5em] \end{example} \pause Thus we need another $\Sigma$-algebra, for example $A = \nat^2$. \end{frame}