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