Certification Problem

Input (COPS 1155)

We consider the TRS containing the following rules:

plus(x,0) x (1)
plus(0,1) 1 (2)
plus(x,plus(y,1)) plus(plus(x,y),1) (3)
times(x,0) 0 (4)
times(x,1) x (5)
times(x,plus(y,1)) plus(times(x,y),x) (6)
m(0) 0 (7)
plus(m(1),1) 0 (8)
plus(m(plus(x,1)),1) m(x) (9)
m(m(x)) x (10)
plus(x,m(y)) m(plus(m(x),y)) (11)
times(x,m(y)) m(times(x,y)) (12)

The underlying signature is as follows:

{plus/2, 0/0, 1/0, times/2, m/1}

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 = times(x,plus(0,1))
times(x,1)
x
= t2

t0 = times(x,plus(0,1))
plus(times(x,0),x)
plus(0,x)
= t2

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