Certification Problem

Input (COPS 73)

We consider the TRS containing the following rules:

f(g(g(x))) → a (1)
f(g(h(x))) → b (2)
f(h(g(x))) → b (3)
f(h(h(x))) → c (4)
g(x) → h(x) (5)
a → b (6)
b → c (7)

The underlying signature is as follows:

{f/1, g/1, a/0, h/1, b/0, c/0}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2022)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

b → c (7)
a → b (6)
g(x) → h(x) (5)
f(h(h(x))) → c (4)
f(h(g(x))) → b (3)
f(g(h(x))) → b (2)
f(g(g(x))) → a (1)
a → c (8)
f(h(g(x))) → c (9)
f(g(h(x))) → c (10)
f(g(g(x))) → b (11)

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Strongly closed

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