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 csi @ CoCo 2022)

1 Non-Joinable Fork

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

t0 = +(x,y)
if(y,x,s(+(x,-(y,s(0)))))
if(y,x,s(+(-(y,s(0)),x)))
if(y,x,s(+(x,-(y,s(0)))))
= t3

t0 = +(x,y)
+(y,x)
if(x,y,s(+(y,-(x,s(0)))))
if(x,y,s(+(-(x,s(0)),y)))
= t3

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