The rewrite relation of the following TRS is considered.
[mark(x1)] |
= |
· x1 +
|
[cons(x1, x2)] |
= |
· x1 + · x2 +
|
[eq(x1, x2)] |
= |
· x1 + · x2 +
|
[true] |
= |
|
[s(x1)] |
= |
· x1 +
|
[nil] |
= |
|
[0] |
= |
|
[inf(x1)] |
= |
· x1 +
|
[length(x1)] |
= |
· x1 +
|
[take(x1, x2)] |
= |
· x1 + · x2 +
|
[false] |
= |
|
[active(x1)] |
= |
· x1 +
|
all of the following rules can be deleted.
[mark(x1)] |
= |
· x1 +
|
[cons(x1, x2)] |
= |
· x1 + · x2 +
|
[eq(x1, x2)] |
= |
· x1 + · x2 +
|
[true] |
= |
|
[s(x1)] |
= |
· x1 +
|
[nil] |
= |
|
[0] |
= |
|
[inf(x1)] |
= |
· x1 +
|
[length(x1)] |
= |
· x1 +
|
[take(x1, x2)] |
= |
· x1 + · x2 +
|
[false] |
= |
|
[active(x1)] |
= |
· x1 +
|
all of the following rules can be deleted.
[mark(x1)] |
= |
· x1 +
|
[cons(x1, x2)] |
= |
· x1 + · x2 +
|
[eq(x1, x2)] |
= |
· x1 + · x2 +
|
[true] |
= |
|
[s(x1)] |
= |
· x1 +
|
[nil] |
= |
|
[0] |
= |
|
[inf(x1)] |
= |
· x1 +
|
[length(x1)] |
= |
· x1 +
|
[take(x1, x2)] |
= |
· x1 + · x2 +
|
[false] |
= |
|
[active(x1)] |
= |
· x1 +
|
all of the following rules can be deleted.
The dependency pairs are split into 8
components.
-
The
1st
component contains the
pair
mark#(length(X)) |
→ |
mark#(X) |
(60) |
mark#(take(X1,X2)) |
→ |
mark#(X1) |
(56) |
mark#(take(X1,X2)) |
→ |
mark#(X2) |
(55) |
mark#(inf(X)) |
→ |
mark#(X) |
(51) |
1.1.1.1.1.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
mark#(length(X)) |
→ |
mark#(X) |
(60) |
|
1 |
> |
1 |
mark#(take(X1,X2)) |
→ |
mark#(X1) |
(56) |
|
1 |
> |
1 |
mark#(take(X1,X2)) |
→ |
mark#(X2) |
(55) |
|
1 |
> |
1 |
mark#(inf(X)) |
→ |
mark#(X) |
(51) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
2nd
component contains the
pair
mark#(eq(X1,X2)) |
→ |
active#(eq(X1,X2)) |
(46) |
active#(eq(s(X),s(Y))) |
→ |
mark#(eq(X,Y)) |
(38) |
1.1.1.1.1.2 Subterm Criterion Processor
We use the projection to multisets
π(mark#)
|
= |
{
1
}
|
π(active#)
|
= |
{
1
}
|
π(eq)
|
= |
{
2
}
|
to remove the pairs:
active#(eq(s(X),s(Y))) |
→ |
mark#(eq(X,Y)) |
(38) |
1.1.1.1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
3rd
component contains the
pair
eq#(X1,active(X2)) |
→ |
eq#(X1,X2) |
(66) |
eq#(active(X1),X2) |
→ |
eq#(X1,X2) |
(65) |
eq#(X1,mark(X2)) |
→ |
eq#(X1,X2) |
(64) |
eq#(mark(X1),X2) |
→ |
eq#(X1,X2) |
(63) |
1.1.1.1.1.3 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
eq#(X1,active(X2)) |
→ |
eq#(X1,X2) |
(66) |
|
2 |
> |
2 |
1 |
≥ |
1 |
eq#(active(X1),X2) |
→ |
eq#(X1,X2) |
(65) |
|
2 |
≥ |
2 |
1 |
> |
1 |
eq#(X1,mark(X2)) |
→ |
eq#(X1,X2) |
(64) |
|
2 |
> |
2 |
1 |
≥ |
1 |
eq#(mark(X1),X2) |
→ |
eq#(X1,X2) |
(63) |
|
2 |
≥ |
2 |
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
4th
component contains the
pair
s#(mark(X)) |
→ |
s#(X) |
(67) |
s#(active(X)) |
→ |
s#(X) |
(68) |
1.1.1.1.1.4 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
s#(mark(X)) |
→ |
s#(X) |
(67) |
|
1 |
> |
1 |
s#(active(X)) |
→ |
s#(X) |
(68) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
5th
component contains the
pair
inf#(mark(X)) |
→ |
inf#(X) |
(69) |
inf#(active(X)) |
→ |
inf#(X) |
(70) |
1.1.1.1.1.5 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
inf#(mark(X)) |
→ |
inf#(X) |
(69) |
|
1 |
> |
1 |
inf#(active(X)) |
→ |
inf#(X) |
(70) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
6th
component contains the
pair
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(71) |
cons#(X1,active(X2)) |
→ |
cons#(X1,X2) |
(74) |
cons#(active(X1),X2) |
→ |
cons#(X1,X2) |
(73) |
cons#(X1,mark(X2)) |
→ |
cons#(X1,X2) |
(72) |
1.1.1.1.1.6 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(71) |
|
2 |
≥ |
2 |
1 |
> |
1 |
cons#(X1,active(X2)) |
→ |
cons#(X1,X2) |
(74) |
|
2 |
> |
2 |
1 |
≥ |
1 |
cons#(active(X1),X2) |
→ |
cons#(X1,X2) |
(73) |
|
2 |
≥ |
2 |
1 |
> |
1 |
cons#(X1,mark(X2)) |
→ |
cons#(X1,X2) |
(72) |
|
2 |
> |
2 |
1 |
≥ |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
7th
component contains the
pair
length#(mark(X)) |
→ |
length#(X) |
(79) |
length#(active(X)) |
→ |
length#(X) |
(80) |
1.1.1.1.1.7 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
length#(mark(X)) |
→ |
length#(X) |
(79) |
|
1 |
> |
1 |
length#(active(X)) |
→ |
length#(X) |
(80) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
8th
component contains the
pair
take#(mark(X1),X2) |
→ |
take#(X1,X2) |
(75) |
take#(X1,active(X2)) |
→ |
take#(X1,X2) |
(78) |
take#(active(X1),X2) |
→ |
take#(X1,X2) |
(77) |
take#(X1,mark(X2)) |
→ |
take#(X1,X2) |
(76) |
1.1.1.1.1.8 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
take#(mark(X1),X2) |
→ |
take#(X1,X2) |
(75) |
|
2 |
≥ |
2 |
1 |
> |
1 |
take#(X1,active(X2)) |
→ |
take#(X1,X2) |
(78) |
|
2 |
> |
2 |
1 |
≥ |
1 |
take#(active(X1),X2) |
→ |
take#(X1,X2) |
(77) |
|
2 |
≥ |
2 |
1 |
> |
1 |
take#(X1,mark(X2)) |
→ |
take#(X1,X2) |
(76) |
|
2 |
> |
2 |
1 |
≥ |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.