Certification Problem

Input (COPS 630)

We consider the TRS containing the following rules:

min(0,y) 0 (1)
min(x,0) 0 (2)
min(s(x),s(y)) min(x,y) (3)
min(x,x) x (4)

The underlying signature is as follows:

{min/2, 0/0, s/1}

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 = min(s(c_1),s(c_1))
s(c_1)
= t1

t0 = min(s(c_1),s(c_1))
min(c_1,c_1)
c_1
= t2

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