The rewrite relation of the following TRS is considered.
| f(x,0) | → | s(0) | (1) |
| f(s(x),s(y)) | → | s(f(x,y)) | (2) |
| g(0,x) | → | g(f(x,x),x) | (3) |
| f#(s(x),s(y)) | → | f#(x,y) | (4) |
| g#(0,x) | → | f#(x,x) | (5) |
| g#(0,x) | → | g#(f(x,x),x) | (6) |
The dependency pairs are split into 1 component.
| f#(s(x),s(y)) | → | f#(x,y) | (4) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| f#(s(x),s(y)) | → | f#(x,y) | (4) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.