The rewrite relation of the following TRS is considered.
| D(t) | → | 1 | (1) |
| D(constant) | → | 0 | (2) |
| D(+(x,y)) | → | +(D(x),D(y)) | (3) |
| D(*(x,y)) | → | +(*(y,D(x)),*(x,D(y))) | (4) |
| D(-(x,y)) | → | -(D(x),D(y)) | (5) |
| D(minus(x)) | → | minus(D(x)) | (6) |
| D(div(x,y)) | → | -(div(D(x),y),div(*(x,D(y)),pow(y,2))) | (7) |
| D(ln(x)) | → | div(D(x),x) | (8) |
| D(pow(x,y)) | → | +(*(*(y,pow(x,-(y,1))),D(x)),*(*(pow(x,y),ln(x)),D(y))) | (9) |
| D#(+(x,y)) | → | D#(y) | (10) |
| D#(+(x,y)) | → | D#(x) | (11) |
| D#(*(x,y)) | → | D#(y) | (12) |
| D#(*(x,y)) | → | D#(x) | (13) |
| D#(-(x,y)) | → | D#(y) | (14) |
| D#(-(x,y)) | → | D#(x) | (15) |
| D#(minus(x)) | → | D#(x) | (16) |
| D#(div(x,y)) | → | D#(y) | (17) |
| D#(div(x,y)) | → | D#(x) | (18) |
| D#(ln(x)) | → | D#(x) | (19) |
| D#(pow(x,y)) | → | D#(y) | (20) |
| D#(pow(x,y)) | → | D#(x) | (21) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| D#(+(x,y)) | → | D#(y) | (10) |
| 1 | > | 1 | |
| D#(+(x,y)) | → | D#(x) | (11) |
| 1 | > | 1 | |
| D#(*(x,y)) | → | D#(y) | (12) |
| 1 | > | 1 | |
| D#(*(x,y)) | → | D#(x) | (13) |
| 1 | > | 1 | |
| D#(-(x,y)) | → | D#(y) | (14) |
| 1 | > | 1 | |
| D#(-(x,y)) | → | D#(x) | (15) |
| 1 | > | 1 | |
| D#(minus(x)) | → | D#(x) | (16) |
| 1 | > | 1 | |
| D#(div(x,y)) | → | D#(y) | (17) |
| 1 | > | 1 | |
| D#(div(x,y)) | → | D#(x) | (18) |
| 1 | > | 1 | |
| D#(ln(x)) | → | D#(x) | (19) |
| 1 | > | 1 | |
| D#(pow(x,y)) | → | D#(y) | (20) |
| 1 | > | 1 | |
| D#(pow(x,y)) | → | D#(x) | (21) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.