Certification Problem

Input (COPS 115)

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 b5 (17)
a5 c5 (18)
b5 b6 (19)
c5 c6 (20)
a6 b6 (21)
a6 c6 (22)
b6 b7 (23)
c6 c7 (24)
a7 b7 (25)
a7 c7 (26)
b7 b8 (27)
c7 c8 (28)
a8 b8 (29)
a8 c8 (30)
b8 b9 (31)
c8 c9 (32)
a9 b9 (33)
a9 c9 (34)
b9 b10 (35)
c9 c10 (36)
a10 b11 (37)
b10 b11 (38)
c10 b11 (39)

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, c6/0, a6/0, b7/0, c7/0, a7/0, b8/0, c8/0, a8/0, b9/0, c9/0, a9/0, b10/0, c10/0, a10/0, b11/0}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

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:

c10 b11 (39)
b10 b11 (38)
a10 b11 (37)
c9 c10 (36)
b9 b10 (35)
a9 c9 (34)
a9 b9 (33)
c8 c9 (32)
b8 b9 (31)
a8 c8 (30)
a8 b8 (29)
c7 c8 (28)
b7 b8 (27)
a7 c7 (26)
a7 b7 (25)
c6 c7 (24)
b6 b7 (23)
a6 c6 (22)
a6 b6 (21)
c5 c6 (20)
b5 b6 (19)
a5 c5 (18)
a5 b5 (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 b11 (40)
c1 b11 (41)
b2 b11 (42)
c2 b11 (43)
b3 b11 (44)
c3 b11 (45)
b4 b11 (46)
c4 b11 (47)
b5 b11 (48)
c5 b11 (49)
b6 b11 (50)
c6 b11 (51)
b7 b11 (52)
c7 b11 (53)
b8 b11 (54)
c8 b11 (55)
b9 b11 (56)
c9 b11 (57)

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

1.1 Strongly closed

Confluence is proven since the TRS is strongly closed. The joins can be performed using 7 step(s).