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) |
div#(s(X),s(Y)) | → | if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0) | (10) |
geq#(s(X),s(Y)) | → | geq#(X,Y) | (11) |
div#(s(X),s(Y)) | → | minus#(X,Y) | (12) |
div#(s(X),s(Y)) | → | geq#(X,Y) | (13) |
minus#(s(X),s(Y)) | → | minus#(X,Y) | (14) |
div#(s(X),s(Y)) | → | div#(minus(X,Y),s(Y)) | (15) |
The dependency pairs are split into 3 components.
div#(s(X),s(Y)) | → | div#(minus(X,Y),s(Y)) | (15) |
[div#(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 2 |
[minus(x1, x2)] | = | x1 + 1 |
[geq#(x1, x2)] | = | 0 |
[false] | = | 0 |
[div(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 0 |
[true] | = | 0 |
[0] | = | 1 |
[if(x1, x2, x3)] | = | 0 |
[minus#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 0 |
minus(0,Y) | → | 0 | (1) |
minus(s(X),s(Y)) | → | minus(X,Y) | (2) |
div#(s(X),s(Y)) | → | div#(minus(X,Y),s(Y)) | (15) |
The dependency pairs are split into 0 components.
geq#(s(X),s(Y)) | → | geq#(X,Y) | (11) |
[div#(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 2 |
[minus(x1, x2)] | = | x1 + 1 |
[geq#(x1, x2)] | = | x1 + x2 + 0 |
[false] | = | 0 |
[div(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 0 |
[true] | = | 0 |
[0] | = | 1 |
[if(x1, x2, x3)] | = | 0 |
[minus#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 0 |
minus(0,Y) | → | 0 | (1) |
minus(s(X),s(Y)) | → | minus(X,Y) | (2) |
geq#(s(X),s(Y)) | → | geq#(X,Y) | (11) |
The dependency pairs are split into 0 components.
minus#(s(X),s(Y)) | → | minus#(X,Y) | (14) |
[div#(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 2 |
[minus(x1, x2)] | = | x1 + 1 |
[geq#(x1, x2)] | = | 0 |
[false] | = | 0 |
[div(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 0 |
[true] | = | 0 |
[0] | = | 1 |
[if(x1, x2, x3)] | = | 0 |
[minus#(x1, x2)] | = | x1 + x2 + 0 |
[if#(x1, x2, x3)] | = | 0 |
minus(0,Y) | → | 0 | (1) |
minus(s(X),s(Y)) | → | minus(X,Y) | (2) |
minus#(s(X),s(Y)) | → | minus#(X,Y) | (14) |
The dependency pairs are split into 0 components.