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