The rewrite relation of the following TRS is considered.
|
minus(x,0) |
→ |
x |
(1) |
|
minus(s(x),s(y)) |
→ |
minus(x,y) |
(2) |
|
quot(0,s(y)) |
→ |
0 |
(3) |
|
quot(s(x),s(y)) |
→ |
s(quot(minus(x,y),s(y))) |
(4) |
|
app(nil,y) |
→ |
y |
(5) |
|
app(add(n,x),y) |
→ |
add(n,app(x,y)) |
(6) |
|
reverse(nil) |
→ |
nil |
(7) |
|
reverse(add(n,x)) |
→ |
app(reverse(x),add(n,nil)) |
(8) |
|
shuffle(nil) |
→ |
nil |
(9) |
|
shuffle(add(n,x)) |
→ |
add(n,shuffle(reverse(x))) |
(10) |
|
concat(leaf,y) |
→ |
y |
(11) |
|
concat(cons(u,v),y) |
→ |
cons(u,concat(v,y)) |
(12) |
|
less_leaves(x,leaf) |
→ |
false |
(13) |
|
less_leaves(leaf,cons(w,z)) |
→ |
true |
(14) |
|
less_leaves(cons(u,v),cons(w,z)) |
→ |
less_leaves(concat(u,v),concat(w,z)) |
(15) |
|
minus#(s(x),s(y)) |
→ |
minus#(x,y) |
(16) |
|
quot#(s(x),s(y)) |
→ |
minus#(x,y) |
(17) |
|
quot#(s(x),s(y)) |
→ |
quot#(minus(x,y),s(y)) |
(18) |
|
app#(add(n,x),y) |
→ |
app#(x,y) |
(19) |
|
reverse#(add(n,x)) |
→ |
reverse#(x) |
(20) |
|
reverse#(add(n,x)) |
→ |
app#(reverse(x),add(n,nil)) |
(21) |
|
shuffle#(add(n,x)) |
→ |
reverse#(x) |
(22) |
|
shuffle#(add(n,x)) |
→ |
shuffle#(reverse(x)) |
(23) |
|
concat#(cons(u,v),y) |
→ |
concat#(v,y) |
(24) |
|
less_leaves#(cons(u,v),cons(w,z)) |
→ |
concat#(w,z) |
(25) |
|
less_leaves#(cons(u,v),cons(w,z)) |
→ |
concat#(u,v) |
(26) |
|
less_leaves#(cons(u,v),cons(w,z)) |
→ |
less_leaves#(concat(u,v),concat(w,z)) |
(27) |
The dependency pairs are split into 7
components.
-
The
1st
component contains the
pair
|
quot#(s(x),s(y)) |
→ |
quot#(minus(x,y),s(y)) |
(18) |
1.1.1 Subterm Criterion Processor
We use the projection to multisets
| π(quot#)
|
= |
{
1
}
|
| π(minus)
|
= |
{
1
}
|
to remove the pairs:
|
quot#(s(x),s(y)) |
→ |
quot#(minus(x,y),s(y)) |
(18) |
1.1.1.1 P is empty
There are no pairs anymore.
-
The
2nd
component contains the
pair
|
minus#(s(x),s(y)) |
→ |
minus#(x,y) |
(16) |
1.1.2 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
minus#(s(x),s(y)) |
→ |
minus#(x,y) |
(16) |
|
|
| 2 |
> |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
3rd
component contains the
pair
|
shuffle#(add(n,x)) |
→ |
shuffle#(reverse(x)) |
(23) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the naturals
| [nil] |
= |
|
| [shuffle#(x1)] |
= |
· x1 +
|
| [app(x1, x2)] |
= |
· x1 + · x2 +
|
| [reverse(x1)] |
= |
· x1 +
|
| [add(x1, x2)] |
= |
· x1 + · x2 +
|
together with the usable
rules
|
reverse(nil) |
→ |
nil |
(7) |
|
reverse(add(n,x)) |
→ |
app(reverse(x),add(n,nil)) |
(8) |
|
app(nil,y) |
→ |
y |
(5) |
|
app(add(n,x),y) |
→ |
add(n,app(x,y)) |
(6) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
|
shuffle#(add(n,x)) |
→ |
shuffle#(reverse(x)) |
(23) |
could be deleted.
1.1.3.1 P is empty
There are no pairs anymore.
-
The
4th
component contains the
pair
|
reverse#(add(n,x)) |
→ |
reverse#(x) |
(20) |
1.1.4 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
reverse#(add(n,x)) |
→ |
reverse#(x) |
(20) |
|
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
5th
component contains the
pair
|
app#(add(n,x),y) |
→ |
app#(x,y) |
(19) |
1.1.5 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
app#(add(n,x),y) |
→ |
app#(x,y) |
(19) |
|
|
| 2 |
≥ |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
6th
component contains the
pair
|
less_leaves#(cons(u,v),cons(w,z)) |
→ |
less_leaves#(concat(u,v),concat(w,z)) |
(27) |
1.1.6 Subterm Criterion Processor
We use the projection to multisets
| π(less_leaves#)
|
= |
{
1
}
|
| π(cons)
|
= |
{
1, 1, 1, 2
}
|
| π(concat)
|
= |
{
1, 1, 2
}
|
| π(add)
|
= |
{
2, 2, 2
}
|
| π(s)
|
= |
{
1, 1, 1
}
|
to remove the pairs:
|
less_leaves#(cons(u,v),cons(w,z)) |
→ |
less_leaves#(concat(u,v),concat(w,z)) |
(27) |
1.1.6.1 P is empty
There are no pairs anymore.
-
The
7th
component contains the
pair
|
concat#(cons(u,v),y) |
→ |
concat#(v,y) |
(24) |
1.1.7 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
concat#(cons(u,v),y) |
→ |
concat#(v,y) |
(24) |
|
|
| 2 |
≥ |
2 |
| 1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.