Certification Problem
Input (COPS 962)
We consider the TRS containing the following rules:
|
a(b(x)) |
→ |
C(x) |
(1) |
|
b(c(x)) |
→ |
A(x) |
(2) |
|
c(a(x)) |
→ |
B(x) |
(3) |
|
A(C(x)) |
→ |
b(x) |
(4) |
|
C(B(x)) |
→ |
a(x) |
(5) |
|
B(A(x)) |
→ |
c(x) |
(6) |
|
a(a(a(a(x)))) |
→ |
A(A(A(x))) |
(7) |
|
A(A(A(A(x)))) |
→ |
a(a(a(x))) |
(8) |
|
b(b(b(b(x)))) |
→ |
B(B(B(x))) |
(9) |
|
B(B(B(B(x)))) |
→ |
b(b(b(x))) |
(10) |
|
c(c(c(c(x)))) |
→ |
C(C(C(x))) |
(11) |
|
C(C(C(C(x)))) |
→ |
c(c(c(x))) |
(12) |
|
B(a(a(a(x)))) |
→ |
c(A(A(A(x)))) |
(13) |
|
A(A(A(b(x)))) |
→ |
a(a(a(C(x)))) |
(14) |
|
C(b(b(b(x)))) |
→ |
a(B(B(B(x)))) |
(15) |
|
B(B(B(c(x)))) |
→ |
b(b(b(A(x)))) |
(16) |
|
A(c(c(c(x)))) |
→ |
b(C(C(C(x)))) |
(17) |
|
C(C(C(a(x)))) |
→ |
c(c(c(B(x)))) |
(18) |
|
a(A(x)) |
→ |
x |
(19) |
|
A(a(x)) |
→ |
x |
(20) |
|
b(B(x)) |
→ |
x |
(21) |
|
B(b(x)) |
→ |
x |
(22) |
|
c(C(x)) |
→ |
x |
(23) |
|
C(c(x)) |
→ |
x |
(24) |
The underlying signature is as follows:
{a/1, b/1, C/1, c/1, A/1, B/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2023)
1 Locally confluent and terminating
Confluence is proven by showing local confluence and termination.
1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [A(x1)] |
= |
2 · x1 + 1 |
| [a(x1)] |
= |
2 · x1 + 1 |
| [c(x1)] |
= |
2 · x1 + 1 |
| [B(x1)] |
= |
2 · x1 + 1 |
| [b(x1)] |
= |
2 · x1 + 1 |
| [C(x1)] |
= |
2 · x1 + 1 |
all of the following rules can be deleted.
|
a(b(x)) |
→ |
C(x) |
(1) |
|
b(c(x)) |
→ |
A(x) |
(2) |
|
c(a(x)) |
→ |
B(x) |
(3) |
|
A(C(x)) |
→ |
b(x) |
(4) |
|
C(B(x)) |
→ |
a(x) |
(5) |
|
B(A(x)) |
→ |
c(x) |
(6) |
|
a(a(a(a(x)))) |
→ |
A(A(A(x))) |
(7) |
|
A(A(A(A(x)))) |
→ |
a(a(a(x))) |
(8) |
|
b(b(b(b(x)))) |
→ |
B(B(B(x))) |
(9) |
|
B(B(B(B(x)))) |
→ |
b(b(b(x))) |
(10) |
|
c(c(c(c(x)))) |
→ |
C(C(C(x))) |
(11) |
|
C(C(C(C(x)))) |
→ |
c(c(c(x))) |
(12) |
|
a(A(x)) |
→ |
x |
(19) |
|
A(a(x)) |
→ |
x |
(20) |
|
b(B(x)) |
→ |
x |
(21) |
|
B(b(x)) |
→ |
x |
(22) |
|
c(C(x)) |
→ |
x |
(23) |
|
C(c(x)) |
→ |
x |
(24) |
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [A(x1)] |
= |
2 · x1 + 0 |
| [a(x1)] |
= |
2 · x1 + 2 |
| [c(x1)] |
= |
2 · x1 + 2 |
| [B(x1)] |
= |
2 · x1 + 0 |
| [b(x1)] |
= |
2 · x1 + 2 |
| [C(x1)] |
= |
2 · x1 + 0 |
all of the following rules can be deleted.
|
B(a(a(a(x)))) |
→ |
c(A(A(A(x)))) |
(13) |
|
A(A(A(b(x)))) |
→ |
a(a(a(C(x)))) |
(14) |
|
C(b(b(b(x)))) |
→ |
a(B(B(B(x)))) |
(15) |
|
B(B(B(c(x)))) |
→ |
b(b(b(A(x)))) |
(16) |
|
A(c(c(c(x)))) |
→ |
b(C(C(C(x)))) |
(17) |
|
C(C(C(a(x)))) |
→ |
c(c(c(B(x)))) |
(18) |
1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.2 Local Confluence Proof
All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.