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