Certification Problem
Input (COPS 761)
We consider the TRS containing the following rules:
| a |
→ |
b |
(1) |
| a |
→ |
d |
(2) |
| b |
→ |
a |
(3) |
| c |
→ |
a |
(4) |
| c |
→ |
b |
(5) |
The underlying signature is as follows:
{a/0, b/0, d/0, c/0}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2021)
1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
| c |
→ |
b |
(5) |
| c |
→ |
a |
(4) |
| b |
→ |
a |
(3) |
| a |
→ |
d |
(2) |
| a |
→ |
b |
(1) |
| c |
→ |
d |
(6) |
| b |
→ |
d |
(7) |
| b |
→ |
b |
(8) |
| a |
→ |
a |
(9) |
All redundant rules that were added or removed can be
simulated in 2 steps
.
1.1 Decreasing Diagrams
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
-
↦ 1
-
↦ 1
-
↦ 0
-
↦ 1
-
↦ 1
-
↦ 0
-
↦ 0
-
↦ 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 = b←→ε a = t can be joined as follows.
s
↔ b ↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = b←→ε d = t can be joined as follows.
s
↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔ a ↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔
t
-
The critical peak s = a←→ε d = t can be joined as follows.
s
↔
t
-
The critical peak s = a←→ε d = t can be joined as follows.
s
↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔ a ↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔
t
-
The critical peak s = d←→ε b = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = d←→ε a = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = b←→ε d = t can be joined as follows.
s
↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔ b ↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = d←→ε b = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = d←→ε a = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = d←→ε a = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = d←→ε b = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔ b ↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔
t
-
The critical peak s = b←→ε a = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = b←→ε d = t can be joined as follows.
s
↔
t
-
The critical peak s = a←→ε d = t can be joined as follows.
s
↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔ a ↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔ d ↔
t
-
The critical peak s = a←→ε b = t can be joined as follows.
s
↔
t
/>