I wrote a simple TRS that I believe is non-confluent, but I'm not able to find a term with two normal forms for it.The TRS is defined on the signature $\mathcal F=\{f,\ l,\ s,\ o\}$ and the rewrite rules $\mathcal R$ are defined as follows:$l\to s(o)$$t(x,\ l)\to s(x)$$t(l,\ x)\to s(x)$.This TRS is clearly finite and terminating.For the first two rules, we have a critical pair $(t(x,\ s(o)),\ s(x))$ which is not joinable. Therefore, the TRS is not confluent.It seems that for such a simple example I should be able to find a term with two normal forms. What am I missing?
Term rewrite system is non-confluent, but cannot find different normal forms of term
normal forms;term rewriting
$t(o,l)$ has two normal forms: $t(o,l)\to s(o)$ and $t(o,l)\to t(o,s(o))$. 