Certification Problem

Input (COPS 1102)

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

b c (1)
h(b,b) a (2)
h(c,c) c (3)
c c (4)

and S contains the following rules:

f(a) b (5)
f(a) f(c) (6)
a d (7)
f(d) b (8)
f(c) b (9)
d c (10)

The underlying signature is as follows:

{a/0, b/0, c/0, d/0, f/1, h/2}

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