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 2021)

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 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)
f(c) → 0 (12)
c → d(f(c),f(c)) (13)
c → d(c,f(f(c))) (14)
c → f(d(c,f(c))) (15)
c → f(f(f(c))) (16)
c → d(c,d(c,f(c))) (17)
c → d(f(f(c)),f(c)) (18)
c → d(c,f(f(f(c)))) (19)
c → 0 (20)
c → d(f(c),f(f(c))) (21)
c → f(d(f(c),f(c))) (22)
c → f(d(c,f(f(c)))) (23)
c → f(f(d(c,f(c)))) (24)
c → f(f(f(f(c)))) (25)
d(c,d(c,f(c))) → 0 (26)
d(d(c,f(c)),c) → 0 (27)
d(c,f(f(c))) → 0 (28)
d(f(f(c)),c) → 0 (29)
d(d(c,f(c)),0) → 0 (30)
d(0,d(c,f(c))) → 0 (31)
d(d(f(c),c),0) → 0 (32)
d(0,d(f(c),c)) → 0 (33)
d(f(c),0) → 0 (34)
d(0,f(c)) → 0 (35)
d(c,c) → 0 (36)

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

1.1.1 Non-Joinable Fork

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

t0 = f(c)
→ f(0)
= t1

t0 = f(c)
→ 0
= t1

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