Certification Problem

Input (COPS 497)

We consider the TRS containing the following rules:

d(x,x) 0 (1)
f(x) d(x,f(x)) (2)
c f(c) (3)

The underlying signature is as follows:

{d/2, 0/0, f/1, c/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2022)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

d(x,x) 0 (1)
f(x) d(x,f(x)) (2)
c f(c) (3)
f(c) d(f(c),f(c)) (4)
f(c) d(c,f(f(c))) (5)
c d(c,f(c)) (6)
c f(f(c)) (7)
d(d(x,x),0) 0 (8)
d(0,d(x,x)) 0 (9)
d(c,f(c)) 0 (10)
d(f(c),c) 0 (11)

All redundant rules that were added or removed can be simulated in 3 steps .

1.1 Non-Joinable Fork

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

t0 = f(c)
f(d(c,f(c)))
f(0)
= t2

t0 = f(c)
d(f(c),f(c))
0
= t2

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