Certification Problem

Input (COPS 70)

We consider the TRS containing the following rules:

F(x,C(x)) A (1)
F(x,x) B (2)
a g(C(a)) (3)
g(x) x (4)

The underlying signature is as follows:

{F/2, C/1, A/0, B/0, a/0, g/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2023)

1 Non-Joinable Fork

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

t0 = F(a,a)
F(a,g(C(a)))
F(a,C(a))
A
= t3

t0 = F(a,a)
B
= t1

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