The rewrite relation of the following TRS is considered.
f(x,f(a,a)) | → | f(f(f(a,a),a),x) | (1) |
The TRS is overlay and locally confluent:
10Hence, it suffices to show innermost termination in the following.
f#(x,f(a,a)) | → | f#(f(f(a,a),a),x) | (2) |
f#(x,f(a,a)) | → | f#(f(a,a),a) | (3) |
The dependency pairs are split into 1 component.
f#(x,f(a,a)) | → | f#(f(f(a,a),a),x) | (2) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
[f#(x1, x2)] | = | -1 + 2 · x1 + 2 · x2 |
[f(x1, x2)] | = | -1 + x1 |
[a] | = | 2 |
f#(x,f(a,a)) | → | f#(f(f(a,a),a),x) | (2) |
There are no pairs anymore.