Certification Problem

Input (COPS 64)

We consider the TRS containing the following rules:

h(f,a,a) h(g,a,a) (1)
h(g,a,a) h(f,a,a) (2)
a a' (3)
h(x,a',y) h(x,y,y) (4)
h(x,y,a') h(x,y,y) (5)

The underlying signature is as follows:

{h/3, f/0, a/0, g/0, a'/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2023)

1 Non-Joinable Fork

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

t0 = h(g,a,a)
h(g,a,a')
h(g,a',a')
= t2

t0 = h(g,a,a)
h(f,a,a)
h(f,a,a')
h(f,a',a')
= t3

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