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