The rewrite relation of the following TRS is considered.
| -(x,0) | → | x | (1) |
| -(s(x),s(y)) | → | -(x,y) | (2) |
| <=(0,y) | → | true | (3) |
| <=(s(x),0) | → | false | (4) |
| <=(s(x),s(y)) | → | <=(x,y) | (5) |
| if(true,x,y) | → | x | (6) |
| if(false,x,y) | → | y | (7) |
| perfectp(0) | → | false | (8) |
| perfectp(s(x)) | → | f(x,s(0),s(x),s(x)) | (9) |
| f(0,y,0,u) | → | true | (10) |
| f(0,y,s(z),u) | → | false | (11) |
| f(s(x),0,z,u) | → | f(x,u,-(z,s(x)),u) | (12) |
| f(s(x),s(y),z,u) | → | if(<=(x,y),f(s(x),-(y,x),z,u),f(x,u,z,u)) | (13) |
| -#(s(x),s(y)) | → | -#(x,y) | (14) |
| <=#(s(x),s(y)) | → | <=#(x,y) | (15) |
| perfectp#(s(x)) | → | f#(x,s(0),s(x),s(x)) | (16) |
| f#(s(x),0,z,u) | → | -#(z,s(x)) | (17) |
| f#(s(x),0,z,u) | → | f#(x,u,-(z,s(x)),u) | (18) |
| f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (19) |
| f#(s(x),s(y),z,u) | → | -#(y,x) | (20) |
| f#(s(x),s(y),z,u) | → | f#(s(x),-(y,x),z,u) | (21) |
| f#(s(x),s(y),z,u) | → | <=#(x,y) | (22) |
| f#(s(x),s(y),z,u) | → | if#(<=(x,y),f(s(x),-(y,x),z,u),f(x,u,z,u)) | (23) |
The dependency pairs are split into 3 components.
| f#(s(x),s(y),z,u) | → | f#(s(x),-(y,x),z,u) | (21) |
| f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (19) |
| f#(s(x),0,z,u) | → | f#(x,u,-(z,s(x)),u) | (18) |
| π(f#) | = | 1 |
| f#(s(x),s(y),z,u) | → | f#(x,u,z,u) | (19) |
| f#(s(x),0,z,u) | → | f#(x,u,-(z,s(x)),u) | (18) |
| π(f#) | = | { 2 } |
| π(-) | = | { 1 } |
| f#(s(x),s(y),z,u) | → | f#(s(x),-(y,x),z,u) | (21) |
There are no pairs anymore.
| -#(s(x),s(y)) | → | -#(x,y) | (14) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| -#(s(x),s(y)) | → | -#(x,y) | (14) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| <=#(s(x),s(y)) | → | <=#(x,y) | (15) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| <=#(s(x),s(y)) | → | <=#(x,y) | (15) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.