The rewrite relation of the following conditional TRS is considered.
| le(0,x) | → | true | |
| le(s(x),0) | → | false | |
| le(s(x),s(y)) | → | le(x,y) | |
| app(nil,x) | → | x | |
| app(cons(x,xs),ys) | → | cons(x,app(xs,ys)) | |
| split(x,nil) | → | pair(nil,nil) | |
| qsort(nil) | → | nil | |
| split(x,cons(y,ys)) | → | pair(xs,cons(y,zs)) | | split(x,ys) ≈ pair(xs,zs), le(x,y) ≈ true |
| split(x,cons(y,ys)) | → | pair(cons(y,xs),zs) | | split(x,ys) ≈ pair(xs,zs), le(x,y) ≈ false |
| qsort(cons(x,xs)) | → | app(qsort(ys),cons(x,qsort(zs))) | | split(x,xs) ≈ pair(ys,zs) |