Certification Problem

Input (COPS 635)

We consider the TRS containing the following rules:

plus(0,y) y (1)
plus(s(x),y) s(plus(x,y)) (2)
qplus(0,y) y (3)
qplus(s(x),y) qplus(x,s(y)) (4)
plus(x,y) qplus(x,y) (5)

The underlying signature is as follows:

{plus/2, 0/0, s/1, qplus/2}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2022)

1 Non-Joinable Fork

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

t0 = plus(s(x160),y)
s(plus(x160,y))
s(qplus(x160,y))
= t2

t0 = plus(s(x160),y)
qplus(s(x160),y)
qplus(x160,s(y))
= t2

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