Certification Problem
Input (COPS 68)
We consider the TRS containing the following rules:
|
b(w(x)) |
→ |
w(w(w(b(x)))) |
(1) |
|
w(b(x)) |
→ |
b(x) |
(2) |
|
b(b(x)) |
→ |
w(w(w(w(x)))) |
(3) |
|
w(w(x)) |
→ |
w(x) |
(4) |
The underlying signature is as follows:
{b/1, w/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2023)
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).
-
|
b(w(x)) |
→ |
w(w(w(b(x)))) |
(1) |
↦ 1
-
↦ 0
-
|
b(b(x)) |
→ |
w(w(w(w(x)))) |
(3) |
↦ 1
-
↦ 0
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 = w(w(w(w(b(x33)))))←→ε b(w(x33)) = t can be joined as follows.
s
↔ w(w(w(b(x33)))) ↔
t
-
The critical peak s = b(w(w(w(b(x34)))))←→ε w(w(w(w(w(x34))))) = t can be joined as follows.
s
↔ b(w(w(b(x34)))) ↔ b(w(b(x34))) ↔ b(b(x34)) ↔ w(w(w(w(x34)))) ↔
t
-
The critical peak s = b(b(x35))←→ε w(w(w(b(b(x35))))) = t can be joined as follows.
s
↔ b(b(x35)) ↔ w(b(b(x35))) ↔ w(w(b(b(x35)))) ↔
t
-
The critical peak s = w(b(x36))←→ε w(b(x36)) = t can be joined as follows.
s
↔
t
-
The critical peak s = w(w(w(w(w(x37)))))←→ε b(b(x37)) = t can be joined as follows.
s
↔ w(w(w(w(x37)))) ↔
t
-
The critical peak s = b(w(w(w(w(x38)))))←→ε w(w(w(w(b(x38))))) = t can be joined as follows.
s
↔ b(w(w(w(x38)))) ↔ b(w(w(x38))) ↔ b(w(x38)) ↔ w(w(w(b(x38)))) ↔
t
-
The critical peak s = b(w(x39))←→ε w(w(w(b(w(x39))))) = t can be joined as follows.
s
↔ b(w(x39)) ↔ w(b(w(x39))) ↔ w(w(b(w(x39)))) ↔
t
-
The critical peak s = w(w(x40))←→ε w(w(x40)) = t can be joined as follows.
s
↔
t
/>