The rewrite relation of the following TRS is considered.
| qsort(nil) | → | nil | (1) |
| qsort(.(x,y)) | → | ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) | (2) |
| lowers(x,nil) | → | nil | (3) |
| lowers(x,.(y,z)) | → | if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) | (4) |
| greaters(x,nil) | → | nil | (5) |
| greaters(x,.(y,z)) | → | if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) | (6) |
| qsort#(.(x,y)) | → | greaters#(x,y) | (7) |
| qsort#(.(x,y)) | → | qsort#(greaters(x,y)) | (8) |
| qsort#(.(x,y)) | → | lowers#(x,y) | (9) |
| qsort#(.(x,y)) | → | qsort#(lowers(x,y)) | (10) |
| lowers#(x,.(y,z)) | → | lowers#(x,z) | (11) |
| greaters#(x,.(y,z)) | → | greaters#(x,z) | (12) |
The dependency pairs are split into 2 components.
| greaters#(x,.(y,z)) | → | greaters#(x,z) | (12) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| greaters#(x,.(y,z)) | → | greaters#(x,z) | (12) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| lowers#(x,.(y,z)) | → | lowers#(x,z) | (11) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| lowers#(x,.(y,z)) | → | lowers#(x,z) | (11) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.