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 ACP @ CoCo 2020)

1 Non-Joinable Fork

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

t0 = +(0,c_1)
→ br(c_1,0,+(s(0),p(c_1)))
→ br(c_1,0,br(s(0),p(c_1),+(p(s(0)),s(p(c_1)))))
→ br(c_1,0,+(p(s(0)),s(p(c_1))))
→ br(c_1,0,+(0,s(p(c_1))))
= t4

t0 = +(0,c_1)
→ br(0,c_1,+(p(0),s(c_1)))
→ c_1
= t2

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