The rewrite relation of the following TRS is considered.
perfectp(0) | → | false | (1) |
perfectp(s(x)) | → | f(x,s(0),s(x),s(x)) | (2) |
f(0,y,0,u) | → | true | (3) |
f(0,y,s(z),u) | → | false | (4) |
f(s(x),0,z,u) | → | f(x,u,minus(z,s(x)),u) | (5) |
f(s(x),s(y),z,u) | → | if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) | (6) |
f#(s(x),s(y),z,u) | → | f#(s(x),minus(y,x),z,u) | (7) |
f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (8) |
perfectp#(s(x)) | → | f#(x,s(0),s(x),s(x)) | (9) |
f#(s(x),0,z,u) | → | f#(x,u,minus(z,s(x)),u) | (10) |
The dependency pairs are split into 1 component.
f#(s(x),0,z,u) | → | f#(x,u,minus(z,s(x)),u) | (10) |
f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (8) |
[le(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[minus(x1, x2)] | = | 1 |
[perfectp#(x1)] | = | 0 |
[false] | = | 0 |
[true] | = | 0 |
[f(x1,...,x4)] | = | 0 |
[0] | = | 2 |
[if(x1, x2, x3)] | = | 0 |
[f#(x1,...,x4)] | = | x1 + x3 + 0 |
[perfectp(x1)] | = | 0 |
f#(s(x),0,z,u) | → | f#(x,u,minus(z,s(x)),u) | (10) |
f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (8) |
The dependency pairs are split into 0 components.