The rewrite relation of the following TRS is considered.
ap(ap(ff,x),x) | → | ap(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (1) |
ap#(ap(ff,x),x) | → | ap#(cons,x) | (2) |
ap#(ap(ff,x),x) | → | ap#(ap(cons,x),nil) | (3) |
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (4) |
ap#(ap(ff,x),x) | → | ap#(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (5) |
The dependency pairs are split into 1 component.
ap#(ap(ff,x),x) | → | ap#(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (5) |
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (4) |
[ap#(x1, x2)] | = | 0 · x1 + 0 · x2 + 0 |
[ap(x1, x2)] | = | -2 · x1 + -3 · x2 + 1 |
[nil] | = | 4 |
[ff] | = | 8 |
[cons] | = | 4 |
ap(ap(ff,x),x) | → | ap(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (1) |
ap#(ap(ff,x),x) | → | ap#(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (5) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (4) |
2 | ≥ | 1 | |
1 | ≥ | 2 | |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.