YES
Confluence Proof
Confluence Proof
by csi
Input
The rewrite relation of the following TRS is considered.
|
a(b(x)) |
→ |
C(x) |
|
b(c(x)) |
→ |
A(x) |
|
c(a(x)) |
→ |
B(x) |
|
A(C(x)) |
→ |
b(x) |
|
C(B(x)) |
→ |
a(x) |
|
B(A(x)) |
→ |
c(x) |
|
a(a(a(a(x)))) |
→ |
A(A(A(x))) |
|
A(A(A(A(x)))) |
→ |
a(a(a(x))) |
|
b(b(b(b(x)))) |
→ |
B(B(B(x))) |
|
B(B(B(B(x)))) |
→ |
b(b(b(x))) |
|
c(c(c(c(x)))) |
→ |
C(C(C(x))) |
|
C(C(C(C(x)))) |
→ |
c(c(c(x))) |
|
B(a(a(a(x)))) |
→ |
c(A(A(A(x)))) |
|
A(A(A(b(x)))) |
→ |
a(a(a(C(x)))) |
|
C(b(b(b(x)))) |
→ |
a(B(B(B(x)))) |
|
B(B(B(c(x)))) |
→ |
b(b(b(A(x)))) |
|
A(c(c(c(x)))) |
→ |
b(C(C(C(x)))) |
|
C(C(C(a(x)))) |
→ |
c(c(c(B(x)))) |
|
a(A(x)) |
→ |
x |
|
A(a(x)) |
→ |
x |
|
b(B(x)) |
→ |
x |
|
B(b(x)) |
→ |
x |
|
c(C(x)) |
→ |
x |
|
C(c(x)) |
→ |
x |
Proof
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 |
the
rules
|
B(a(a(a(x)))) |
→ |
c(A(A(A(x)))) |
|
A(A(A(b(x)))) |
→ |
a(a(a(C(x)))) |
|
C(b(b(b(x)))) |
→ |
a(B(B(B(x)))) |
|
B(B(B(c(x)))) |
→ |
b(b(b(A(x)))) |
|
A(c(c(c(x)))) |
→ |
b(C(C(C(x)))) |
|
C(C(C(a(x)))) |
→ |
c(c(c(B(x)))) |
remain.
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 rules could be removed.
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.
Tool configuration
csi
- version: csi 1.2.5 [hg: unknown]
- strategy:
(cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!