Certification Problem

Input (COPS 584)

We consider the TRS containing the following rules:

br(0,y,z) y (1)
br(s(x),y,z) z (2)
p(0) 0 (3)
p(s(x)) x (4)
+(x,y) br(x,y,+(p(x),s(y))) (5)
+(x,y) br(y,x,+(s(x),p(y))) (6)

The underlying signature is as follows:

{br/3, 0/0, s/1, p/1, +/2}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2021)

1 Non-Joinable Fork

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

t0 = +(x,y)
br(x,y,+(p(x),s(y)))
= t1

t0 = +(x,y)
br(y,x,+(s(x),p(y)))
= t1

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