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) |
dbl1(0) | → | 01 | (10) |
dbl1(s(X)) | → | s1(s1(dbl1(activate(X)))) | (11) |
sel1(0,cons(X,Y)) | → | activate(X) | (12) |
sel1(s(X),cons(Y,Z)) | → | sel1(activate(X),activate(Z)) | (13) |
quote(0) | → | 01 | (14) |
quote(s(X)) | → | s1(quote(activate(X))) | (15) |
quote(dbl(X)) | → | dbl1(X) | (16) |
quote(sel(X,Y)) | → | sel1(X,Y) | (17) |
s(X) | → | n__s(X) | (18) |
dbl(X) | → | n__dbl(X) | (19) |
dbls(X) | → | n__dbls(X) | (20) |
sel(X1,X2) | → | n__sel(X1,X2) | (21) |
indx(X1,X2) | → | n__indx(X1,X2) | (22) |
from(X) | → | n__from(X) | (23) |
activate(n__s(X)) | → | s(X) | (24) |
activate(n__dbl(X)) | → | dbl(activate(X)) | (25) |
activate(n__dbls(X)) | → | dbls(activate(X)) | (26) |
activate(n__sel(X1,X2)) | → | sel(activate(X1),activate(X2)) | (27) |
activate(n__indx(X1,X2)) | → | indx(activate(X1),X2) | (28) |
activate(n__from(X)) | → | from(X) | (29) |
activate(X) | → | X | (30) |
dbl#(s(X)) | → | activate#(X) | (31) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (32) |
dbls#(cons(X,Y)) | → | activate#(Y) | (33) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (34) |
dbl1#(s(X)) | → | activate#(X) | (35) |
sel1#(s(X),cons(Y,Z)) | → | activate#(Z) | (36) |
from#(X) | → | activate#(X) | (37) |
quote#(sel(X,Y)) | → | sel1#(X,Y) | (38) |
activate#(n__sel(X1,X2)) | → | activate#(X2) | (39) |
dbl1#(s(X)) | → | dbl1#(activate(X)) | (40) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (32) |
activate#(n__s(X)) | → | s#(X) | (41) |
indx#(cons(X,Y),Z) | → | activate#(Y) | (42) |
activate#(n__dbls(X)) | → | dbls#(activate(X)) | (43) |
activate#(n__indx(X1,X2)) | → | activate#(X1) | (44) |
sel1#(s(X),cons(Y,Z)) | → | sel1#(activate(X),activate(Z)) | (45) |
from#(X) | → | activate#(X) | (37) |
quote#(s(X)) | → | activate#(X) | (46) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (47) |
indx#(cons(X,Y),Z) | → | activate#(X) | (48) |
activate#(n__sel(X1,X2)) | → | activate#(X1) | (49) |
dbls#(cons(X,Y)) | → | activate#(X) | (50) |
quote#(dbl(X)) | → | dbl1#(X) | (51) |
activate#(n__dbl(X)) | → | activate#(X) | (52) |
quote#(s(X)) | → | quote#(activate(X)) | (53) |
activate#(n__indx(X1,X2)) | → | indx#(activate(X1),X2) | (54) |
activate#(n__dbls(X)) | → | activate#(X) | (55) |
activate#(n__sel(X1,X2)) | → | sel#(activate(X1),activate(X2)) | (56) |
activate#(n__dbl(X)) | → | dbl#(activate(X)) | (57) |
activate#(n__from(X)) | → | from#(X) | (58) |
dbl#(s(X)) | → | s#(n__s(n__dbl(activate(X)))) | (59) |
sel1#(s(X),cons(Y,Z)) | → | activate#(X) | (60) |
sel1#(0,cons(X,Y)) | → | activate#(X) | (61) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (62) |
sel#(0,cons(X,Y)) | → | activate#(X) | (63) |
The dependency pairs are split into 4 components.
quote#(s(X)) | → | quote#(activate(X)) | (53) |
π(dbl1#) | = | 1 |
π(activate) | = | 1 |
π(dbls#) | = | 1 |
π(sel1) | = | 2 |
prec(01) | = | 0 | status(01) | = | [] | list-extension(01) | = | Lex | ||
prec(s) | = | 2 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(dbls) | = | 1 | status(dbls) | = | [1] | list-extension(dbls) | = | Lex | ||
prec(dbl) | = | 3 | status(dbl) | = | [1] | list-extension(dbl) | = | Lex | ||
prec(indx) | = | 1 | status(indx) | = | [2] | list-extension(indx) | = | Lex | ||
prec(n__indx) | = | 1 | status(n__indx) | = | [2] | list-extension(n__indx) | = | Lex | ||
prec(n__from) | = | 0 | status(n__from) | = | [] | list-extension(n__from) | = | Lex | ||
prec(dbl#) | = | 0 | status(dbl#) | = | [] | list-extension(dbl#) | = | Lex | ||
prec(activate#) | = | 0 | status(activate#) | = | [] | list-extension(activate#) | = | Lex | ||
prec(n__dbls) | = | 1 | 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(sel#) | = | 0 | status(sel#) | = | [] | list-extension(sel#) | = | Lex | ||
prec(indx#) | = | 0 | status(indx#) | = | [2, 1] | list-extension(indx#) | = | Lex | ||
prec(sel) | = | 0 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(from) | = | 0 | status(from) | = | [] | list-extension(from) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(nil) | = | 1 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(dbl1) | = | 0 | status(dbl1) | = | [] | list-extension(dbl1) | = | Lex | ||
prec(sel1#) | = | 0 | status(sel1#) | = | [] | list-extension(sel1#) | = | Lex | ||
prec(n__sel) | = | 0 | status(n__sel) | = | [] | list-extension(n__sel) | = | Lex | ||
prec(from#) | = | 0 | status(from#) | = | [] | list-extension(from#) | = | Lex | ||
prec(quote) | = | 0 | status(quote) | = | [] | list-extension(quote) | = | Lex | ||
prec(cons) | = | 0 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(quote#) | = | 0 | status(quote#) | = | [1] | list-extension(quote#) | = | Lex | ||
prec(s1) | = | 0 | status(s1) | = | [] | list-extension(s1) | = | Lex |
[01] | = | 0 |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 0 |
[indx(x1, x2)] | = | x2 + 4 |
[n__indx(x1, x2)] | = | x2 + 4 |
[n__from(x1)] | = | x1 + 284 |
[dbl#(x1)] | = | 1 |
[activate#(x1)] | = | 1 |
[n__dbls(x1)] | = | x1 + 0 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 0 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 1 |
[indx#(x1, x2)] | = | x1 + x2 + 1 |
[sel(x1, x2)] | = | x2 + 1 |
[from(x1)] | = | x1 + 284 |
[s#(x1)] | = | 1 |
[nil] | = | 4 |
[dbl1(x1)] | = | 1 |
[sel1#(x1, x2)] | = | x1 + 1 |
[n__sel(x1, x2)] | = | x2 + 1 |
[from#(x1)] | = | 1 |
[quote(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 2, x2 + 0, 0) |
[quote#(x1)] | = | x1 + 1 |
[s1(x1)] | = | 1 |
s(X) | → | n__s(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
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) |
sel(X1,X2) | → | n__sel(X1,X2) | (21) |
activate(n__dbls(X)) | → | dbls(activate(X)) | (26) |
dbl(X) | → | n__dbl(X) | (19) |
activate(n__sel(X1,X2)) | → | sel(activate(X1),activate(X2)) | (27) |
indx(X1,X2) | → | n__indx(X1,X2) | (22) |
activate(n__indx(X1,X2)) | → | indx(activate(X1),X2) | (28) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
indx(nil,X) | → | nil | (7) |
dbls(X) | → | n__dbls(X) | (20) |
activate(n__dbl(X)) | → | dbl(activate(X)) | (25) |
activate(X) | → | X | (30) |
from(X) | → | n__from(X) | (23) |
activate(n__s(X)) | → | s(X) | (24) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
activate(n__from(X)) | → | from(X) | (29) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
quote#(s(X)) | → | quote#(activate(X)) | (53) |
The dependency pairs are split into 0 components.
dbl1#(s(X)) | → | dbl1#(activate(X)) | (40) |
π(dbl1#) | = | 1 |
π(activate) | = | 1 |
π(dbls#) | = | 1 |
π(sel1) | = | 2 |
prec(01) | = | 0 | status(01) | = | [] | list-extension(01) | = | Lex | ||
prec(s) | = | 3 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(dbls) | = | 2 | status(dbls) | = | [1] | list-extension(dbls) | = | Lex | ||
prec(dbl) | = | 4 | status(dbl) | = | [1] | list-extension(dbl) | = | Lex | ||
prec(indx) | = | 3 | status(indx) | = | [] | list-extension(indx) | = | Lex | ||
prec(n__indx) | = | 3 | status(n__indx) | = | [] | list-extension(n__indx) | = | Lex | ||
prec(n__from) | = | 1 | status(n__from) | = | [] | list-extension(n__from) | = | Lex | ||
prec(dbl#) | = | 0 | status(dbl#) | = | [] | list-extension(dbl#) | = | Lex | ||
prec(activate#) | = | 0 | status(activate#) | = | [] | list-extension(activate#) | = | Lex | ||
prec(n__dbls) | = | 2 | status(n__dbls) | = | [1] | list-extension(n__dbls) | = | Lex | ||
prec(n__s) | = | 3 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(n__dbl) | = | 4 | status(n__dbl) | = | [1] | list-extension(n__dbl) | = | Lex | ||
prec(0) | = | 1 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(sel#) | = | 0 | status(sel#) | = | [] | list-extension(sel#) | = | Lex | ||
prec(indx#) | = | 0 | status(indx#) | = | [2, 1] | list-extension(indx#) | = | Lex | ||
prec(sel) | = | 0 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(from) | = | 1 | status(from) | = | [] | list-extension(from) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(nil) | = | 2 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(dbl1) | = | 0 | status(dbl1) | = | [] | list-extension(dbl1) | = | Lex | ||
prec(sel1#) | = | 0 | status(sel1#) | = | [] | list-extension(sel1#) | = | Lex | ||
prec(n__sel) | = | 0 | status(n__sel) | = | [] | list-extension(n__sel) | = | Lex | ||
prec(from#) | = | 0 | status(from#) | = | [] | list-extension(from#) | = | Lex | ||
prec(quote) | = | 0 | status(quote) | = | [] | list-extension(quote) | = | Lex | ||
prec(cons) | = | 0 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(quote#) | = | 0 | status(quote#) | = | [1] | list-extension(quote#) | = | Lex | ||
prec(s1) | = | 0 | status(s1) | = | [] | list-extension(s1) | = | Lex |
[01] | = | 0 |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 0 |
[indx(x1, x2)] | = | x2 + 4 |
[n__indx(x1, x2)] | = | x2 + 4 |
[n__from(x1)] | = | x1 + 3 |
[dbl#(x1)] | = | 1 |
[activate#(x1)] | = | 1 |
[n__dbls(x1)] | = | x1 + 0 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 0 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 1 |
[indx#(x1, x2)] | = | x1 + x2 + 1 |
[sel(x1, x2)] | = | x2 + 1 |
[from(x1)] | = | x1 + 3 |
[s#(x1)] | = | 1 |
[nil] | = | 3 |
[dbl1(x1)] | = | 1 |
[sel1#(x1, x2)] | = | x1 + 1 |
[n__sel(x1, x2)] | = | x2 + 1 |
[from#(x1)] | = | 1 |
[quote(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 2, x2 + 0, 0) |
[quote#(x1)] | = | x1 + 1 |
[s1(x1)] | = | 1 |
s(X) | → | n__s(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
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) |
sel(X1,X2) | → | n__sel(X1,X2) | (21) |
activate(n__dbls(X)) | → | dbls(activate(X)) | (26) |
dbl(X) | → | n__dbl(X) | (19) |
activate(n__sel(X1,X2)) | → | sel(activate(X1),activate(X2)) | (27) |
indx(X1,X2) | → | n__indx(X1,X2) | (22) |
activate(n__indx(X1,X2)) | → | indx(activate(X1),X2) | (28) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
indx(nil,X) | → | nil | (7) |
dbls(X) | → | n__dbls(X) | (20) |
activate(n__dbl(X)) | → | dbl(activate(X)) | (25) |
activate(X) | → | X | (30) |
from(X) | → | n__from(X) | (23) |
activate(n__s(X)) | → | s(X) | (24) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
activate(n__from(X)) | → | from(X) | (29) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
dbl1#(s(X)) | → | dbl1#(activate(X)) | (40) |
The dependency pairs are split into 0 components.
sel1#(s(X),cons(Y,Z)) | → | sel1#(activate(X),activate(Z)) | (45) |
π(activate) | = | 1 |
π(dbls#) | = | 1 |
π(sel1#) | = | 1 |
π(sel1) | = | 2 |
prec(dbl1#) | = | 0 | status(dbl1#) | = | [] | list-extension(dbl1#) | = | Lex | ||
prec(01) | = | 0 | status(01) | = | [] | list-extension(01) | = | Lex | ||
prec(s) | = | 3 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(dbls) | = | 2 | status(dbls) | = | [] | list-extension(dbls) | = | Lex | ||
prec(dbl) | = | 4 | status(dbl) | = | [1] | list-extension(dbl) | = | Lex | ||
prec(indx) | = | 2 | status(indx) | = | [] | list-extension(indx) | = | Lex | ||
prec(n__indx) | = | 2 | status(n__indx) | = | [] | list-extension(n__indx) | = | Lex | ||
prec(n__from) | = | 1 | status(n__from) | = | [] | list-extension(n__from) | = | Lex | ||
prec(dbl#) | = | 0 | status(dbl#) | = | [] | list-extension(dbl#) | = | Lex | ||
prec(activate#) | = | 0 | status(activate#) | = | [] | list-extension(activate#) | = | Lex | ||
prec(n__dbls) | = | 2 | status(n__dbls) | = | [] | list-extension(n__dbls) | = | Lex | ||
prec(n__s) | = | 3 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(n__dbl) | = | 4 | status(n__dbl) | = | [1] | list-extension(n__dbl) | = | Lex | ||
prec(0) | = | 1 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(sel#) | = | 0 | status(sel#) | = | [] | list-extension(sel#) | = | Lex | ||
prec(indx#) | = | 0 | status(indx#) | = | [2, 1] | list-extension(indx#) | = | Lex | ||
prec(sel) | = | 0 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(from) | = | 1 | status(from) | = | [] | list-extension(from) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(nil) | = | 2 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(dbl1) | = | 0 | status(dbl1) | = | [] | list-extension(dbl1) | = | Lex | ||
prec(n__sel) | = | 0 | status(n__sel) | = | [] | list-extension(n__sel) | = | Lex | ||
prec(from#) | = | 0 | status(from#) | = | [] | list-extension(from#) | = | Lex | ||
prec(quote) | = | 0 | status(quote) | = | [] | list-extension(quote) | = | Lex | ||
prec(cons) | = | 0 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(quote#) | = | 0 | status(quote#) | = | [] | list-extension(quote#) | = | Lex | ||
prec(s1) | = | 0 | status(s1) | = | [] | list-extension(s1) | = | Lex |
[dbl1#(x1)] | = | 0 |
[01] | = | 0 |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 0 |
[indx(x1, x2)] | = | x2 + 31603 |
[n__indx(x1, x2)] | = | x2 + 31603 |
[n__from(x1)] | = | x1 + 4 |
[dbl#(x1)] | = | 1 |
[activate#(x1)] | = | 1 |
[n__dbls(x1)] | = | x1 + 0 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 0 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 1 |
[indx#(x1, x2)] | = | x1 + x2 + 1 |
[sel(x1, x2)] | = | x2 + 1 |
[from(x1)] | = | x1 + 4 |
[s#(x1)] | = | 1 |
[nil] | = | 20585 |
[dbl1(x1)] | = | 1 |
[n__sel(x1, x2)] | = | x2 + 1 |
[from#(x1)] | = | 1 |
[quote(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 3, x2 + 0, 0) |
[quote#(x1)] | = | 1 |
[s1(x1)] | = | 1 |
s(X) | → | n__s(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
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) |
sel(X1,X2) | → | n__sel(X1,X2) | (21) |
activate(n__dbls(X)) | → | dbls(activate(X)) | (26) |
dbl(X) | → | n__dbl(X) | (19) |
activate(n__sel(X1,X2)) | → | sel(activate(X1),activate(X2)) | (27) |
indx(X1,X2) | → | n__indx(X1,X2) | (22) |
activate(n__indx(X1,X2)) | → | indx(activate(X1),X2) | (28) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
indx(nil,X) | → | nil | (7) |
dbls(X) | → | n__dbls(X) | (20) |
activate(n__dbl(X)) | → | dbl(activate(X)) | (25) |
activate(X) | → | X | (30) |
from(X) | → | n__from(X) | (23) |
activate(n__s(X)) | → | s(X) | (24) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
activate(n__from(X)) | → | from(X) | (29) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
sel1#(s(X),cons(Y,Z)) | → | sel1#(activate(X),activate(Z)) | (45) |
The dependency pairs are split into 0 components.
sel#(0,cons(X,Y)) | → | activate#(X) | (63) |
activate#(n__dbls(X)) | → | dbls#(activate(X)) | (43) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (62) |
indx#(cons(X,Y),Z) | → | activate#(Y) | (42) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (32) |
activate#(n__sel(X1,X2)) | → | activate#(X2) | (39) |
activate#(n__from(X)) | → | from#(X) | (58) |
activate#(n__dbl(X)) | → | dbl#(activate(X)) | (57) |
activate#(n__sel(X1,X2)) | → | sel#(activate(X1),activate(X2)) | (56) |
activate#(n__dbls(X)) | → | activate#(X) | (55) |
from#(X) | → | activate#(X) | (37) |
activate#(n__indx(X1,X2)) | → | indx#(activate(X1),X2) | (54) |
activate#(n__dbl(X)) | → | activate#(X) | (52) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (34) |
dbls#(cons(X,Y)) | → | activate#(X) | (50) |
activate#(n__sel(X1,X2)) | → | activate#(X1) | (49) |
indx#(cons(X,Y),Z) | → | activate#(X) | (48) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (47) |
from#(X) | → | activate#(X) | (37) |
dbls#(cons(X,Y)) | → | activate#(Y) | (33) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (32) |
dbl#(s(X)) | → | activate#(X) | (31) |
activate#(n__indx(X1,X2)) | → | activate#(X1) | (44) |
[dbl1#(x1)] | = | 0 |
[01] | = | 0 |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 2 |
[activate(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 2 |
[indx(x1, x2)] | = | max(x1 + 67291, x2 + 67293, 0) |
[n__indx(x1, x2)] | = | max(x1 + 67291, x2 + 67293, 0) |
[n__from(x1)] | = | x1 + 31893 |
[dbl#(x1)] | = | x1 + 10424 |
[activate#(x1)] | = | x1 + 10423 |
[dbls#(x1)] | = | x1 + 10424 |
[n__dbls(x1)] | = | x1 + 2 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 2 |
[0] | = | 1 |
[sel#(x1, x2)] | = | max(x1 + 10425, x2 + 10424, 0) |
[indx#(x1, x2)] | = | max(x1 + 18458, x2 + 77715, 0) |
[sel(x1, x2)] | = | max(x1 + 45634, x2 + 20979, 0) |
[from(x1)] | = | x1 + 31893 |
[s#(x1)] | = | 0 |
[nil] | = | 67294 |
[dbl1(x1)] | = | 0 |
[sel1#(x1, x2)] | = | max(0) |
[n__sel(x1, x2)] | = | max(x1 + 45634, x2 + 20979, 0) |
[from#(x1)] | = | x1 + 10424 |
[quote(x1)] | = | 0 |
[cons(x1, x2)] | = | max(x1 + 21657, x2 + 0, 0) |
[quote#(x1)] | = | 0 |
[sel1(x1, x2)] | = | max(0) |
[s1(x1)] | = | 0 |
s(X) | → | n__s(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
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) |
sel(X1,X2) | → | n__sel(X1,X2) | (21) |
activate(n__dbls(X)) | → | dbls(activate(X)) | (26) |
dbl(X) | → | n__dbl(X) | (19) |
activate(n__sel(X1,X2)) | → | sel(activate(X1),activate(X2)) | (27) |
indx(X1,X2) | → | n__indx(X1,X2) | (22) |
activate(n__indx(X1,X2)) | → | indx(activate(X1),X2) | (28) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
indx(nil,X) | → | nil | (7) |
dbls(X) | → | n__dbls(X) | (20) |
activate(n__dbl(X)) | → | dbl(activate(X)) | (25) |
activate(X) | → | X | (30) |
from(X) | → | n__from(X) | (23) |
activate(n__s(X)) | → | s(X) | (24) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
activate(n__from(X)) | → | from(X) | (29) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
sel#(0,cons(X,Y)) | → | activate#(X) | (63) |
activate#(n__dbls(X)) | → | dbls#(activate(X)) | (43) |
indx#(cons(X,Y),Z) | → | activate#(Y) | (42) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (32) |
activate#(n__sel(X1,X2)) | → | activate#(X2) | (39) |
activate#(n__from(X)) | → | from#(X) | (58) |
activate#(n__dbl(X)) | → | dbl#(activate(X)) | (57) |
activate#(n__sel(X1,X2)) | → | sel#(activate(X1),activate(X2)) | (56) |
activate#(n__dbls(X)) | → | activate#(X) | (55) |
from#(X) | → | activate#(X) | (37) |
activate#(n__indx(X1,X2)) | → | indx#(activate(X1),X2) | (54) |
activate#(n__dbl(X)) | → | activate#(X) | (52) |
sel#(s(X),cons(Y,Z)) | → | activate#(Z) | (34) |
dbls#(cons(X,Y)) | → | activate#(X) | (50) |
activate#(n__sel(X1,X2)) | → | activate#(X1) | (49) |
indx#(cons(X,Y),Z) | → | activate#(X) | (48) |
sel#(s(X),cons(Y,Z)) | → | activate#(X) | (47) |
from#(X) | → | activate#(X) | (37) |
dbls#(cons(X,Y)) | → | activate#(Y) | (33) |
indx#(cons(X,Y),Z) | → | activate#(Z) | (32) |
dbl#(s(X)) | → | activate#(X) | (31) |
activate#(n__indx(X1,X2)) | → | activate#(X1) | (44) |
The dependency pairs are split into 1 component.
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (62) |
π(activate) | = | 1 |
π(dbls#) | = | 1 |
π(sel#) | = | 1 |
π(sel1#) | = | 1 |
π(sel1) | = | 2 |
prec(dbl1#) | = | 0 | status(dbl1#) | = | [] | list-extension(dbl1#) | = | Lex | ||
prec(01) | = | 0 | status(01) | = | [] | list-extension(01) | = | Lex | ||
prec(s) | = | 3 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(dbls) | = | 2 | status(dbls) | = | [] | list-extension(dbls) | = | Lex | ||
prec(dbl) | = | 4 | status(dbl) | = | [1] | list-extension(dbl) | = | Lex | ||
prec(indx) | = | 2 | status(indx) | = | [] | list-extension(indx) | = | Lex | ||
prec(n__indx) | = | 2 | status(n__indx) | = | [] | list-extension(n__indx) | = | Lex | ||
prec(n__from) | = | 1 | status(n__from) | = | [] | list-extension(n__from) | = | Lex | ||
prec(dbl#) | = | 0 | status(dbl#) | = | [] | list-extension(dbl#) | = | Lex | ||
prec(activate#) | = | 0 | status(activate#) | = | [] | list-extension(activate#) | = | Lex | ||
prec(n__dbls) | = | 2 | status(n__dbls) | = | [] | list-extension(n__dbls) | = | Lex | ||
prec(n__s) | = | 3 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(n__dbl) | = | 4 | status(n__dbl) | = | [1] | list-extension(n__dbl) | = | Lex | ||
prec(0) | = | 1 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(indx#) | = | 0 | status(indx#) | = | [2, 1] | list-extension(indx#) | = | Lex | ||
prec(sel) | = | 0 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(from) | = | 1 | status(from) | = | [] | list-extension(from) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(nil) | = | 2 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(dbl1) | = | 0 | status(dbl1) | = | [] | list-extension(dbl1) | = | Lex | ||
prec(n__sel) | = | 0 | status(n__sel) | = | [] | list-extension(n__sel) | = | Lex | ||
prec(from#) | = | 0 | status(from#) | = | [] | list-extension(from#) | = | Lex | ||
prec(quote) | = | 0 | status(quote) | = | [] | list-extension(quote) | = | Lex | ||
prec(cons) | = | 0 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(quote#) | = | 0 | status(quote#) | = | [] | list-extension(quote#) | = | Lex | ||
prec(s1) | = | 0 | status(s1) | = | [] | list-extension(s1) | = | Lex |
[dbl1#(x1)] | = | 0 |
[01] | = | 0 |
[s(x1)] | = | x1 + 0 |
[dbls(x1)] | = | x1 + 0 |
[dbl(x1)] | = | x1 + 0 |
[indx(x1, x2)] | = | x2 + 31603 |
[n__indx(x1, x2)] | = | x2 + 31603 |
[n__from(x1)] | = | x1 + 491 |
[dbl#(x1)] | = | 1 |
[activate#(x1)] | = | 1 |
[n__dbls(x1)] | = | x1 + 0 |
[n__s(x1)] | = | x1 + 0 |
[n__dbl(x1)] | = | x1 + 0 |
[0] | = | 1 |
[indx#(x1, x2)] | = | x1 + x2 + 1 |
[sel(x1, x2)] | = | x2 + 1 |
[from(x1)] | = | x1 + 491 |
[s#(x1)] | = | 1 |
[nil] | = | 7579 |
[dbl1(x1)] | = | 1 |
[n__sel(x1, x2)] | = | x2 + 1 |
[from#(x1)] | = | 1 |
[quote(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 490, x2 + 0, 0) |
[quote#(x1)] | = | 1 |
[s1(x1)] | = | 1 |
s(X) | → | n__s(X) | (18) |
dbls(cons(X,Y)) | → | cons(n__dbl(activate(X)),n__dbls(activate(Y))) | (4) |
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) |
sel(X1,X2) | → | n__sel(X1,X2) | (21) |
activate(n__dbls(X)) | → | dbls(activate(X)) | (26) |
dbl(X) | → | n__dbl(X) | (19) |
activate(n__sel(X1,X2)) | → | sel(activate(X1),activate(X2)) | (27) |
indx(X1,X2) | → | n__indx(X1,X2) | (22) |
activate(n__indx(X1,X2)) | → | indx(activate(X1),X2) | (28) |
sel(0,cons(X,Y)) | → | activate(X) | (5) |
indx(nil,X) | → | nil | (7) |
dbls(X) | → | n__dbls(X) | (20) |
activate(n__dbl(X)) | → | dbl(activate(X)) | (25) |
activate(X) | → | X | (30) |
from(X) | → | n__from(X) | (23) |
activate(n__s(X)) | → | s(X) | (24) |
from(X) | → | cons(activate(X),n__from(n__s(activate(X)))) | (9) |
sel(s(X),cons(Y,Z)) | → | sel(activate(X),activate(Z)) | (6) |
activate(n__from(X)) | → | from(X) | (29) |
dbl(s(X)) | → | s(n__s(n__dbl(activate(X)))) | (2) |
sel#(s(X),cons(Y,Z)) | → | sel#(activate(X),activate(Z)) | (62) |
The dependency pairs are split into 0 components.