YES
Confluence Proof
Confluence Proof
by csi
Input
The rewrite relation of the following TRS is considered.
|
C(x) |
→ |
c(x) |
|
c(c(x)) |
→ |
x |
|
b(b(x)) |
→ |
B(x) |
|
B(B(x)) |
→ |
b(x) |
|
c(B(c(b(c(x))))) |
→ |
B(c(b(c(B(c(b(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
| [c(x1)] |
= |
2 · x1 + 1 |
| [B(x1)] |
= |
1 · x1 + 0 |
| [C(x1)] |
= |
2 · x1 + 1 |
| [b(x1)] |
= |
1 · x1 + 0 |
the
rules
|
C(x) |
→ |
c(x) |
|
b(b(x)) |
→ |
B(x) |
|
B(B(x)) |
→ |
b(x) |
|
c(B(c(b(c(x))))) |
→ |
B(c(b(c(B(c(b(x))))))) |
|
b(B(x)) |
→ |
x |
|
B(b(x)) |
→ |
x |
remain.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [c(x1)] |
= |
1 · x1 + 0 |
| [B(x1)] |
= |
1 · x1 + 0 |
| [C(x1)] |
= |
2 · x1 + 4 |
| [b(x1)] |
= |
1 · x1 + 0 |
the
rules
|
b(b(x)) |
→ |
B(x) |
|
B(B(x)) |
→ |
b(x) |
|
c(B(c(b(c(x))))) |
→ |
B(c(b(c(B(c(b(x))))))) |
|
b(B(x)) |
→ |
x |
|
B(b(x)) |
→ |
x |
remain.
1.1.1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
|
b(b(x)) |
→ |
B(x) |
|
B(B(x)) |
→ |
b(x) |
|
c(b(c(B(c(x))))) |
→ |
b(c(B(c(b(c(B(x))))))) |
|
B(b(x)) |
→ |
x |
|
b(B(x)) |
→ |
x |
1.1.1.1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
b#(b(x)) |
→ |
B#(x) |
|
B#(B(x)) |
→ |
b#(x) |
|
c#(b(c(B(c(x))))) |
→ |
B#(x) |
|
c#(b(c(B(c(x))))) |
→ |
c#(B(x)) |
|
c#(b(c(B(c(x))))) |
→ |
b#(c(B(x))) |
|
c#(b(c(B(c(x))))) |
→ |
c#(b(c(B(x)))) |
|
c#(b(c(B(c(x))))) |
→ |
B#(c(b(c(B(x))))) |
|
c#(b(c(B(c(x))))) |
→ |
c#(B(c(b(c(B(x)))))) |
|
c#(b(c(B(c(x))))) |
→ |
b#(c(B(c(b(c(B(x))))))) |
1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 2
components.
-
The
1st
component contains the
pairs
|
c#(b(c(B(c(x))))) |
→ |
c#(B(c(b(c(B(x)))))) |
|
c#(b(c(B(c(x))))) |
→ |
c#(B(x)) |
|
c#(b(c(B(c(x))))) |
→ |
c#(b(c(B(x)))) |
1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules
Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(c#) |
= |
3 |
|
weight(c#) |
= |
1 |
|
|
|
| prec(B) |
= |
2 |
|
weight(B) |
= |
1 |
|
|
|
| prec(b) |
= |
1 |
|
weight(b) |
= |
1 |
|
|
|
| prec(c) |
= |
0 |
|
weight(c) |
= |
1 |
|
|
|
in combination with the following argument filter
| π(c#) |
= |
1 |
| π(B) |
= |
1 |
| π(b) |
= |
1 |
| π(c) |
= |
[1] |
together with the usable
rules
|
b(b(x)) |
→ |
B(x) |
|
B(B(x)) |
→ |
b(x) |
|
c(b(c(B(c(x))))) |
→ |
b(c(B(c(b(c(B(x))))))) |
|
B(b(x)) |
→ |
x |
|
b(B(x)) |
→ |
x |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
|
c#(b(c(B(c(x))))) |
→ |
c#(B(c(b(c(B(x)))))) |
remains.
1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1
over the arctic semiring over the integers
| [c(x1)] |
= |
· x1 +
|
| [B(x1)] |
= |
· x1 +
|
| [c#(x1)] |
= |
· x1 +
|
| [b(x1)] |
= |
· x1 +
|
together with the usable
rules
|
b(b(x)) |
→ |
B(x) |
|
B(B(x)) |
→ |
b(x) |
|
c(b(c(B(c(x))))) |
→ |
b(c(B(c(b(c(B(x))))))) |
|
B(b(x)) |
→ |
x |
|
b(B(x)) |
→ |
x |
(w.r.t. the implicit argument filter of the reduction pair),
all pairs could be removed.
1.1.1.1.1.1.1.1.1 P is empty
There are no pairs anymore.
-
The
2nd
component contains the
pairs
|
B#(B(x)) |
→ |
b#(x) |
|
b#(b(x)) |
→ |
B#(x) |
1.1.1.1.1.1.2 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
As there is no critical graph in the transitive closure, there are no infinite chains.
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])!)))))!