Certification Problem

Input (COPS 216)

We consider the TRS containing the following rules:

f(u(O),u(y)) A (1)
f(v(x),v(O)) B (2)
O u(O) (3)
O v(O) (4)
u(x) x (5)
v(x) x (6)
f(x,y) f(x,u(y)) (7)
f(x,y) f(v(x),y) (8)

The underlying signature is as follows:

{f/2, u/1, O/0, A/0, v/1, B/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2020)

1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.

t0 = f(v(O),v(O))
f(v(O),u(v(O)))
f(O,u(v(O)))
f(u(O),u(v(O)))
A
= t4

t0 = f(v(O),v(O))
B
= t1

The two resulting terms cannot be joined for the following reason: