The rewrite relation of the following TRS is considered.
minus(0,Y) | → | 0 | (1) |
minus(s(X),s(Y)) | → | minus(X,Y) | (2) |
geq(X,0) | → | true | (3) |
geq(0,s(Y)) | → | false | (4) |
geq(s(X),s(Y)) | → | geq(X,Y) | (5) |
div(0,s(Y)) | → | 0 | (6) |
div(s(X),s(Y)) | → | if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) | (7) |
if(true,X,Y) | → | X | (8) |
if(false,X,Y) | → | Y | (9) |
minus#(s(X),s(Y)) | → | minus#(X,Y) | (10) |
geq#(s(X),s(Y)) | → | geq#(X,Y) | (11) |
div#(s(X),s(Y)) | → | minus#(X,Y) | (12) |
div#(s(X),s(Y)) | → | div#(minus(X,Y),s(Y)) | (13) |
div#(s(X),s(Y)) | → | geq#(X,Y) | (14) |
div#(s(X),s(Y)) | → | if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0) | (15) |
The dependency pairs are split into 2 components.
minus#(s(X),s(Y)) | → | minus#(X,Y) | (10) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
minus#(s(X),s(Y)) | → | minus#(X,Y) | (10) |
2 | > | 2 | |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
geq#(s(X),s(Y)) | → | geq#(X,Y) | (11) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
geq#(s(X),s(Y)) | → | geq#(X,Y) | (11) |
2 | > | 2 | |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.