The rewrite relation of the following TRS is considered.
| le(0,Y) | → | true | (1) |
| le(s(X),0) | → | false | (2) |
| le(s(X),s(Y)) | → | le(X,Y) | (3) |
| app(nil,Y) | → | Y | (4) |
| app(cons(N,L),Y) | → | cons(N,app(L,Y)) | (5) |
| low(N,nil) | → | nil | (6) |
| low(N,cons(M,L)) | → | iflow(le(M,N),N,cons(M,L)) | (7) |
| iflow(true,N,cons(M,L)) | → | cons(M,low(N,L)) | (8) |
| iflow(false,N,cons(M,L)) | → | low(N,L) | (9) |
| high(N,nil) | → | nil | (10) |
| high(N,cons(M,L)) | → | ifhigh(le(M,N),N,cons(M,L)) | (11) |
| ifhigh(true,N,cons(M,L)) | → | high(N,L) | (12) |
| ifhigh(false,N,cons(M,L)) | → | cons(M,high(N,L)) | (13) |
| quicksort(nil) | → | nil | (14) |
| quicksort(cons(N,L)) | → | app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) | (15) |
| le#(s(X),s(Y)) | → | le#(X,Y) | (16) |
| app#(cons(N,L),Y) | → | app#(L,Y) | (17) |
| low#(N,cons(M,L)) | → | le#(M,N) | (18) |
| low#(N,cons(M,L)) | → | iflow#(le(M,N),N,cons(M,L)) | (19) |
| iflow#(true,N,cons(M,L)) | → | low#(N,L) | (20) |
| iflow#(false,N,cons(M,L)) | → | low#(N,L) | (21) |
| high#(N,cons(M,L)) | → | le#(M,N) | (22) |
| high#(N,cons(M,L)) | → | ifhigh#(le(M,N),N,cons(M,L)) | (23) |
| ifhigh#(true,N,cons(M,L)) | → | high#(N,L) | (24) |
| ifhigh#(false,N,cons(M,L)) | → | high#(N,L) | (25) |
| quicksort#(cons(N,L)) | → | high#(N,L) | (26) |
| quicksort#(cons(N,L)) | → | quicksort#(high(N,L)) | (27) |
| quicksort#(cons(N,L)) | → | low#(N,L) | (28) |
| quicksort#(cons(N,L)) | → | quicksort#(low(N,L)) | (29) |
| quicksort#(cons(N,L)) | → | app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) | (30) |
The dependency pairs are split into 5 components.
| quicksort#(cons(N,L)) | → | quicksort#(high(N,L)) | (27) |
| quicksort#(cons(N,L)) | → | quicksort#(low(N,L)) | (29) |
| π(quicksort#) | = | { 1 } |
| π(ifhigh) | = | { 3 } |
| π(high) | = | { 2 } |
| π(iflow) | = | { 3 } |
| π(low) | = | { 2 } |
| π(cons) | = | { 1, 1, 1, 2 } |
| quicksort#(cons(N,L)) | → | quicksort#(high(N,L)) | (27) |
| quicksort#(cons(N,L)) | → | quicksort#(low(N,L)) | (29) |
There are no pairs anymore.
| app#(cons(N,L),Y) | → | app#(L,Y) | (17) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(cons(N,L),Y) | → | app#(L,Y) | (17) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| low#(N,cons(M,L)) | → | iflow#(le(M,N),N,cons(M,L)) | (19) |
| iflow#(true,N,cons(M,L)) | → | low#(N,L) | (20) |
| iflow#(false,N,cons(M,L)) | → | low#(N,L) | (21) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| low#(N,cons(M,L)) | → | iflow#(le(M,N),N,cons(M,L)) | (19) |
| 2 | ≥ | 3 | |
| 1 | ≥ | 2 | |
| iflow#(true,N,cons(M,L)) | → | low#(N,L) | (20) |
| 3 | > | 2 | |
| 2 | ≥ | 1 | |
| iflow#(false,N,cons(M,L)) | → | low#(N,L) | (21) |
| 3 | > | 2 | |
| 2 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| high#(N,cons(M,L)) | → | ifhigh#(le(M,N),N,cons(M,L)) | (23) |
| ifhigh#(true,N,cons(M,L)) | → | high#(N,L) | (24) |
| ifhigh#(false,N,cons(M,L)) | → | high#(N,L) | (25) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| high#(N,cons(M,L)) | → | ifhigh#(le(M,N),N,cons(M,L)) | (23) |
| 2 | ≥ | 3 | |
| 1 | ≥ | 2 | |
| ifhigh#(true,N,cons(M,L)) | → | high#(N,L) | (24) |
| 3 | > | 2 | |
| 2 | ≥ | 1 | |
| ifhigh#(false,N,cons(M,L)) | → | high#(N,L) | (25) |
| 3 | > | 2 | |
| 2 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| le#(s(X),s(Y)) | → | le#(X,Y) | (16) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| le#(s(X),s(Y)) | → | le#(X,Y) | (16) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.