The rewrite relation of the following TRS is considered.
dbl(0) | → | 0 | (1) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
dbls(nil) | → | nil | (3) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
indx(nil,X) | → | nil | (7) |
indx(cons(X,Y),Z) | → | cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) | (8) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
s(X) | → | n__s(X) | (10) |
dbl(X) | → | n__dbl(X) | (11) |
dbls(X) | → | n__dbls(X) | (12) |
sel(X1,X2) | → | n__sel(X1,X2) | (13) |
indx(X1,X2) | → | n__indx(X1,X2) | (14) |
from(X) | → | n__from(X) | (15) |
activate(n__s(X)) | → | s(X) | (16) |
activate(n__dbl(X)) | → | dbl(X) | (17) |
activate(n__dbls(X)) | → | dbls(X) | (18) |
activate(n__sel(X1,X2)) | → | sel(X1,X2) | (19) |
activate(n__indx(X1,X2)) | → | indx(X1,X2) | (20) |
activate(n__from(X)) | → | from(X) | (21) |
activate(X) | → | X | (22) |
dbl#(s(X)) | → | activate#(X) | (23) |
from#(X) | → | activate#(X) | (24) |
activate#(n__s(X)) | → | s#(X) | (25) |
sel#(0,cons(X,Y)) | → | activate#(X) | (26) |
activate#(n__sel(X1,X2)) | → | sel#(X1,X2) | (27) |
activate#(n__from(X)) | → | from#(X) | (28) |
indx#(cons(X,Y),Z) | → | activate#(X) | (29) |
activate#(n__dbls(X)) | → | dbls#(X) | (30) |
from#(X) | → | activate#(X) | (24) |
activate#(n__dbl(X)) | → | dbl#(X) | (31) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (32) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (33) |
dbls#(cons(X,Y)) | → | activate#(Y) | (34) |
indx#(cons(X,Y),Z) | → | activate#(Y) | (35) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (36) |
dbl#(s(X)) | → | s#(n__s(n__dbl(activate(X)))) | (37) |
activate#(n__indx(X1,X2)) | → | indx#(X1,X2) | (38) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (33) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (39) |
dbls#(cons(X,Y)) | → | activate#(X) | (40) |
The dependency pairs are split into 1 component.
dbls#(cons(X,Y)) | → | activate#(X) | (40) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (39) |
indx#(cons(X,Y),Z) | → | activate#(X) | (29) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (33) |
activate#(n__from(X)) | → | from#(X) | (28) |
activate#(n__indx(X1,X2)) | → | indx#(X1,X2) | (38) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (36) |
indx#(cons(X,Y),Z) | → | activate#(Y) | (35) |
activate#(n__sel(X1,X2)) | → | sel#(X1,X2) | (27) |
sel#(0,cons(X,Y)) | → | activate#(X) | (26) |
dbls#(cons(X,Y)) | → | activate#(Y) | (34) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (33) |
from#(X) | → | activate#(X) | (24) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (32) |
activate#(n__dbl(X)) | → | dbl#(X) | (31) |
from#(X) | → | activate#(X) | (24) |
dbl#(s(X)) | → | activate#(X) | (23) |
activate#(n__dbls(X)) | → | dbls#(X) | (30) |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 32287 |
[activate(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 32287 |
[indx(x1, x2)] | = | max(x1 + 5513, x2 + 11026, 0) |
[n__indx(x1, x2)] | = | max(x1 + 5513, x2 + 11026, 0) |
[n__from(x1)] | = | x1 + 8367 |
[dbl#(x1)] | = | x1 + 16305 |
[activate#(x1)] | = | x1 + 16304 |
[dbls#(x1)] | = | x1 + 16305 |
[n__dbls(x1)] | = | x1 + 32287 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 32287 |
[0] | = | 1 |
[sel#(x1, x2)] | = | max(x1 + 16304, x2 + 16304, 0) |
[indx#(x1, x2)] | = | max(x1 + 21816, x2 + 16305, 0) |
[sel(x1, x2)] | = | max(x1 + 5513, x2 + 0, 0) |
[from(x1)] | = | x1 + 8367 |
[s#(x1)] | = | 0 |
[nil] | = | 11027 |
[n__sel(x1, x2)] | = | max(x1 + 5513, x2 + 0, 0) |
[from#(x1)] | = | x1 + 24670 |
[cons(x1, x2)] | = | max(x1 + 5512, x2 + 0, 0) |
activate(n__dbls(X)) | → | dbls(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
from(X) | → | n__from(X) | (15) |
indx(cons(X,Y),Z) | → | cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) | (8) |
dbl(0) | → | 0 | (1) |
dbls(nil) | → | nil | (3) |
activate(n__s(X)) | → | s(X) | (16) |
activate(n__from(X)) | → | from(X) | (21) |
activate(n__sel(X1,X2)) | → | sel(X1,X2) | (19) |
activate(n__dbl(X)) | → | dbl(X) | (17) |
activate(X) | → | X | (22) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
s(X) | → | n__s(X) | (10) |
indx(nil,X) | → | nil | (7) |
activate(n__indx(X1,X2)) | → | indx(X1,X2) | (20) |
indx(X1,X2) | → | n__indx(X1,X2) | (14) |
dbls(X) | → | n__dbls(X) | (12) |
dbl(X) | → | n__dbl(X) | (11) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(X1,X2) | → | n__sel(X1,X2) | (13) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
dbls#(cons(X,Y)) | → | activate#(X) | (40) |
indx#(cons(X,Y),Z) | → | activate#(X) | (29) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (33) |
activate#(n__from(X)) | → | from#(X) | (28) |
activate#(n__indx(X1,X2)) | → | indx#(X1,X2) | (38) |
indx#(cons(X,Y),Z) | → | activate#(Y) | (35) |
sel#(0,cons(X,Y)) | → | activate#(X) | (26) |
dbls#(cons(X,Y)) | → | activate#(Y) | (34) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (33) |
from#(X) | → | activate#(X) | (24) |
activate#(n__dbl(X)) | → | dbl#(X) | (31) |
from#(X) | → | activate#(X) | (24) |
dbl#(s(X)) | → | activate#(X) | (23) |
activate#(n__dbls(X)) | → | dbls#(X) | (30) |
The dependency pairs are split into 1 component.
activate#(n__sel(X1,X2)) | → | sel#(X1,X2) | (27) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (32) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (39) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (36) |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 1 |
[activate(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 1 |
[indx(x1, x2)] | = | max(x1 + 2999, x2 + 3001, 0) |
[n__indx(x1, x2)] | = | max(x1 + 2999, x2 + 3001, 0) |
[n__from(x1)] | = | x1 + 20977 |
[dbl#(x1)] | = | 16305 |
[activate#(x1)] | = | x1 + 46572 |
[dbls#(x1)] | = | 16305 |
[n__dbls(x1)] | = | x1 + 1 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 1 |
[0] | = | 1 |
[sel#(x1, x2)] | = | max(x1 + 49571, x2 + 46572, 0) |
[indx#(x1, x2)] | = | max(0) |
[sel(x1, x2)] | = | max(x1 + 2999, x2 + 0, 0) |
[from(x1)] | = | x1 + 20977 |
[s#(x1)] | = | 0 |
[nil] | = | 3002 |
[n__sel(x1, x2)] | = | max(x1 + 2999, x2 + 0, 0) |
[from#(x1)] | = | 24670 |
[cons(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
activate(n__dbls(X)) | → | dbls(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
from(X) | → | n__from(X) | (15) |
indx(cons(X,Y),Z) | → | cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) | (8) |
dbl(0) | → | 0 | (1) |
dbls(nil) | → | nil | (3) |
activate(n__s(X)) | → | s(X) | (16) |
activate(n__from(X)) | → | from(X) | (21) |
activate(n__sel(X1,X2)) | → | sel(X1,X2) | (19) |
activate(n__dbl(X)) | → | dbl(X) | (17) |
activate(X) | → | X | (22) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
s(X) | → | n__s(X) | (10) |
indx(nil,X) | → | nil | (7) |
activate(n__indx(X1,X2)) | → | indx(X1,X2) | (20) |
indx(X1,X2) | → | n__indx(X1,X2) | (14) |
dbls(X) | → | n__dbls(X) | (12) |
dbl(X) | → | n__dbl(X) | (11) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(X1,X2) | → | n__sel(X1,X2) | (13) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (39) |
The dependency pairs are split into 1 component.
activate#(n__sel(X1,X2)) | → | sel#(X1,X2) | (27) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (32) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (36) |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 1 |
[activate(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 1 |
[indx(x1, x2)] | = | max(x1 + 1326, x2 + 1328, 0) |
[n__indx(x1, x2)] | = | max(x1 + 1326, x2 + 1328, 0) |
[n__from(x1)] | = | x1 + 53255 |
[dbl#(x1)] | = | 16305 |
[activate#(x1)] | = | x1 + 4688 |
[dbls#(x1)] | = | 16305 |
[n__dbls(x1)] | = | x1 + 1 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 1 |
[0] | = | 38607 |
[sel#(x1, x2)] | = | max(x1 + 4687, x2 + 4689, 0) |
[indx#(x1, x2)] | = | max(0) |
[sel(x1, x2)] | = | max(x1 + 1326, x2 + 1, 0) |
[from(x1)] | = | x1 + 53255 |
[s#(x1)] | = | 0 |
[nil] | = | 1329 |
[n__sel(x1, x2)] | = | max(x1 + 1326, x2 + 1, 0) |
[from#(x1)] | = | 24670 |
[cons(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
activate(n__dbls(X)) | → | dbls(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
from(X) | → | n__from(X) | (15) |
indx(cons(X,Y),Z) | → | cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) | (8) |
dbl(0) | → | 0 | (1) |
dbls(nil) | → | nil | (3) |
activate(n__s(X)) | → | s(X) | (16) |
activate(n__from(X)) | → | from(X) | (21) |
activate(n__sel(X1,X2)) | → | sel(X1,X2) | (19) |
activate(n__dbl(X)) | → | dbl(X) | (17) |
activate(X) | → | X | (22) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
s(X) | → | n__s(X) | (10) |
indx(nil,X) | → | nil | (7) |
activate(n__indx(X1,X2)) | → | indx(X1,X2) | (20) |
indx(X1,X2) | → | n__indx(X1,X2) | (14) |
dbls(X) | → | n__dbls(X) | (12) |
dbl(X) | → | n__dbl(X) | (11) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(X1,X2) | → | n__sel(X1,X2) | (13) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (32) |
The dependency pairs are split into 1 component.
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (36) |
π(activate#) | = | 1 |
π(dbls#) | = | 1 |
π(sel#) | = | 1 |
π(s#) | = | 1 |
prec(s) | = | 2 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(dbls) | = | 5 | status(dbls) | = | [1] | list-extension(dbls) | = | Lex | ||
prec(activate) | = | 1 | status(activate) | = | [1] | list-extension(activate) | = | Lex | ||
prec(dbl) | = | 3 | status(dbl) | = | [1] | list-extension(dbl) | = | Lex | ||
prec(indx) | = | 4 | status(indx) | = | [] | list-extension(indx) | = | Lex | ||
prec(n__indx) | = | 4 | status(n__indx) | = | [] | list-extension(n__indx) | = | Lex | ||
prec(n__from) | = | 4 | status(n__from) | = | [] | list-extension(n__from) | = | Lex | ||
prec(dbl#) | = | 0 | status(dbl#) | = | [] | list-extension(dbl#) | = | Lex | ||
prec(n__dbls) | = | 5 | status(n__dbls) | = | [1] | list-extension(n__dbls) | = | Lex | ||
prec(n__s) | = | 2 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(n__dbl) | = | 3 | status(n__dbl) | = | [1] | list-extension(n__dbl) | = | Lex | ||
prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(indx#) | = | 0 | status(indx#) | = | [1, 2] | list-extension(indx#) | = | Lex | ||
prec(sel) | = | 5 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(from) | = | 4 | status(from) | = | [] | list-extension(from) | = | Lex | ||
prec(nil) | = | 4 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(n__sel) | = | 5 | status(n__sel) | = | [] | list-extension(n__sel) | = | Lex | ||
prec(from#) | = | 0 | status(from#) | = | [] | list-extension(from#) | = | Lex | ||
prec(cons) | = | 4 | status(cons) | = | [] | list-extension(cons) | = | Lex |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 57802 |
[activate(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 25907 |
[indx(x1, x2)] | = | x1 + x2 + 31895 |
[n__indx(x1, x2)] | = | x1 + x2 + 31895 |
[n__from(x1)] | = | x1 + 58180 |
[dbl#(x1)] | = | 1 |
[n__dbls(x1)] | = | x1 + 57802 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 25907 |
[0] | = | 2998 |
[indx#(x1, x2)] | = | x1 + x2 + 1 |
[sel(x1, x2)] | = | x1 + x2 + 31893 |
[from(x1)] | = | x1 + 58180 |
[nil] | = | 36336 |
[n__sel(x1, x2)] | = | x1 + x2 + 31893 |
[from#(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 31894, x2 + 0, 0) |
activate(n__dbls(X)) | → | dbls(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
from(X) | → | n__from(X) | (15) |
indx(cons(X,Y),Z) | → | cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) | (8) |
dbl(0) | → | 0 | (1) |
dbls(nil) | → | nil | (3) |
activate(n__s(X)) | → | s(X) | (16) |
activate(n__from(X)) | → | from(X) | (21) |
activate(n__sel(X1,X2)) | → | sel(X1,X2) | (19) |
activate(n__dbl(X)) | → | dbl(X) | (17) |
activate(X) | → | X | (22) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
s(X) | → | n__s(X) | (10) |
indx(nil,X) | → | nil | (7) |
activate(n__indx(X1,X2)) | → | indx(X1,X2) | (20) |
indx(X1,X2) | → | n__indx(X1,X2) | (14) |
dbls(X) | → | n__dbls(X) | (12) |
dbl(X) | → | n__dbl(X) | (11) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(X1,X2) | → | n__sel(X1,X2) | (13) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (36) |
The dependency pairs are split into 0 components.