The rewrite relation of the following TRS is considered.
| eq(0,0) | → | true | (1) |
| eq(0,s(m)) | → | false | (2) |
| eq(s(n),0) | → | false | (3) |
| eq(s(n),s(m)) | → | eq(n,m) | (4) |
| le(0,m) | → | true | (5) |
| le(s(n),0) | → | false | (6) |
| le(s(n),s(m)) | → | le(n,m) | (7) |
| min(cons(0,nil)) | → | 0 | (8) |
| min(cons(s(n),nil)) | → | s(n) | (9) |
| min(cons(n,cons(m,x))) | → | if_min(le(n,m),cons(n,cons(m,x))) | (10) |
| if_min(true,cons(n,cons(m,x))) | → | min(cons(n,x)) | (11) |
| if_min(false,cons(n,cons(m,x))) | → | min(cons(m,x)) | (12) |
| replace(n,m,nil) | → | nil | (13) |
| replace(n,m,cons(k,x)) | → | if_replace(eq(n,k),n,m,cons(k,x)) | (14) |
| if_replace(true,n,m,cons(k,x)) | → | cons(m,x) | (15) |
| if_replace(false,n,m,cons(k,x)) | → | cons(k,replace(n,m,x)) | (16) |
| sort(nil) | → | nil | (17) |
| sort(cons(n,x)) | → | cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x))) | (18) |
| eq#(s(n),s(m)) | → | eq#(n,m) | (19) |
| le#(s(n),s(m)) | → | le#(n,m) | (20) |
| min#(cons(n,cons(m,x))) | → | le#(n,m) | (21) |
| min#(cons(n,cons(m,x))) | → | if_min#(le(n,m),cons(n,cons(m,x))) | (22) |
| if_min#(true,cons(n,cons(m,x))) | → | min#(cons(n,x)) | (23) |
| if_min#(false,cons(n,cons(m,x))) | → | min#(cons(m,x)) | (24) |
| replace#(n,m,cons(k,x)) | → | eq#(n,k) | (25) |
| replace#(n,m,cons(k,x)) | → | if_replace#(eq(n,k),n,m,cons(k,x)) | (26) |
| if_replace#(false,n,m,cons(k,x)) | → | replace#(n,m,x) | (27) |
| sort#(cons(n,x)) | → | replace#(min(cons(n,x)),n,x) | (28) |
| sort#(cons(n,x)) | → | sort#(replace(min(cons(n,x)),n,x)) | (29) |
| sort#(cons(n,x)) | → | min#(cons(n,x)) | (30) |
The dependency pairs are split into 5 components.
| sort#(cons(n,x)) | → | sort#(replace(min(cons(n,x)),n,x)) | (29) |
| prec(sort#) | = | 0 | stat(sort#) | = | lex | |
| prec(if_replace) | = | 0 | stat(if_replace) | = | lex | |
| prec(replace) | = | 0 | stat(replace) | = | lex | |
| prec(if_min) | = | 0 | stat(if_min) | = | lex | |
| prec(min) | = | 0 | stat(min) | = | lex | |
| prec(cons) | = | 0 | stat(cons) | = | lex | |
| prec(nil) | = | 0 | stat(nil) | = | lex | |
| prec(le) | = | 0 | stat(le) | = | lex | |
| prec(false) | = | 0 | stat(false) | = | lex | |
| prec(s) | = | 0 | stat(s) | = | lex | |
| prec(true) | = | 0 | stat(true) | = | lex | |
| prec(eq) | = | 0 | stat(eq) | = | lex | |
| prec(0) | = | 0 | stat(0) | = | lex |
| π(sort#) | = | 1 |
| π(if_replace) | = | 4 |
| π(replace) | = | 3 |
| π(if_min) | = | 2 |
| π(min) | = | 1 |
| π(cons) | = | [2] |
| π(nil) | = | [] |
| π(le) | = | 2 |
| π(false) | = | [] |
| π(s) | = | 1 |
| π(true) | = | [] |
| π(eq) | = | 1 |
| π(0) | = | [] |
| replace(n,m,nil) | → | nil | (13) |
| replace(n,m,cons(k,x)) | → | if_replace(eq(n,k),n,m,cons(k,x)) | (14) |
| if_replace(true,n,m,cons(k,x)) | → | cons(m,x) | (15) |
| if_replace(false,n,m,cons(k,x)) | → | cons(k,replace(n,m,x)) | (16) |
| sort#(cons(n,x)) | → | sort#(replace(min(cons(n,x)),n,x)) | (29) |
There are no pairs anymore.
| min#(cons(n,cons(m,x))) | → | if_min#(le(n,m),cons(n,cons(m,x))) | (22) |
| if_min#(true,cons(n,cons(m,x))) | → | min#(cons(n,x)) | (23) |
| if_min#(false,cons(n,cons(m,x))) | → | min#(cons(m,x)) | (24) |
| [false] | = | 7 |
| [min#(x1)] | = | 4 · x1 + 0 |
| [s(x1)] | = | -∞ · x1 + 0 |
| [if_min#(x1, x2)] | = | -∞ · x1 + 3 · x2 + 4 |
| [le(x1, x2)] | = | 0 · x1 + 0 · x2 + -∞ |
| [0] | = | 0 |
| [cons(x1, x2)] | = | -∞ · x1 + 1 · x2 + 2 |
| [true] | = | 7 |
| min#(cons(n,cons(m,x))) | → | if_min#(le(n,m),cons(n,cons(m,x))) | (22) |
The dependency pairs are split into 0 components.
| le#(s(n),s(m)) | → | le#(n,m) | (20) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| le#(s(n),s(m)) | → | le#(n,m) | (20) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| replace#(n,m,cons(k,x)) | → | if_replace#(eq(n,k),n,m,cons(k,x)) | (26) |
| if_replace#(false,n,m,cons(k,x)) | → | replace#(n,m,x) | (27) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| replace#(n,m,cons(k,x)) | → | if_replace#(eq(n,k),n,m,cons(k,x)) | (26) |
| 3 | ≥ | 4 | |
| 2 | ≥ | 3 | |
| 1 | ≥ | 2 | |
| if_replace#(false,n,m,cons(k,x)) | → | replace#(n,m,x) | (27) |
| 4 | > | 3 | |
| 3 | ≥ | 2 | |
| 2 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| eq#(s(n),s(m)) | → | eq#(n,m) | (19) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| eq#(s(n),s(m)) | → | eq#(n,m) | (19) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.