Certification Problem

Input (COPS 1113)

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

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

and S contains the following rules:

-(+(x,-(x))) → 0 (3)
+(x,-(x)) → 0 (4)
0 → -(0) (5)

The underlying signature is as follows:

{+/2, -/1, 0/0, a/0, b/0, c/0, f/1, h/2, x/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).