Certification Problem

Input (COPS 1107)

We consider two TRSs R and S where R contains the rules

a → b (1)
a → f(a) (2)
b → f(f(b)) (3)
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → b (4)

and S contains the following rules:

a1 → b1 (5)
a1 → c1 (6)
b1 → b2 (7)
c1 → c2 (8)
a2 → b2 (9)
a2 → c2 (10)
b2 → b3 (11)
c2 → c3 (12)
a3 → b3 (13)
a3 → c3 (14)
b3 → b4 (15)
c3 → c4 (16)
a4 → b4 (17)
a4 → c4 (18)
b4 → b5 (19)
c4 → c5 (20)
a5 → b6 (21)
b5 → b6 (22)
c5 → b6 (23)

The underlying signature is as follows:

{a/0, b/0, f/1, a1/0, a2/0, a3/0, a4/0, a5/0, b1/0, b2/0, b3/0, b4/0, b5/0, b6/0, c1/0, c2/0, c3/0, c4/0, c5/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).