\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}