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