The rewrite relation of the following TRS is considered.
natsFrom(N) | → | cons(N,n__natsFrom(s(N))) | (1) |
fst(pair(XS,YS)) | → | XS | (2) |
snd(pair(XS,YS)) | → | YS | (3) |
splitAt(0,XS) | → | pair(nil,XS) | (4) |
splitAt(s(N),cons(X,XS)) | → | u(splitAt(N,activate(XS)),N,X,activate(XS)) | (5) |
u(pair(YS,ZS),N,X,XS) | → | pair(cons(activate(X),YS),ZS) | (6) |
head(cons(N,XS)) | → | N | (7) |
tail(cons(N,XS)) | → | activate(XS) | (8) |
sel(N,XS) | → | head(afterNth(N,XS)) | (9) |
take(N,XS) | → | fst(splitAt(N,XS)) | (10) |
afterNth(N,XS) | → | snd(splitAt(N,XS)) | (11) |
natsFrom(X) | → | n__natsFrom(X) | (12) |
activate(n__natsFrom(X)) | → | natsFrom(X) | (13) |
activate(X) | → | X | (14) |
prec(natsFrom) | = | 4 | stat(natsFrom) | = | mul | |
prec(cons) | = | 0 | stat(cons) | = | mul | |
prec(n__natsFrom) | = | 1 | stat(n__natsFrom) | = | mul | |
prec(s) | = | 2 | stat(s) | = | mul | |
prec(fst) | = | 5 | stat(fst) | = | mul | |
prec(pair) | = | 3 | stat(pair) | = | mul | |
prec(snd) | = | 6 | stat(snd) | = | mul | |
prec(splitAt) | = | 7 | stat(splitAt) | = | lex | |
prec(0) | = | 7 | stat(0) | = | mul | |
prec(nil) | = | 7 | stat(nil) | = | mul | |
prec(u) | = | 4 | stat(u) | = | mul | |
prec(activate) | = | 4 | stat(activate) | = | mul | |
prec(tail) | = | 4 | stat(tail) | = | mul | |
prec(sel) | = | 8 | stat(sel) | = | mul | |
prec(afterNth) | = | 8 | stat(afterNth) | = | mul | |
prec(take) | = | 9 | stat(take) | = | mul |
π(natsFrom) | = | [1] |
π(cons) | = | [1,2] |
π(n__natsFrom) | = | [1] |
π(s) | = | [1] |
π(fst) | = | [1] |
π(pair) | = | [1,2] |
π(snd) | = | [1] |
π(splitAt) | = | [1,2] |
π(0) | = | [] |
π(nil) | = | [] |
π(u) | = | [1,2,3,4] |
π(activate) | = | [1] |
π(head) | = | 1 |
π(tail) | = | [1] |
π(sel) | = | [1,2] |
π(afterNth) | = | [1,2] |
π(take) | = | [1,2] |
natsFrom(N) | → | cons(N,n__natsFrom(s(N))) | (1) |
fst(pair(XS,YS)) | → | XS | (2) |
snd(pair(XS,YS)) | → | YS | (3) |
splitAt(0,XS) | → | pair(nil,XS) | (4) |
splitAt(s(N),cons(X,XS)) | → | u(splitAt(N,activate(XS)),N,X,activate(XS)) | (5) |
u(pair(YS,ZS),N,X,XS) | → | pair(cons(activate(X),YS),ZS) | (6) |
head(cons(N,XS)) | → | N | (7) |
tail(cons(N,XS)) | → | activate(XS) | (8) |
take(N,XS) | → | fst(splitAt(N,XS)) | (10) |
afterNth(N,XS) | → | snd(splitAt(N,XS)) | (11) |
natsFrom(X) | → | n__natsFrom(X) | (12) |
activate(n__natsFrom(X)) | → | natsFrom(X) | (13) |
activate(X) | → | X | (14) |
prec(head) | = | 0 | weight(head) | = | 1 | ||||
prec(sel) | = | 1 | weight(sel) | = | 1 | ||||
prec(afterNth) | = | 2 | weight(afterNth) | = | 0 |
sel(N,XS) | → | head(afterNth(N,XS)) | (9) |
There are no rules in the TRS. Hence, it is terminating.