The rewrite relation of the following TRS is considered.
| minus(x,0) | → | x | (1) |
| minus(s(x),s(y)) | → | minus(x,y) | (2) |
| quot(0,s(y)) | → | 0 | (3) |
| quot(s(x),s(y)) | → | s(quot(minus(x,y),s(y))) | (4) |
| le(0,y) | → | true | (5) |
| le(s(x),0) | → | false | (6) |
| le(s(x),s(y)) | → | le(x,y) | (7) |
| app(nil,y) | → | y | (8) |
| app(add(n,x),y) | → | add(n,app(x,y)) | (9) |
| low(n,nil) | → | nil | (10) |
| low(n,add(m,x)) | → | if_low(le(m,n),n,add(m,x)) | (11) |
| if_low(true,n,add(m,x)) | → | add(m,low(n,x)) | (12) |
| if_low(false,n,add(m,x)) | → | low(n,x) | (13) |
| high(n,nil) | → | nil | (14) |
| high(n,add(m,x)) | → | if_high(le(m,n),n,add(m,x)) | (15) |
| if_high(true,n,add(m,x)) | → | high(n,x) | (16) |
| if_high(false,n,add(m,x)) | → | add(m,high(n,x)) | (17) |
| quicksort(nil) | → | nil | (18) |
| quicksort(add(n,x)) | → | app(quicksort(low(n,x)),add(n,quicksort(high(n,x)))) | (19) |
| minus#(s(x),s(y)) | → | minus#(x,y) | (20) |
| quot#(s(x),s(y)) | → | minus#(x,y) | (21) |
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (22) |
| le#(s(x),s(y)) | → | le#(x,y) | (23) |
| app#(add(n,x),y) | → | app#(x,y) | (24) |
| low#(n,add(m,x)) | → | le#(m,n) | (25) |
| low#(n,add(m,x)) | → | if_low#(le(m,n),n,add(m,x)) | (26) |
| if_low#(true,n,add(m,x)) | → | low#(n,x) | (27) |
| if_low#(false,n,add(m,x)) | → | low#(n,x) | (28) |
| high#(n,add(m,x)) | → | le#(m,n) | (29) |
| high#(n,add(m,x)) | → | if_high#(le(m,n),n,add(m,x)) | (30) |
| if_high#(true,n,add(m,x)) | → | high#(n,x) | (31) |
| if_high#(false,n,add(m,x)) | → | high#(n,x) | (32) |
| quicksort#(add(n,x)) | → | high#(n,x) | (33) |
| quicksort#(add(n,x)) | → | quicksort#(high(n,x)) | (34) |
| quicksort#(add(n,x)) | → | low#(n,x) | (35) |
| quicksort#(add(n,x)) | → | quicksort#(low(n,x)) | (36) |
| quicksort#(add(n,x)) | → | app#(quicksort(low(n,x)),add(n,quicksort(high(n,x)))) | (37) |
The dependency pairs are split into 7 components.
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (22) |
| π(quot#) | = | { 1 } |
| π(minus) | = | { 1 } |
| quot#(s(x),s(y)) | → | quot#(minus(x,y),s(y)) | (22) |
There are no pairs anymore.
| minus#(s(x),s(y)) | → | minus#(x,y) | (20) |
| π(minus#) | = | 1 |
| minus#(s(x),s(y)) | → | minus#(x,y) | (20) |
There are no pairs anymore.
| quicksort#(add(n,x)) | → | quicksort#(high(n,x)) | (34) |
| quicksort#(add(n,x)) | → | quicksort#(low(n,x)) | (36) |
| prec(quicksort#) | = | 0 | stat(quicksort#) | = | lex | |
| prec(if_high) | = | 0 | stat(if_high) | = | lex | |
| prec(high) | = | 0 | stat(high) | = | lex | |
| prec(if_low) | = | 0 | stat(if_low) | = | lex | |
| prec(low) | = | 0 | stat(low) | = | lex | |
| prec(add) | = | 0 | stat(add) | = | lex | |
| prec(nil) | = | 0 | stat(nil) | = | lex | |
| prec(false) | = | 0 | stat(false) | = | lex | |
| prec(true) | = | 0 | stat(true) | = | lex | |
| prec(le) | = | 0 | stat(le) | = | lex | |
| prec(s) | = | 0 | stat(s) | = | lex | |
| prec(0) | = | 0 | stat(0) | = | lex |
| π(quicksort#) | = | 1 |
| π(if_high) | = | 3 |
| π(high) | = | 2 |
| π(if_low) | = | 3 |
| π(low) | = | 2 |
| π(add) | = | [2] |
| π(nil) | = | [] |
| π(false) | = | [] |
| π(true) | = | [] |
| π(le) | = | [] |
| π(s) | = | 1 |
| π(0) | = | [] |
| high(n,nil) | → | nil | (14) |
| high(n,add(m,x)) | → | if_high(le(m,n),n,add(m,x)) | (15) |
| if_high(true,n,add(m,x)) | → | high(n,x) | (16) |
| if_high(false,n,add(m,x)) | → | add(m,high(n,x)) | (17) |
| low(n,nil) | → | nil | (10) |
| low(n,add(m,x)) | → | if_low(le(m,n),n,add(m,x)) | (11) |
| if_low(true,n,add(m,x)) | → | add(m,low(n,x)) | (12) |
| if_low(false,n,add(m,x)) | → | low(n,x) | (13) |
| quicksort#(add(n,x)) | → | quicksort#(high(n,x)) | (34) |
| quicksort#(add(n,x)) | → | quicksort#(low(n,x)) | (36) |
There are no pairs anymore.
| app#(add(n,x),y) | → | app#(x,y) | (24) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(add(n,x),y) | → | app#(x,y) | (24) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| low#(n,add(m,x)) | → | if_low#(le(m,n),n,add(m,x)) | (26) |
| if_low#(true,n,add(m,x)) | → | low#(n,x) | (27) |
| if_low#(false,n,add(m,x)) | → | low#(n,x) | (28) |
| π(if_low#) | = | 3 |
| π(low#) | = | 2 |
| if_low#(true,n,add(m,x)) | → | low#(n,x) | (27) |
| if_low#(false,n,add(m,x)) | → | low#(n,x) | (28) |
The dependency pairs are split into 0 components.
| high#(n,add(m,x)) | → | if_high#(le(m,n),n,add(m,x)) | (30) |
| if_high#(true,n,add(m,x)) | → | high#(n,x) | (31) |
| if_high#(false,n,add(m,x)) | → | high#(n,x) | (32) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| high#(n,add(m,x)) | → | if_high#(le(m,n),n,add(m,x)) | (30) |
| 2 | ≥ | 3 | |
| 1 | ≥ | 2 | |
| if_high#(true,n,add(m,x)) | → | high#(n,x) | (31) |
| 3 | > | 2 | |
| 2 | ≥ | 1 | |
| if_high#(false,n,add(m,x)) | → | high#(n,x) | (32) |
| 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) | (23) |
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) | (23) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.