The rewrite relation of the following TRS is considered.
times(x,plus(y,1)) | → | plus(times(x,plus(y,times(1,0))),x) | (1) |
times(x,1) | → | x | (2) |
plus(x,0) | → | x | (3) |
times(x,0) | → | 0 | (4) |
The TRS is overlay and locally confluent:
10Hence, it suffices to show innermost termination in the following.
times#(x,plus(y,1)) | → | plus#(times(x,plus(y,times(1,0))),x) | (5) |
times#(x,plus(y,1)) | → | times#(x,plus(y,times(1,0))) | (6) |
times#(x,plus(y,1)) | → | plus#(y,times(1,0)) | (7) |
times#(x,plus(y,1)) | → | times#(1,0) | (8) |
The dependency pairs are split into 1 component.
times#(x,plus(y,1)) | → | times#(x,plus(y,times(1,0))) | (6) |
We restrict the rewrite rules to the following usable rules of the DP problem.
times(x,0) | → | 0 | (4) |
plus(x,0) | → | x | (3) |
[times(x1, x2)] | = | 2 · x1 + 1 · x2 |
[0] | = | 0 |
[plus(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[times#(x1, x2)] | = | 1 · x1 + 2 · x2 |
[1] | = | 0 |
times(x,plus(y,1)) | → | plus(times(x,plus(y,times(1,0))),x) | (1) |
times(x,1) | → | x | (2) |
plus(x,0) | → | x | (3) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
times#(x,plus(y,1)) | → | times#(x,plus(y,times(1,0))) | (6) |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.