Certification Problem

Input (COPS 740)

We consider the TRS containing the following rules:

f(a,f(x,a))

→

f(a,f(f(a,a),a))

(1)

The underlying signature is as follows:

{f/2, a/0}

Prove or disprove confluence.

Yes.

Confluence is proven since the TRS is development closed. The joins can be performed using 1 development step(s).