The rewrite relation of the following TRS is considered.
| f(a,g(y)) | → | g(g(y)) | (1) |
| f(g(x),a) | → | f(x,g(a)) | (2) |
| f(g(x),g(y)) | → | h(g(y),x,g(y)) | (3) |
| h(g(x),y,z) | → | f(y,h(x,y,z)) | (4) |
| h(a,y,z) | → | z | (5) |
| f#(g(x),a) | → | f#(x,g(a)) | (6) |
| f#(g(x),g(y)) | → | h#(g(y),x,g(y)) | (7) |
| h#(g(x),y,z) | → | h#(x,y,z) | (8) |
| h#(g(x),y,z) | → | f#(y,h(x,y,z)) | (9) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| f#(g(x),a) | → | f#(x,g(a)) | (6) |
| 1 | > | 1 | |
| f#(g(x),g(y)) | → | h#(g(y),x,g(y)) | (7) |
| 2 | ≥ | 3 | |
| 2 | ≥ | 1 | |
| 1 | > | 2 | |
| h#(g(x),y,z) | → | h#(x,y,z) | (8) |
| 3 | ≥ | 3 | |
| 2 | ≥ | 2 | |
| 1 | > | 1 | |
| h#(g(x),y,z) | → | f#(y,h(x,y,z)) | (9) |
| 2 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.