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 2020)

1 Redundant Rules Transformation

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

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

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

1.1 Redundant Rules Transformation

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

h(x)	→	g(x)	(7)
g(x)	→	h(x)	(6)
f(x,y)	→	f(y,x)	(5)
f(h(x),h(y))	→	f(y,x)	(4)
f(g(x),h(y))	→	f(x,y)	(3)
f(h(y),g(x))	→	f(x,y)	(8)
f(g(x),g(y))	→	f(x,y)	(9)
f(h(x),g(y))	→	f(y,x)	(10)
f(h(x85),g(x84))	→	f(x84,x85)	(11)

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

1.1.1 Decreasing Diagrams

1.1.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).

h(x) → g(x) (7)
↦ 1
g(x) → h(x) (6)
↦ 7
f(x,y) → f(y,x) (5)
↦ 0
f(h(x),h(y)) → f(y,x) (4)
↦ 3
f(g(x),h(y)) → f(x,y) (3)
↦ 2
f(h(y),g(x)) → f(x,y) (8)
↦ 2
f(g(x),g(y)) → f(x,y) (9)
↦ 0
f(h(x),g(y)) → f(y,x) (10)
↦ 9
f(h(x85),g(x84)) → f(x84,x85) (11)
↦ 9

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(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 ↔ t
The critical peak s = f(g(x),g(y))←→_ε f(x,y) = t can be joined as follows.
s ↔ t
The critical peak s = f(g(y),g(x))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(y,x) ↔ t
The critical peak s = f(g(x),g(y))←→_ε f(y,x) = t can be joined as follows.
s ↔ f(x,y) ↔ t
The critical peak s = f(g(x85),g(x84))←→_ε f(x84,x85) = t can be joined as follows.
s ↔ f(x85,x84) ↔ 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(h(y),h(x))←→_ε f(x,y) = t can be joined as follows.
s ↔ t
The critical peak s = f(h(x),g(y))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(y,x) ↔ t
The critical peak s = f(g(x),h(y))←→_ε f(x,y) = t can be joined as follows.
s ↔ t
The critical peak s = f(h(x),h(y))←→_ε f(y,x) = t can be joined as follows.
s ↔ t
The critical peak s = f(h(x85),h(x84))←→_ε f(x84,x85) = t can be joined as follows.
s ↔ 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(y),g(x))←→_ε f(x,y) = t can be joined as follows.
s ↔ t
The critical peak s = f(g(x),h(y))←→_ε f(x,y) = t can be joined as follows.
s ↔ t
The critical peak s = f(g(y),g(x))←→_ε f(x,y) = t can be joined as follows.
s ↔ f(y,x) ↔ t
The critical peak s = f(g(y),h(x))←→_ε f(y,x) = t can be joined as follows.
s ↔ t
The critical peak s = f(g(x84),h(x85))←→_ε f(x84,x85) = t can be joined as follows.
s ↔ t
The critical peak s = f(x447,x446)←→_ε f(h(x447),h(x446)) = t can be joined as follows.
s ↔ f(x446,x447) ↔ t
The critical peak s = f(x448,x449)←→_ε f(h(x449),g(x448)) = t can be joined as follows.
s ↔ f(x448,x449) ↔ t
The critical peak s = f(x451,x450)←→_ε f(g(x451),h(x450)) = t can be joined as follows.
s ↔ f(x451,x450) ↔ t
The critical peak s = f(x452,x453)←→_ε f(g(x453),g(x452)) = t can be joined as follows.
s ↔ f(x453,x452) ↔ t
The critical peak s = f(x455,x454)←→_ε f(g(x455),h(x454)) = t can be joined as follows.
s ↔ f(x455,x454) ↔ t
The critical peak s = f(x457,x456)←→_ε f(g(x457),h(x456)) = t can be joined as follows.
s ↔ f(x457,x456) ↔ t