Certification Problem

Input (COPS 121)

We consider the TRS containing the following rules:

f(g(x),g(y))	→	f(g(x),h(y))	(1)
f(h(x),g(y))	→	f(g(x),g(y))	(2)
f(g(x),h(y))	→	f(x,y)	(3)
f(h(x),h(y))	→	f(y,x)	(4)
f(x,y)	→	f(y,x)	(5)
g(x)	→	h(x)	(6)
h(x)	→	g(x)	(7)

The underlying signature is as follows:

{f/2, g/1, h/1}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2021)

1 Decreasing Diagrams

1.2 Rule Labeling

Confluence is proven, because all critical peaks can be joined decreasingly using the following rule labeling function (rules that are not shown have label 0).

f(g(x),g(y)) → f(g(x),h(y)) (1)
↦ 0
f(h(x),g(y)) → f(g(x),g(y)) (2)
↦ 4
f(g(x),h(y)) → f(x,y) (3)
↦ 2
f(h(x),h(y)) → f(y,x) (4)
↦ 1
f(x,y) → f(y,x) (5)
↦ 0
g(x) → h(x) (6)
↦ 0
h(x) → g(x) (7)
↦ 4

The critical pairs can be joined as follows. Here, ↔ is always chosen as an appropriate rewrite relation which is automatically inferred by the certifier.

The critical peak s = f(g(x182),h(x183))←→_ε f(g(x183),g(x182)) = t can be joined as follows.
s ↔ f(h(x183),g(x182)) ↔ t
The critical peak s = f(g(x182),h(x183))←→_ε f(g(x183),g(x182)) = t can be joined as follows.
s ↔ f(g(x182),g(x183)) ↔ t
The critical peak s = f(g(x184),g(x185))←→_ε f(g(x185),h(x184)) = t can be joined as follows.
s ↔ f(g(x185),g(x184)) ↔ t
The critical peak s = f(g(x184),g(x185))←→_ε f(g(x185),h(x184)) = t can be joined as follows.
s ↔ f(h(x184),g(x185)) ↔ t
The critical peak s = f(x186,x187)←→_ε f(h(x187),g(x186)) = t can be joined as follows.
s ↔ f(x186,x187) ↔ f(g(x186),h(x187)) ↔ t
The critical peak s = f(x186,x187)←→_ε f(h(x187),g(x186)) = t can be joined as follows.
s ↔ f(x186,x187) ↔ f(h(x187),h(x186)) ↔ t
The critical peak s = f(x189,x188)←→_ε f(h(x189),h(x188)) = t can be joined as follows.
s ↔ f(x188,x189) ↔ t
The critical peak s = f(g(y),g(x))←→_ε f(g(x),h(y)) = t can be joined as follows.
s ↔ f(g(x),g(y)) ↔ t
The critical peak s = f(g(y),g(x))←→_ε f(g(x),h(y)) = t can be joined as follows.
s ↔ f(h(y),g(x)) ↔ t
The critical peak s = f(g(y),h(x))←→_ε f(g(x),g(y)) = t can be joined as follows.
s ↔ f(h(x),g(y)) ↔ t
The critical peak s = f(g(y),h(x))←→_ε f(g(x),g(y)) = t can be joined as follows.
s ↔ f(g(y),g(x)) ↔ t
The critical peak s = f(h(y),g(x))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(g(x),h(y)) ↔ t
The critical peak s = f(h(y),g(x))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(h(y),h(x)) ↔ t
The critical peak s = f(h(y),h(x))←→_ε f(y,x) = t can be joined as follows.
s ↔ f(x,y) ↔ t
The critical peak s = f(h(x),g(y))←→_ε f(g(x),h(y)) = t can be joined as follows.
s ↔ f(g(x),g(y)) ↔ t
The critical peak s = f(h(x),g(y))←→_ε f(g(x),h(y)) = t can be joined as follows.
s ↔ f(h(x),h(y)) ↔ t
The critical peak s = f(g(x),h(y))←→_ε f(g(x),h(y)) = t can be joined as follows.
s ↔ t
The critical peak s = f(h(x),h(y))←→_ε f(g(x),g(y)) = t can be joined as follows.
s ↔ f(h(x),g(y)) ↔ t
The critical peak s = f(h(x),h(y))←→_ε f(g(x),g(y)) = t can be joined as follows.
s ↔ f(g(x),h(y)) ↔ t
The critical peak s = f(h(x),h(y))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(y,x) ↔ t
The critical peak s = f(g(x),g(y))←→_ε f(g(x),g(y)) = t can be joined as follows.
s ↔ t
The critical peak s = f(g(x),g(y))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(g(x),h(y)) ↔ t
The critical peak s = f(g(x),h(y))←→_ε f(y,x) = t can be joined as follows.
s ↔ f(x,y) ↔ t
The critical peak s = f(h(x),g(y))←→_ε f(y,x) = t can be joined as follows.
s ↔ f(g(y),h(x)) ↔ t
The critical peak s = f(h(x),g(y))←→_ε f(y,x) = t can be joined as follows.
s ↔ f(h(x),h(y)) ↔ t