The rewrite relation of the following TRS is considered.
| minus(0,y) | → | 0 | (1) |
| minus(s(x),0) | → | s(x) | (2) |
| minus(s(x),s(y)) | → | minus(x,y) | (3) |
| le(0,y) | → | true | (4) |
| le(s(x),0) | → | false | (5) |
| le(s(x),s(y)) | → | le(x,y) | (6) |
| if(true,x,y) | → | x | (7) |
| if(false,x,y) | → | y | (8) |
| perfectp(0) | → | false | (9) |
| perfectp(s(x)) | → | f(x,s(0),s(x),s(x)) | (10) |
| f(0,y,0,u) | → | true | (11) |
| f(0,y,s(z),u) | → | false | (12) |
| f(s(x),0,z,u) | → | f(x,u,minus(z,s(x)),u) | (13) |
| f(s(x),s(y),z,u) | → | if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) | (14) |
| f#(s(x),0,z,u) | → | f#(x,u,minus(z,s(x)),u) | (15) |
| f#(s(x),s(y),z,u) | → | f#(s(x),minus(y,x),z,u) | (16) |
| perfectp#(s(x)) | → | f#(x,s(0),s(x),s(x)) | (17) |
| f#(s(x),s(y),z,u) | → | minus#(y,x) | (18) |
| minus#(s(x),s(y)) | → | minus#(x,y) | (19) |
| f#(s(x),s(y),z,u) | → | le#(x,y) | (20) |
| f#(s(x),0,z,u) | → | minus#(z,s(x)) | (21) |
| le#(s(x),s(y)) | → | le#(x,y) | (22) |
| f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (23) |
| f#(s(x),s(y),z,u) | → | if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) | (24) |
The dependency pairs are split into 3 components.
| f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (23) |
| f#(s(x),s(y),z,u) | → | f#(s(x),minus(y,x),z,u) | (16) |
| f#(s(x),0,z,u) | → | f#(x,u,minus(z,s(x)),u) | (15) |
| [le(x1, x2)] | = | 0 |
| [s(x1)] | = | x1 + 2 |
| [le#(x1, x2)] | = | 0 |
| [minus(x1, x2)] | = | x1 + 1 |
| [perfectp#(x1)] | = | 0 |
| [false] | = | 0 |
| [true] | = | 0 |
| [f(x1,...,x4)] | = | 0 |
| [0] | = | 1 |
| [if(x1, x2, x3)] | = | 0 |
| [f#(x1,...,x4)] | = | x1 + x3 + 0 |
| [minus#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [perfectp(x1)] | = | 0 |
| minus(0,y) | → | 0 | (1) |
| minus(s(x),s(y)) | → | minus(x,y) | (3) |
| minus(s(x),0) | → | s(x) | (2) |
| f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (23) |
| f#(s(x),0,z,u) | → | f#(x,u,minus(z,s(x)),u) | (15) |
The dependency pairs are split into 1 component.
| f#(s(x),s(y),z,u) | → | f#(s(x),minus(y,x),z,u) | (16) |
| [le(x1, x2)] | = | 0 |
| [s(x1)] | = | x1 + 2 |
| [le#(x1, x2)] | = | 0 |
| [minus(x1, x2)] | = | x1 + 1 |
| [perfectp#(x1)] | = | 0 |
| [false] | = | 0 |
| [true] | = | 0 |
| [f(x1,...,x4)] | = | 0 |
| [0] | = | 1 |
| [if(x1, x2, x3)] | = | 0 |
| [f#(x1,...,x4)] | = | x2 + x3 + 0 |
| [minus#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [perfectp(x1)] | = | 0 |
| minus(0,y) | → | 0 | (1) |
| minus(s(x),s(y)) | → | minus(x,y) | (3) |
| minus(s(x),0) | → | s(x) | (2) |
| f#(s(x),s(y),z,u) | → | f#(s(x),minus(y,x),z,u) | (16) |
The dependency pairs are split into 0 components.
| le#(s(x),s(y)) | → | le#(x,y) | (22) |
| [le(x1, x2)] | = | 0 |
| [s(x1)] | = | x1 + 2 |
| [le#(x1, x2)] | = | x1 + x2 + 0 |
| [minus(x1, x2)] | = | x1 + 1 |
| [perfectp#(x1)] | = | 0 |
| [false] | = | 0 |
| [true] | = | 0 |
| [f(x1,...,x4)] | = | 0 |
| [0] | = | 1 |
| [if(x1, x2, x3)] | = | 0 |
| [f#(x1,...,x4)] | = | x2 + x3 + 0 |
| [minus#(x1, x2)] | = | 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [perfectp(x1)] | = | 0 |
| minus(0,y) | → | 0 | (1) |
| minus(s(x),s(y)) | → | minus(x,y) | (3) |
| minus(s(x),0) | → | s(x) | (2) |
| le#(s(x),s(y)) | → | le#(x,y) | (22) |
The dependency pairs are split into 0 components.
| minus#(s(x),s(y)) | → | minus#(x,y) | (19) |
| [le(x1, x2)] | = | 0 |
| [s(x1)] | = | x1 + 2 |
| [le#(x1, x2)] | = | 0 |
| [minus(x1, x2)] | = | x1 + 1 |
| [perfectp#(x1)] | = | 0 |
| [false] | = | 0 |
| [true] | = | 0 |
| [f(x1,...,x4)] | = | 0 |
| [0] | = | 1 |
| [if(x1, x2, x3)] | = | 0 |
| [f#(x1,...,x4)] | = | x2 + x3 + 0 |
| [minus#(x1, x2)] | = | x1 + x2 + 0 |
| [if#(x1, x2, x3)] | = | 0 |
| [perfectp(x1)] | = | 0 |
| minus(0,y) | → | 0 | (1) |
| minus(s(x),s(y)) | → | minus(x,y) | (3) |
| minus(s(x),0) | → | s(x) | (2) |
| minus#(s(x),s(y)) | → | minus#(x,y) | (19) |
The dependency pairs are split into 0 components.