The rewrite relation of the following TRS is considered.
| f(0) | → | 0 | (1) |
| f(s(0)) | → | s(0) | (2) |
| f(s(s(x))) | → | p(h(g(x))) | (3) |
| g(0) | → | pair(s(0),s(0)) | (4) |
| g(s(x)) | → | h(g(x)) | (5) |
| h(x) | → | pair(+(p(x),q(x)),p(x)) | (6) |
| p(pair(x,y)) | → | x | (7) |
| q(pair(x,y)) | → | y | (8) |
| +(x,0) | → | x | (9) |
| +(x,s(y)) | → | s(+(x,y)) | (10) |
| f(s(s(x))) | → | +(p(g(x)),q(g(x))) | (11) |
| g(s(x)) | → | pair(+(p(g(x)),q(g(x))),p(g(x))) | (12) |
| f#(s(s(x))) | → | g#(x) | (13) |
| f#(s(s(x))) | → | h#(g(x)) | (14) |
| f#(s(s(x))) | → | p#(h(g(x))) | (15) |
| g#(s(x)) | → | g#(x) | (16) |
| g#(s(x)) | → | h#(g(x)) | (17) |
| h#(x) | → | q#(x) | (18) |
| h#(x) | → | p#(x) | (19) |
| h#(x) | → | +#(p(x),q(x)) | (20) |
| +#(x,s(y)) | → | +#(x,y) | (21) |
| f#(s(s(x))) | → | q#(g(x)) | (22) |
| f#(s(s(x))) | → | p#(g(x)) | (23) |
| f#(s(s(x))) | → | +#(p(g(x)),q(g(x))) | (24) |
| g#(s(x)) | → | q#(g(x)) | (25) |
| g#(s(x)) | → | p#(g(x)) | (26) |
| g#(s(x)) | → | +#(p(g(x)),q(g(x))) | (27) |
The dependency pairs are split into 2 components.
| g#(s(x)) | → | g#(x) | (16) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| g#(s(x)) | → | g#(x) | (16) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| +#(x,s(y)) | → | +#(x,y) | (21) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| +#(x,s(y)) | → | +#(x,y) | (21) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.