Certification Problem

Input (COPS 114)

We consider the TRS containing the following rules:

a1 → b1 (1)
a1 → c1 (2)
b1 → b2 (3)
c1 → c2 (4)
a2 → b2 (5)
a2 → c2 (6)
b2 → b3 (7)
c2 → c3 (8)
a3 → b3 (9)
a3 → c3 (10)
b3 → b4 (11)
c3 → c4 (12)
a4 → b4 (13)
a4 → c4 (14)
b4 → b5 (15)
c4 → c5 (16)
a5 → b6 (17)
b5 → b6 (18)
c5 → b6 (19)

The underlying signature is as follows:

{a1/0, b1/0, c1/0, b2/0, c2/0, a2/0, b3/0, c3/0, a3/0, b4/0, c4/0, a4/0, b5/0, c5/0, a5/0, b6/0}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2020)

1 Redundant Rules Transformation

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

c5 → b6 (19)
b5 → b6 (18)
a5 → b6 (17)
c4 → c5 (16)
b4 → b5 (15)
a4 → c4 (14)
a4 → b4 (13)
c3 → c4 (12)
b3 → b4 (11)
a3 → c3 (10)
a3 → b3 (9)
c2 → c3 (8)
b2 → b3 (7)
a2 → c2 (6)
a2 → b2 (5)
c1 → c2 (4)
b1 → b2 (3)
a1 → c1 (2)
a1 → b1 (1)
b1 → b6 (20)
c1 → b6 (21)
b2 → b6 (22)
c2 → b6 (23)
b3 → b6 (24)
c3 → b6 (25)
b4 → b6 (26)
c4 → b6 (27)

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

1.1 Parallel Closed

Confluence is proven since the TRS is (almost) parallel closed. The joins can be performed using 1 parallel step(s).