Certification Problem

Input (COPS 78)

We consider the TRS containing the following rules:

join(x,meet(x,y)) x (1)
meet(x,joint(y,z)) join(meet(x,y),meet(x,z)) (2)
meet(x,x) x (3)
join(x,x) x (4)
meet(meet(x,y),z) meet(x,meet(y,z)) (5)
meet(x,y) meet(y,x) (6)
join(join(x,y),z) join(x,join(y,z)) (7)
join(x,y) join(y,x) (8)

The underlying signature is as follows:

{join/2, meet/2, joint/2}

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:

join(x,meet(x,y)) x (1)
meet(x,joint(y,z)) join(meet(x,y),meet(x,z)) (2)
meet(x,x) x (3)
join(x,x) x (4)
meet(meet(x,y),z) meet(x,meet(y,z)) (5)
meet(x,y) meet(y,x) (6)
join(join(x,y),z) join(x,join(y,z)) (7)
join(x,y) join(y,x) (8)
meet(y,x) meet(y,x) (9)
join(meet(x,y),x) x (10)
join(y,x) join(y,x) (11)
join(y,meet(x,y)) y (12)
join(meet(y,x282),y) y (13)
meet(meet(x,x),x) x (14)
meet(x,meet(x,x)) x (15)
meet(join(x,x),x) x (16)
meet(x,join(x,x)) x (17)
join(meet(x,x),x) x (18)
join(x,meet(x,x)) x (19)
join(join(x,x),x) x (20)
join(x,join(x,x)) x (21)
meet(x,y) meet(x,y) (22)
join(x,y) join(x,y) (23)

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 = join(joint(f25,f26),meet(f3,joint(f25,f26)))
join(joint(f25,f26),join(meet(f3,f25),meet(f3,f26)))
= t1

t0 = join(joint(f25,f26),meet(f3,joint(f25,f26)))
joint(f25,f26)
= t1

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