Certification Problem

Input (COPS 599)

We consider the TRS containing the following rules:

+(x,y) if(y,x,s(+(x,-(y,s(0))))) (1)
+(x,y) +(y,x) (2)
if(0,y,z) y (3)
if(s(x),y,z) z (4)
if(x,y,y) y (5)
-(x,0) x (6)
-(0,s(y)) 0 (7)
-(s(x),s(y)) -(x,y) (8)

The underlying signature is as follows:

{+/2, if/3, s/1, -/2, 0/0}

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)
if(c_1,0,s(+(0,-(c_1,s(0)))))
if(c_1,0,s(+(-(c_1,s(0)),0)))
if(c_1,0,s(if(0,-(c_1,s(0)),s(+(-(c_1,s(0)),-(0,s(0)))))))
if(c_1,0,s(-(c_1,s(0))))
= t4

t0 = +(0,c_1)
+(c_1,0)
if(0,c_1,s(+(c_1,-(0,s(0)))))
c_1
= t3

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