Certification Problem
Input (COPS 167)
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 2022)
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(x86),g(x85)) |
→ |
f(x85,x86) |
(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).
-
↦ 1
-
↦ 7
-
↦ 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(x86),g(x85)) |
→ |
f(x85,x86) |
(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(x86),g(x85))←→ε f(x85,x86) = t can be joined as follows.
s
↔ f(x86,x85) ↔
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(x86),h(x85))←→ε f(x85,x86) = 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(x85),h(x86))←→ε f(x85,x86) = t can be joined as follows.
s
↔
t
-
The critical peak s = f(x448,x447)←→ε f(h(x448),h(x447)) = t can be joined as follows.
s
↔ f(x447,x448) ↔
t
-
The critical peak s = f(x449,x450)←→ε f(h(x450),g(x449)) = t can be joined as follows.
s
↔ f(x449,x450) ↔
t
-
The critical peak s = f(x452,x451)←→ε f(g(x452),h(x451)) = t can be joined as follows.
s
↔ f(x452,x451) ↔
t
-
The critical peak s = f(x453,x454)←→ε f(g(x454),g(x453)) = t can be joined as follows.
s
↔ f(x454,x453) ↔
t
-
The critical peak s = f(x456,x455)←→ε f(g(x456),h(x455)) = t can be joined as follows.
s
↔ f(x456,x455) ↔
t
-
The critical peak s = f(x458,x457)←→ε f(g(x458),h(x457)) = t can be joined as follows.
s
↔ f(x458,x457) ↔
t
/>