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) |
| quot(0,s(y)) | → | 0 | (8) |
| quot(s(x),s(y)) | → | s(quot(minus(x,y),s(y))) | (9) |
| log(s(0)) | → | 0 | (10) |
| log(s(s(x))) | → | s(log(s(quot(x,s(s(0)))))) | (11) |
| le#(s(x),s(y)) | → | le#(x,y) | (12) |
| minus#(s(x),y) | → | le#(s(x),y) | (13) |
| minus#(s(x),y) | → | if_minus#(le(s(x),y),s(x),y) | (14) |
| if_minus#(false,s(x),y) | → | minus#(x,y) | (15) |
| quot#(s(x),s(y)) | → | minus#(x,y) | (16) |
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (17) |
| log#(s(s(x))) | → | quot#(x,s(s(0))) | (18) |
| log#(s(s(x))) | → | log#(s(quot(x,s(s(0))))) | (19) |
The dependency pairs are split into 4 components.
| log#(s(s(x))) | → | log#(s(quot(x,s(s(0))))) | (19) |
| prec(log#) | = | 0 | stat(log#) | = | lex | |
| prec(quot) | = | 0 | stat(quot) | = | lex | |
| prec(if_minus) | = | 0 | stat(if_minus) | = | lex | |
| prec(minus) | = | 0 | stat(minus) | = | lex | |
| prec(false) | = | 0 | stat(false) | = | lex | |
| prec(s) | = | 1 | stat(s) | = | lex | |
| prec(true) | = | 0 | stat(true) | = | lex | |
| prec(le) | = | 0 | stat(le) | = | lex | |
| prec(0) | = | 0 | stat(0) | = | lex |
| π(log#) | = | 1 |
| π(quot) | = | 1 |
| π(if_minus) | = | 2 |
| π(minus) | = | 1 |
| π(false) | = | [] |
| π(s) | = | [1] |
| π(true) | = | [] |
| π(le) | = | 1 |
| π(0) | = | [] |
| quot(0,s(y)) | → | 0 | (8) |
| quot(s(x),s(y)) | → | s(quot(minus(x,y),s(y))) | (9) |
| 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) |
| log#(s(s(x))) | → | log#(s(quot(x,s(s(0))))) | (19) |
There are no pairs anymore.
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (17) |
| prec(quot#) | = | 0 | stat(quot#) | = | lex | |
| prec(if_minus) | = | 0 | stat(if_minus) | = | lex | |
| prec(minus) | = | 0 | stat(minus) | = | lex | |
| prec(false) | = | 0 | stat(false) | = | lex | |
| prec(s) | = | 1 | stat(s) | = | lex | |
| prec(true) | = | 0 | stat(true) | = | lex | |
| prec(le) | = | 0 | stat(le) | = | lex | |
| prec(0) | = | 0 | stat(0) | = | lex |
| π(quot#) | = | 1 |
| π(if_minus) | = | 2 |
| π(minus) | = | 1 |
| π(false) | = | [] |
| π(s) | = | [1] |
| π(true) | = | [] |
| π(le) | = | [] |
| π(0) | = | [] |
| 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) |
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (17) |
There are no pairs anymore.
| minus#(s(x),y) | → | if_minus#(le(s(x),y),s(x),y) | (14) |
| if_minus#(false,s(x),y) | → | minus#(x,y) | (15) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| minus#(s(x),y) | → | if_minus#(le(s(x),y),s(x),y) | (14) |
| 2 | ≥ | 3 | |
| 1 | ≥ | 2 | |
| if_minus#(false,s(x),y) | → | minus#(x,y) | (15) |
| 3 | ≥ | 2 | |
| 2 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| le#(s(x),s(y)) | → | le#(x,y) | (12) |
| π(le#) | = | 1 |
| le#(s(x),s(y)) | → | le#(x,y) | (12) |
There are no pairs anymore.