Certification Problem

Input (COPS 1106)

We consider two TRSs R and S where R contains the 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)

and S contains the following rules:

a b (40)
a c (41)
a e (42)
b d (43)
c a (44)
d a (45)
d e (46)
g(x) h(a) (47)
h(x) e (48)

The underlying signature is as follows:

{a/0, b/0, c/0, d/0, e/0, g/1, h/1, a1/0, a2/0, a3/0, a4/0, a5/0, a6/0, a7/0, a8/0, a9/0, b1/0, b2/0, b3/0, b4/0, b5/0, b6/0, b7/0, b8/0, b9/0, c1/0, c2/0, c3/0, c4/0, c5/0, c6/0, c7/0, c8/0, c9/0, a10/0, b10/0, b11/0, c10/0}

Property / Task

Prove or disprove commutation.

Answer / Result

Yes.

Proof (by ACP @ CoCo 2023)

1 Development Closed

Commutation is proven since the TRSs are development closed. The joins can be performed using 5 step(s).