The rewrite relation of the following TRS is considered.
| f(x,nil) | → | g(nil,x) | (1) |
| f(x,g(y,z)) | → | g(f(x,y),z) | (2) |
| ++(x,nil) | → | x | (3) |
| ++(x,g(y,z)) | → | g(++(x,y),z) | (4) |
| null(nil) | → | true | (5) |
| null(g(x,y)) | → | false | (6) |
| mem(nil,y) | → | false | (7) |
| mem(g(x,y),z) | → | or(=(y,z),mem(x,z)) | (8) |
| mem(x,max(x)) | → | not(null(x)) | (9) |
| max(g(g(nil,x),y)) | → | max'(x,y) | (10) |
| max(g(g(g(x,y),z),u)) | → | max'(max(g(g(x,y),z)),u) | (11) |
| f#(x,g(y,z)) | → | f#(x,y) | (12) |
| ++#(x,g(y,z)) | → | ++#(x,y) | (13) |
| mem#(g(x,y),z) | → | mem#(x,z) | (14) |
| mem#(x,max(x)) | → | null#(x) | (15) |
| max#(g(g(g(x,y),z),u)) | → | max#(g(g(x,y),z)) | (16) |
The dependency pairs are split into 4 components.
| f#(x,g(y,z)) | → | f#(x,y) | (12) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| f#(x,g(y,z)) | → | f#(x,y) | (12) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| ++#(x,g(y,z)) | → | ++#(x,y) | (13) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| ++#(x,g(y,z)) | → | ++#(x,y) | (13) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| mem#(g(x,y),z) | → | mem#(x,z) | (14) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| mem#(g(x,y),z) | → | mem#(x,z) | (14) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| max#(g(g(g(x,y),z),u)) | → | max#(g(g(x,y),z)) | (16) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| max#(g(g(g(x,y),z),u)) | → | max#(g(g(x,y),z)) | (16) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.