Certification Problem

Input (COPS 569)

We consider the TRS containing the following rules:

s(p(x)) x (1)
p(s(x)) x (2)
+(x,0) x (3)
+(x,s(y)) s(+(x,y)) (4)
+(x,p(y)) p(+(x,y)) (5)
-(x,0) x (6)
-(x,s(y)) p(-(x,y)) (7)
-(x,p(y)) s(-(x,y)) (8)
*(x,0) 0 (9)
*(x,s(y)) +(*(x,y),x) (10)
*(x,p(y)) -(*(x,y),x) (11)

The underlying signature is as follows:

{s/1, p/1, +/2, 0/0, -/2, */2}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2022)

1 Non-Joinable Fork

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

t0 = *(c_2,s(p(c_1)))
+(*(c_2,p(c_1)),c_2)
+(-(*(c_2,c_1),c_2),c_2)
= t2

t0 = *(c_2,s(p(c_1)))
*(c_2,c_1)
= t1

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