Certification Problem

Input (COPS 216)

We consider the TRS containing the following rules:

f(u(O),u(y)) A (1)
f(v(x),v(O)) B (2)
O u(O) (3)
O v(O) (4)
u(x) x (5)
v(x) x (6)
f(x,y) f(x,u(y)) (7)
f(x,y) f(v(x),y) (8)

The underlying signature is as follows:

{f/2, u/1, O/0, A/0, v/1, B/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:

f(u(O),u(y)) A (1)
f(v(x),v(O)) B (2)
O u(O) (3)
O v(O) (4)
u(x) x (5)
v(x) x (6)
f(x,y) f(x,u(y)) (7)
f(x,y) f(v(x),y) (8)
O u(u(O)) (9)
O u(v(O)) (10)
O O (11)
O v(u(O)) (12)
O v(v(O)) (13)
u(f(u(O),u(y))) A (14)
u(f(v(x),v(O))) B (15)
u(O) u(O) (16)
u(O) v(O) (17)
u(u(x)) x (18)
u(v(x)) x (19)
v(f(u(O),u(y))) A (20)
v(f(v(x),v(O))) B (21)
v(O) u(O) (22)
v(O) v(O) (23)
v(u(x)) x (24)
v(v(x)) x (25)
f(u(O),y) A (26)
f(x146,x) f(x146,x) (27)
f(x,v(O)) B (28)
f(x,x149) f(x,x149) (29)
f(O,u(x134)) A (30)
f(u(O),O) A (31)
f(u(O),u(O)) A (32)
u(f(u(O),u(x134))) A (33)
f(u(u(O)),u(x134)) A (34)
f(u(O),u(u(x134))) A (35)
f(u(O),u(u(x))) A (36)
v(f(u(O),u(x134))) A (37)
f(v(u(O)),u(x134)) A (38)
f(u(v(O)),u(x134)) A (39)
f(u(O),v(u(x134))) A (40)
f(u(O),u(v(x))) A (41)
f(v(O),v(O)) B (42)
f(O,v(O)) B (43)
f(v(x135),O) B (44)
u(f(v(x135),v(O))) B (45)
f(u(v(x135)),v(O)) B (46)
f(v(u(x)),v(O)) B (47)
f(v(x135),u(v(O))) B (48)
f(v(x135),v(u(O))) B (49)
v(f(v(x135),v(O))) B (50)
f(v(v(x135)),v(O)) B (51)
f(v(v(x)),v(O)) B (52)
f(v(x135),v(v(O))) B (53)
u(u(x136)) x136 (54)
v(u(x136)) x136 (55)
u(v(x137)) x137 (56)
v(v(x137)) x137 (57)

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(u(O),v(O))
A
= t1

t0 = f(u(O),v(O))
B
= t1

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