Certification Problem

Input (COPS 74)

We consider the TRS containing the following rules:

a c (1)
b c (2)
f(a,b) d (3)
f(x,c) f(c,c) (4)
f(c,x) f(c,c) (5)
d f(a,c) (6)
d f(c,b) (7)

The underlying signature is as follows:

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

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ACP @ CoCo 2021)

1 Strongly closed

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