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