Certification Problem

Input (COPS 116)

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 b7 (24)
b7 b1 (25)
b7 c1 (26)

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}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2023)

1 Strongly closed

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