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

1 Non-Joinable Fork

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

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

t0 = min(s(x97),s(x97))
s(x97)
= t1

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