The rewrite relation of the following TRS is considered.
eq(0,0) | → | true | (1) |
eq(0,s(Y)) | → | 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) |
min(cons(0,nil)) | → | 0 | (8) |
min(cons(s(N),nil)) | → | s(N) | (9) |
min(cons(N,cons(M,L))) | → | ifmin(le(N,M),cons(N,cons(M,L))) | (10) |
ifmin(true,cons(N,cons(M,L))) | → | min(cons(N,L)) | (11) |
ifmin(false,cons(N,cons(M,L))) | → | min(cons(M,L)) | (12) |
replace(N,M,nil) | → | nil | (13) |
replace(N,M,cons(K,L)) | → | ifrepl(eq(N,K),N,M,cons(K,L)) | (14) |
ifrepl(true,N,M,cons(K,L)) | → | cons(M,L) | (15) |
ifrepl(false,N,M,cons(K,L)) | → | cons(K,replace(N,M,L)) | (16) |
selsort(nil) | → | nil | (17) |
selsort(cons(N,L)) | → | ifselsort(eq(N,min(cons(N,L))),cons(N,L)) | (18) |
ifselsort(true,cons(N,L)) | → | cons(N,selsort(L)) | (19) |
ifselsort(false,cons(N,L)) | → | cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) | (20) |
ifmin#(false,cons(N,cons(M,L))) | → | min#(cons(M,L)) | (21) |
ifselsort#(false,cons(N,L)) | → | selsort#(replace(min(cons(N,L)),N,L)) | (22) |
ifrepl#(false,N,M,cons(K,L)) | → | replace#(N,M,L) | (23) |
le#(s(X),s(Y)) | → | le#(X,Y) | (24) |
min#(cons(N,cons(M,L))) | → | le#(N,M) | (25) |
ifselsort#(true,cons(N,L)) | → | selsort#(L) | (26) |
eq#(s(X),s(Y)) | → | eq#(X,Y) | (27) |
ifselsort#(false,cons(N,L)) | → | replace#(min(cons(N,L)),N,L) | (28) |
min#(cons(N,cons(M,L))) | → | ifmin#(le(N,M),cons(N,cons(M,L))) | (29) |
ifselsort#(false,cons(N,L)) | → | min#(cons(N,L)) | (30) |
selsort#(cons(N,L)) | → | min#(cons(N,L)) | (31) |
selsort#(cons(N,L)) | → | eq#(N,min(cons(N,L))) | (32) |
replace#(N,M,cons(K,L)) | → | ifrepl#(eq(N,K),N,M,cons(K,L)) | (33) |
ifmin#(true,cons(N,cons(M,L))) | → | min#(cons(N,L)) | (34) |
ifselsort#(false,cons(N,L)) | → | min#(cons(N,L)) | (30) |
selsort#(cons(N,L)) | → | ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) | (35) |
replace#(N,M,cons(K,L)) | → | eq#(N,K) | (36) |
The dependency pairs are split into 5 components.
selsort#(cons(N,L)) | → | ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) | (35) |
ifselsort#(true,cons(N,L)) | → | selsort#(L) | (26) |
ifselsort#(false,cons(N,L)) | → | selsort#(replace(min(cons(N,L)),N,L)) | (22) |
[ifselsort(x1, x2)] | = | 0 |
[le(x1, x2)] | = | x2 + 4 |
[s(x1)] | = | x1 + 43374 |
[le#(x1, x2)] | = | 0 |
[ifmin(x1, x2)] | = | x1 + x2 + 0 |
[eq(x1, x2)] | = | 20543 |
[false] | = | 6 |
[min#(x1)] | = | 0 |
[true] | = | 2 |
[eq#(x1, x2)] | = | 0 |
[0] | = | 1 |
[nil] | = | 28382 |
[ifrepl(x1,...,x4)] | = | x4 + 1146 |
[selsort(x1)] | = | 0 |
[ifrepl#(x1,...,x4)] | = | 0 |
[selsort#(x1)] | = | x1 + 20544 |
[replace#(x1, x2, x3)] | = | 0 |
[ifselsort#(x1, x2)] | = | x1 + x2 + 0 |
[min(x1)] | = | 43373 |
[cons(x1, x2)] | = | x2 + 21685 |
[ifmin#(x1, x2)] | = | 0 |
[replace(x1, x2, x3)] | = | x3 + 1146 |
eq(s(X),s(Y)) | → | eq(X,Y) | (4) |
ifrepl(true,N,M,cons(K,L)) | → | cons(M,L) | (15) |
eq(0,0) | → | true | (1) |
eq(s(X),0) | → | false | (3) |
ifrepl(false,N,M,cons(K,L)) | → | cons(K,replace(N,M,L)) | (16) |
replace(N,M,cons(K,L)) | → | ifrepl(eq(N,K),N,M,cons(K,L)) | (14) |
replace(N,M,nil) | → | nil | (13) |
eq(0,s(Y)) | → | false | (2) |
selsort#(cons(N,L)) | → | ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) | (35) |
ifselsort#(true,cons(N,L)) | → | selsort#(L) | (26) |
ifselsort#(false,cons(N,L)) | → | selsort#(replace(min(cons(N,L)),N,L)) | (22) |
The dependency pairs are split into 0 components.
replace#(N,M,cons(K,L)) | → | ifrepl#(eq(N,K),N,M,cons(K,L)) | (33) |
ifrepl#(false,N,M,cons(K,L)) | → | replace#(N,M,L) | (23) |
[ifselsort(x1, x2)] | = | 0 |
[le(x1, x2)] | = | x2 + 4 |
[s(x1)] | = | x1 + 43374 |
[le#(x1, x2)] | = | 0 |
[ifmin(x1, x2)] | = | x1 + x2 + 0 |
[eq(x1, x2)] | = | 6 |
[false] | = | 6 |
[min#(x1)] | = | 0 |
[true] | = | 2 |
[eq#(x1, x2)] | = | 0 |
[0] | = | 1 |
[nil] | = | 35231 |
[ifrepl(x1,...,x4)] | = | x4 + 1146 |
[selsort(x1)] | = | 0 |
[ifrepl#(x1,...,x4)] | = | x1 + x4 + 0 |
[selsort#(x1)] | = | x1 + 20544 |
[replace#(x1, x2, x3)] | = | x3 + 7 |
[ifselsort#(x1, x2)] | = | x1 + 0 |
[min(x1)] | = | 7 |
[cons(x1, x2)] | = | x2 + 2 |
[ifmin#(x1, x2)] | = | 0 |
[replace(x1, x2, x3)] | = | x3 + 1146 |
eq(s(X),s(Y)) | → | eq(X,Y) | (4) |
ifrepl(true,N,M,cons(K,L)) | → | cons(M,L) | (15) |
eq(0,0) | → | true | (1) |
eq(s(X),0) | → | false | (3) |
ifrepl(false,N,M,cons(K,L)) | → | cons(K,replace(N,M,L)) | (16) |
replace(N,M,cons(K,L)) | → | ifrepl(eq(N,K),N,M,cons(K,L)) | (14) |
replace(N,M,nil) | → | nil | (13) |
eq(0,s(Y)) | → | false | (2) |
replace#(N,M,cons(K,L)) | → | ifrepl#(eq(N,K),N,M,cons(K,L)) | (33) |
ifrepl#(false,N,M,cons(K,L)) | → | replace#(N,M,L) | (23) |
The dependency pairs are split into 0 components.
eq#(s(X),s(Y)) | → | eq#(X,Y) | (27) |
[ifselsort(x1, x2)] | = | 0 |
[le(x1, x2)] | = | x2 + 3 |
[s(x1)] | = | x1 + 43371 |
[le#(x1, x2)] | = | 0 |
[ifmin(x1, x2)] | = | x1 + x2 + 0 |
[eq(x1, x2)] | = | 5 |
[false] | = | 5 |
[min#(x1)] | = | 0 |
[true] | = | 1 |
[eq#(x1, x2)] | = | x2 + 0 |
[0] | = | 1 |
[nil] | = | 54788 |
[ifrepl(x1,...,x4)] | = | x4 + 19781 |
[selsort(x1)] | = | 0 |
[ifrepl#(x1,...,x4)] | = | x1 + 0 |
[selsort#(x1)] | = | x1 + 20544 |
[replace#(x1, x2, x3)] | = | 7 |
[ifselsort#(x1, x2)] | = | x1 + 0 |
[min(x1)] | = | 4 |
[cons(x1, x2)] | = | x2 + 1 |
[ifmin#(x1, x2)] | = | 0 |
[replace(x1, x2, x3)] | = | x3 + 19781 |
eq(s(X),s(Y)) | → | eq(X,Y) | (4) |
ifrepl(true,N,M,cons(K,L)) | → | cons(M,L) | (15) |
eq(0,0) | → | true | (1) |
eq(s(X),0) | → | false | (3) |
ifrepl(false,N,M,cons(K,L)) | → | cons(K,replace(N,M,L)) | (16) |
replace(N,M,cons(K,L)) | → | ifrepl(eq(N,K),N,M,cons(K,L)) | (14) |
replace(N,M,nil) | → | nil | (13) |
eq(0,s(Y)) | → | false | (2) |
eq#(s(X),s(Y)) | → | eq#(X,Y) | (27) |
The dependency pairs are split into 0 components.
ifmin#(true,cons(N,cons(M,L))) | → | min#(cons(N,L)) | (34) |
min#(cons(N,cons(M,L))) | → | ifmin#(le(N,M),cons(N,cons(M,L))) | (29) |
ifmin#(false,cons(N,cons(M,L))) | → | min#(cons(M,L)) | (21) |
[ifselsort(x1, x2)] | = | 0 |
[le(x1, x2)] | = | x2 + 3 |
[s(x1)] | = | x1 + 43373 |
[le#(x1, x2)] | = | 0 |
[ifmin(x1, x2)] | = | x1 + x2 + 0 |
[eq(x1, x2)] | = | 1 |
[false] | = | 0 |
[min#(x1)] | = | x1 + 1 |
[true] | = | 1 |
[eq#(x1, x2)] | = | 0 |
[0] | = | 1 |
[nil] | = | 54788 |
[ifrepl(x1,...,x4)] | = | x4 + 19781 |
[selsort(x1)] | = | 0 |
[ifrepl#(x1,...,x4)] | = | x1 + 0 |
[selsort#(x1)] | = | x1 + 20544 |
[replace#(x1, x2, x3)] | = | 7 |
[ifselsort#(x1, x2)] | = | x1 + 0 |
[min(x1)] | = | 6 |
[cons(x1, x2)] | = | x2 + 2 |
[ifmin#(x1, x2)] | = | x2 + 0 |
[replace(x1, x2, x3)] | = | x3 + 19781 |
eq(s(X),s(Y)) | → | eq(X,Y) | (4) |
ifrepl(true,N,M,cons(K,L)) | → | cons(M,L) | (15) |
eq(0,0) | → | true | (1) |
eq(s(X),0) | → | false | (3) |
ifrepl(false,N,M,cons(K,L)) | → | cons(K,replace(N,M,L)) | (16) |
le(0,Y) | → | true | (5) |
le(s(X),s(Y)) | → | le(X,Y) | (7) |
replace(N,M,cons(K,L)) | → | ifrepl(eq(N,K),N,M,cons(K,L)) | (14) |
replace(N,M,nil) | → | nil | (13) |
le(s(X),0) | → | false | (6) |
eq(0,s(Y)) | → | false | (2) |
ifmin#(true,cons(N,cons(M,L))) | → | min#(cons(N,L)) | (34) |
min#(cons(N,cons(M,L))) | → | ifmin#(le(N,M),cons(N,cons(M,L))) | (29) |
ifmin#(false,cons(N,cons(M,L))) | → | min#(cons(M,L)) | (21) |
The dependency pairs are split into 0 components.
le#(s(X),s(Y)) | → | le#(X,Y) | (24) |
[ifselsort(x1, x2)] | = | 0 |
[le(x1, x2)] | = | x2 + 3 |
[s(x1)] | = | x1 + 43371 |
[le#(x1, x2)] | = | x2 + 0 |
[ifmin(x1, x2)] | = | x1 + x2 + 0 |
[eq(x1, x2)] | = | 1 |
[false] | = | 0 |
[min#(x1)] | = | 1 |
[true] | = | 1 |
[eq#(x1, x2)] | = | 0 |
[0] | = | 1 |
[nil] | = | 33694 |
[ifrepl(x1,...,x4)] | = | x4 + 36229 |
[selsort(x1)] | = | 0 |
[ifrepl#(x1,...,x4)] | = | x1 + 0 |
[selsort#(x1)] | = | x1 + 20544 |
[replace#(x1, x2, x3)] | = | 7 |
[ifselsort#(x1, x2)] | = | x1 + 0 |
[min(x1)] | = | 4 |
[cons(x1, x2)] | = | x2 + 1 |
[ifmin#(x1, x2)] | = | 0 |
[replace(x1, x2, x3)] | = | x3 + 36229 |
eq(s(X),s(Y)) | → | eq(X,Y) | (4) |
ifrepl(true,N,M,cons(K,L)) | → | cons(M,L) | (15) |
eq(0,0) | → | true | (1) |
eq(s(X),0) | → | false | (3) |
ifrepl(false,N,M,cons(K,L)) | → | cons(K,replace(N,M,L)) | (16) |
le(0,Y) | → | true | (5) |
le(s(X),s(Y)) | → | le(X,Y) | (7) |
replace(N,M,cons(K,L)) | → | ifrepl(eq(N,K),N,M,cons(K,L)) | (14) |
replace(N,M,nil) | → | nil | (13) |
le(s(X),0) | → | false | (6) |
eq(0,s(Y)) | → | false | (2) |
le#(s(X),s(Y)) | → | le#(X,Y) | (24) |
The dependency pairs are split into 0 components.