The rewrite relation of the following TRS is considered.
from(X) | → | cons(X,n__from(s(X))) | (1) |
head(cons(X,XS)) | → | X | (2) |
2nd(cons(X,XS)) | → | head(activate(XS)) | (3) |
take(0,XS) | → | nil | (4) |
take(s(N),cons(X,XS)) | → | cons(X,n__take(N,activate(XS))) | (5) |
sel(0,cons(X,XS)) | → | X | (6) |
sel(s(N),cons(X,XS)) | → | sel(N,activate(XS)) | (7) |
from(X) | → | n__from(X) | (8) |
take(X1,X2) | → | n__take(X1,X2) | (9) |
activate(n__from(X)) | → | from(X) | (10) |
activate(n__take(X1,X2)) | → | take(X1,X2) | (11) |
activate(X) | → | X | (12) |
prec(sel) | = | 12 | status(sel) | = | [1, 2] | list-extension(sel) | = | Lex | ||
prec(n__take) | = | 0 | status(n__take) | = | [2, 1] | list-extension(n__take) | = | Lex | ||
prec(nil) | = | 0 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(take) | = | 1 | status(take) | = | [2, 1] | list-extension(take) | = | Lex | ||
prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(activate) | = | 8 | status(activate) | = | [1] | list-extension(activate) | = | Lex | ||
prec(2nd) | = | 0 | status(2nd) | = | [1] | list-extension(2nd) | = | Lex | ||
prec(head) | = | 0 | status(head) | = | [1] | list-extension(head) | = | Lex | ||
prec(cons) | = | 0 | status(cons) | = | [1, 2] | list-extension(cons) | = | Lex | ||
prec(n__from) | = | 0 | status(n__from) | = | [1] | list-extension(n__from) | = | Lex | ||
prec(s) | = | 0 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(from) | = | 1 | status(from) | = | [1] | list-extension(from) | = | Lex |
[sel(x1, x2)] | = | max(0, 2 + 1 · x1, 0 + 1 · x2) |
[n__take(x1, x2)] | = | max(0, 4 + 1 · x1, 2 + 1 · x2) |
[nil] | = | max(0) |
[take(x1, x2)] | = | max(0, 4 + 1 · x1, 2 + 1 · x2) |
[0] | = | max(4) |
[activate(x1)] | = | max(0, 0 + 1 · x1) |
[2nd(x1)] | = | 4 + 1 · x1 |
[head(x1)] | = | max(1, 0 + 1 · x1) |
[cons(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
[n__from(x1)] | = | max(0, 0 + 1 · x1) |
[s(x1)] | = | 0 + 1 · x1 |
[from(x1)] | = | max(0, 0 + 1 · x1) |
from(X) | → | cons(X,n__from(s(X))) | (1) |
head(cons(X,XS)) | → | X | (2) |
2nd(cons(X,XS)) | → | head(activate(XS)) | (3) |
take(0,XS) | → | nil | (4) |
take(s(N),cons(X,XS)) | → | cons(X,n__take(N,activate(XS))) | (5) |
sel(0,cons(X,XS)) | → | X | (6) |
sel(s(N),cons(X,XS)) | → | sel(N,activate(XS)) | (7) |
from(X) | → | n__from(X) | (8) |
take(X1,X2) | → | n__take(X1,X2) | (9) |
activate(n__from(X)) | → | from(X) | (10) |
activate(n__take(X1,X2)) | → | take(X1,X2) | (11) |
activate(X) | → | X | (12) |
There are no rules in the TRS. Hence, it is terminating.