The rewrite relation of the following TRS is considered.
f(c(a,z,x)) | → | b(a,z) | (1) |
b(x,b(z,y)) | → | f(b(f(f(z)),c(x,z,y))) | (2) |
b(y,z) | → | z | (3) |
b#(x,b(z,y)) | → | b#(f(f(z)),c(x,z,y)) | (4) |
f#(c(a,z,x)) | → | b#(a,z) | (5) |
b#(x,b(z,y)) | → | f#(f(z)) | (6) |
b#(x,b(z,y)) | → | f#(b(f(f(z)),c(x,z,y))) | (7) |
b#(x,b(z,y)) | → | f#(z) | (8) |
The dependency pairs are split into 1 component.
b#(x,b(z,y)) | → | f#(z) | (8) |
b#(x,b(z,y)) | → | f#(b(f(f(z)),c(x,z,y))) | (7) |
b#(x,b(z,y)) | → | f#(f(z)) | (6) |
f#(c(a,z,x)) | → | b#(a,z) | (5) |
[a] | = | 0 |
[b(x1, x2)] | = | max(x1 + 26576, x2 + 26574, 0) |
[c(x1, x2, x3)] | = | max(x2 + 17718, x3 + 1, 0) |
[f(x1)] | = | x1 + 8858 |
[f#(x1)] | = | x1 + 14236 |
[b#(x1, x2)] | = | max(x1 + 14235, x2 + 31953, 0) |
f(c(a,z,x)) | → | b(a,z) | (1) |
b(y,z) | → | z | (3) |
b(x,b(z,y)) | → | f(b(f(f(z)),c(x,z,y))) | (2) |
b#(x,b(z,y)) | → | f#(z) | (8) |
b#(x,b(z,y)) | → | f#(b(f(f(z)),c(x,z,y))) | (7) |
b#(x,b(z,y)) | → | f#(f(z)) | (6) |
f#(c(a,z,x)) | → | b#(a,z) | (5) |
The dependency pairs are split into 0 components.