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 2021)

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 Parallel Closed

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