The rewrite relation of the following TRS is considered.
| f(a,f(x,a)) | → | f(a,f(f(a,a),f(a,x))) | (1) |
The TRS is overlay and locally confluent:
10Hence, it suffices to show innermost termination in the following.
| f#(a,f(x,a)) | → | f#(a,f(f(a,a),f(a,x))) | (2) |
| f#(a,f(x,a)) | → | f#(f(a,a),f(a,x)) | (3) |
| f#(a,f(x,a)) | → | f#(a,a) | (4) |
| f#(a,f(x,a)) | → | f#(a,x) | (5) |
The dependency pairs are split into 1 component.
| f#(a,f(x,a)) | → | f#(a,x) | (5) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| f#(a,f(x,a)) | → | f#(a,x) | (5) |
| 1 | ≥ | 1 | |
| 2 | > | 1 | |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.