The rewrite relation of the following TRS is considered.
| c(z,x,a) | → | f(b(b(f(z),z),x)) | (1) |
| b(y,b(z,a)) | → | f(b(c(f(a),y,z),z)) | (2) |
| f(c(c(z,a,a),x,a)) | → | z | (3) |
| c#(z,x,a) | → | f#(z) | (4) |
| c#(z,x,a) | → | b#(f(z),z) | (5) |
| c#(z,x,a) | → | b#(b(f(z),z),x) | (6) |
| c#(z,x,a) | → | f#(b(b(f(z),z),x)) | (7) |
| b#(y,b(z,a)) | → | f#(a) | (8) |
| b#(y,b(z,a)) | → | c#(f(a),y,z) | (9) |
| b#(y,b(z,a)) | → | b#(c(f(a),y,z),z) | (10) |
| b#(y,b(z,a)) | → | f#(b(c(f(a),y,z),z)) | (11) |
The dependency pairs are split into 1 component.
| b#(y,b(z,a)) | → | b#(c(f(a),y,z),z) | (10) |
| b#(y,b(z,a)) | → | c#(f(a),y,z) | (9) |
| c#(z,x,a) | → | b#(f(z),z) | (5) |
| c#(z,x,a) | → | b#(b(f(z),z),x) | (6) |
| [c#(x1, x2, x3)] | = | 4 · x1 + 0 · x2 + 0 · x3 + 4 |
| [c(x1, x2, x3)] | = | 1 · x1 + -∞ · x2 + -∞ · x3 + 4 |
| [b(x1, x2)] | = | 0 · x1 + -∞ · x2 + 4 |
| [a] | = | 0 |
| [b#(x1, x2)] | = | 0 · x1 + 0 · x2 + 0 |
| [f(x1)] | = | 0 · x1 + 0 |
| c(z,x,a) | → | f(b(b(f(z),z),x)) | (1) |
| b(y,b(z,a)) | → | f(b(c(f(a),y,z),z)) | (2) |
| f(c(c(z,a,a),x,a)) | → | z | (3) |
| c#(z,x,a) | → | b#(f(z),z) | (5) |
| [c#(x1, x2, x3)] | = | -2 · x1 + -4 · x2 + -5 · x3 + 0 |
| [c(x1, x2, x3)] | = | 3 · x1 + -3 · x2 + -∞ · x3 + 0 |
| [b(x1, x2)] | = | 0 · x1 + -1 · x2 + -16 |
| [a] | = | 6 |
| [b#(x1, x2)] | = | -4 · x1 + -5 · x2 + 0 |
| [f(x1)] | = | -5 · x1 + 0 |
| c(z,x,a) | → | f(b(b(f(z),z),x)) | (1) |
| b(y,b(z,a)) | → | f(b(c(f(a),y,z),z)) | (2) |
| f(c(c(z,a,a),x,a)) | → | z | (3) |
| c#(z,x,a) | → | b#(b(f(z),z),x) | (6) |
The dependency pairs are split into 1 component.
| b#(y,b(z,a)) | → | b#(c(f(a),y,z),z) | (10) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| b#(y,b(z,a)) | → | b#(c(f(a),y,z),z) | (10) |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.