I wrote a simple TRS that I believe is non-confluent, but I\'m not able to find

ID: 646132 • Letter: I

Question

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 F={f, l, s, o} and the rewrite rules R are defined as follows:

l?s(o)
t(x, l)?s(x)
t(l, x)?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?

t(o,l) has two normal forms: t(o,l)?s(o) and t(o,l)?t(o,s(o)).