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(x,nil)) | → | x | (8) |
| min(cons(n,cons(m,x))) | → | if_min(le(n,m),cons(n,cons(m,x))) | (9) |
| if_min(true,cons(n,cons(m,x))) | → | min(cons(n,x)) | (10) |
| if_min(false,cons(n,cons(m,x))) | → | min(cons(m,x)) | (11) |
| replace(n,m,nil) | → | nil | (12) |
| replace(n,m,cons(k,x)) | → | if_replace(eq(n,k),n,m,cons(k,x)) | (13) |
| if_replace(true,n,m,cons(k,x)) | → | cons(m,x) | (14) |
| if_replace(false,n,m,cons(k,x)) | → | cons(k,replace(n,m,x)) | (15) |
| empty(nil) | → | true | (16) |
| empty(cons(n,x)) | → | false | (17) |
| head(cons(n,x)) | → | n | (18) |
| tail(nil) | → | nil | (19) |
| tail(cons(n,x)) | → | x | (20) |
| sort(x) | → | sortIter(x,nil) | (21) |
| sortIter(x,y) | → | if(empty(x),x,y,append(y,cons(min(x),nil))) | (22) |
| if(true,x,y,z) | → | y | (23) |
| if(false,x,y,z) | → | sortIter(replace(min(x),head(x),tail(x)),z) | (24) |
| eq#(s(n),s(m)) | → | eq#(n,m) | (25) |
| le#(s(n),s(m)) | → | le#(n,m) | (26) |
| min#(cons(n,cons(m,x))) | → | le#(n,m) | (27) |
| min#(cons(n,cons(m,x))) | → | if_min#(le(n,m),cons(n,cons(m,x))) | (28) |
| if_min#(true,cons(n,cons(m,x))) | → | min#(cons(n,x)) | (29) |
| if_min#(false,cons(n,cons(m,x))) | → | min#(cons(m,x)) | (30) |
| replace#(n,m,cons(k,x)) | → | eq#(n,k) | (31) |
| replace#(n,m,cons(k,x)) | → | if_replace#(eq(n,k),n,m,cons(k,x)) | (32) |
| if_replace#(false,n,m,cons(k,x)) | → | replace#(n,m,x) | (33) |
| sort#(x) | → | sortIter#(x,nil) | (34) |
| sortIter#(x,y) | → | min#(x) | (35) |
| sortIter#(x,y) | → | empty#(x) | (36) |
| sortIter#(x,y) | → | if#(empty(x),x,y,append(y,cons(min(x),nil))) | (37) |
| if#(false,x,y,z) | → | tail#(x) | (38) |
| if#(false,x,y,z) | → | head#(x) | (39) |
| if#(false,x,y,z) | → | min#(x) | (40) |
| if#(false,x,y,z) | → | replace#(min(x),head(x),tail(x)) | (41) |
| if#(false,x,y,z) | → | sortIter#(replace(min(x),head(x),tail(x)),z) | (42) |
The dependency pairs are split into 5 components.
| if#(false,x,y,z) | → | sortIter#(replace(min(x),head(x),tail(x)),z) | (42) |
| sortIter#(x,y) | → | if#(empty(x),x,y,append(y,cons(min(x),nil))) | (37) |
| [false] | = | 3 |
| [min(x1)] | = | 0 · x1 + 1/2 |
| [eq(x1, x2)] | = | 0 · x1 + 0 · x2 + 0 |
| [s(x1)] | = | 2 · x1 + 0 |
| [append(x1, x2)] | = | 0 · x1 + 2 · x2 + 0 |
| [le(x1, x2)] | = | 1 · x1 + 7/2 · x2 + 1 |
| [replace(x1, x2, x3)] | = | 0 · x1 + 0 · x2 + 1 · x3 + 0 |
| [0] | = | 0 |
| [cons(x1, x2)] | = | 0 · x1 + 2 · x2 + 3 |
| [if#(x1,...,x4)] | = | 1/2 · x1 + 1/2 · x2 + 0 · x3 + 0 · x4 + 0 |
| [tail(x1)] | = | 1/2 · x1 + 1 |
| [empty(x1)] | = | 1 · x1 + 0 |
| [if_replace(x1,...,x4)] | = | 0 · x1 + 0 · x2 + 0 · x3 + 1 · x4 + 0 |
| [if_min(x1, x2)] | = | 3 · x1 + 0 · x2 + 2 |
| [head(x1)] | = | 0 · x1 + 0 |
| [nil] | = | 0 |
| [sortIter#(x1, x2)] | = | 1 · x1 + 0 · x2 + 1/2 |
| [true] | = | 0 |
| tail(nil) | → | nil | (19) |
| tail(cons(n,x)) | → | x | (20) |
| replace(n,m,nil) | → | nil | (12) |
| replace(n,m,cons(k,x)) | → | if_replace(eq(n,k),n,m,cons(k,x)) | (13) |
| if_replace(true,n,m,cons(k,x)) | → | cons(m,x) | (14) |
| if_replace(false,n,m,cons(k,x)) | → | cons(k,replace(n,m,x)) | (15) |
| empty(nil) | → | true | (16) |
| empty(cons(n,x)) | → | false | (17) |
| sortIter#(x,y) | → | if#(empty(x),x,y,append(y,cons(min(x),nil))) | (37) |
The dependency pairs are split into 0 components.
| replace#(n,m,cons(k,x)) | → | if_replace#(eq(n,k),n,m,cons(k,x)) | (32) |
| if_replace#(false,n,m,cons(k,x)) | → | replace#(n,m,x) | (33) |
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)) | (32) |
| 3 | ≥ | 4 | |
| 2 | ≥ | 3 | |
| 1 | ≥ | 2 | |
| if_replace#(false,n,m,cons(k,x)) | → | replace#(n,m,x) | (33) |
| 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) | (25) |
| π(eq#) | = | 1 |
| eq#(s(n),s(m)) | → | eq#(n,m) | (25) |
There are no pairs anymore.
| min#(cons(n,cons(m,x))) | → | if_min#(le(n,m),cons(n,cons(m,x))) | (28) |
| if_min#(true,cons(n,cons(m,x))) | → | min#(cons(n,x)) | (29) |
| if_min#(false,cons(n,cons(m,x))) | → | min#(cons(m,x)) | (30) |
| π(if_min#) | = | { 2, 2 } |
| π(min#) | = | { 1, 1 } |
| π(append) | = | { 1, 1 } |
| π(cons) | = | { 1, 1, 2 } |
| if_min#(true,cons(n,cons(m,x))) | → | min#(cons(n,x)) | (29) |
| if_min#(false,cons(n,cons(m,x))) | → | min#(cons(m,x)) | (30) |
The dependency pairs are split into 0 components.
| le#(s(n),s(m)) | → | le#(n,m) | (26) |
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) | (26) |
| 2 | > | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.