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: