Certification Problem

Input (COPS 1104)

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

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

and S contains the following rules:

g(f(a)) f(g(f(a))) (4)
g(f(a)) f(f(a)) (5)
f(f(a)) f(a) (6)

The underlying signature is as follows:

{a/0, b/0, c/0, f/1, g/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).