The rewrite relation of the following TRS is considered.
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (1) |
a__fst(pair(XS,YS)) | → | mark(XS) | (2) |
a__snd(pair(XS,YS)) | → | mark(YS) | (3) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (4) |
a__splitAt(s(N),cons(X,XS)) | → | a__u(a__splitAt(mark(N),mark(XS)),N,X,XS) | (5) |
a__u(pair(YS,ZS),N,X,XS) | → | pair(cons(mark(X),YS),mark(ZS)) | (6) |
a__head(cons(N,XS)) | → | mark(N) | (7) |
a__tail(cons(N,XS)) | → | mark(XS) | (8) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (9) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (10) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (11) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (12) |
mark(fst(X)) | → | a__fst(mark(X)) | (13) |
mark(snd(X)) | → | a__snd(mark(X)) | (14) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (15) |
mark(u(X1,X2,X3,X4)) | → | a__u(mark(X1),X2,X3,X4) | (16) |
mark(head(X)) | → | a__head(mark(X)) | (17) |
mark(tail(X)) | → | a__tail(mark(X)) | (18) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (19) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (20) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (21) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (22) |
mark(s(X)) | → | s(mark(X)) | (23) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (24) |
mark(0) | → | 0 | (25) |
mark(nil) | → | nil | (26) |
a__natsFrom(X) | → | natsFrom(X) | (27) |
a__fst(X) | → | fst(X) | (28) |
a__snd(X) | → | snd(X) | (29) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (30) |
a__u(X1,X2,X3,X4) | → | u(X1,X2,X3,X4) | (31) |
a__head(X) | → | head(X) | (32) |
a__tail(X) | → | tail(X) | (33) |
a__sel(X1,X2) | → | sel(X1,X2) | (34) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
a__take(X1,X2) | → | take(X1,X2) | (36) |
a__u#(pair(YS,ZS),N,X,XS) | → | mark#(X) | (37) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (38) |
a__splitAt#(s(N),cons(X,XS)) | → | a__u#(a__splitAt(mark(N),mark(XS)),N,X,XS) | (39) |
mark#(head(X)) | → | mark#(X) | (40) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (41) |
mark#(u(X1,X2,X3,X4)) | → | a__u#(mark(X1),X2,X3,X4) | (42) |
mark#(take(X1,X2)) | → | mark#(X2) | (43) |
mark#(sel(X1,X2)) | → | mark#(X1) | (44) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (45) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (46) |
mark#(sel(X1,X2)) | → | mark#(X2) | (47) |
a__sel#(N,XS) | → | a__head#(a__afterNth(mark(N),mark(XS))) | (48) |
mark#(take(X1,X2)) | → | mark#(X1) | (49) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (50) |
a__afterNth#(N,XS) | → | mark#(XS) | (51) |
a__sel#(N,XS) | → | mark#(XS) | (52) |
a__afterNth#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (53) |
a__head#(cons(N,XS)) | → | mark#(N) | (54) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (55) |
a__natsFrom#(N) | → | mark#(N) | (56) |
a__afterNth#(N,XS) | → | mark#(N) | (57) |
a__splitAt#(s(N),cons(X,XS)) | → | mark#(N) | (58) |
mark#(pair(X1,X2)) | → | mark#(X1) | (59) |
a__splitAt#(s(N),cons(X,XS)) | → | a__splitAt#(mark(N),mark(XS)) | (60) |
mark#(tail(X)) | → | mark#(X) | (61) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (62) |
a__take#(N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (63) |
mark#(snd(X)) | → | mark#(X) | (64) |
a__sel#(N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (65) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (66) |
a__afterNth#(N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (67) |
mark#(cons(X1,X2)) | → | mark#(X1) | (68) |
mark#(fst(X)) | → | mark#(X) | (69) |
a__snd#(pair(XS,YS)) | → | mark#(YS) | (70) |
a__take#(N,XS) | → | mark#(XS) | (71) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (72) |
mark#(head(X)) | → | a__head#(mark(X)) | (73) |
a__take#(N,XS) | → | mark#(N) | (74) |
mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | (75) |
a__splitAt#(s(N),cons(X,XS)) | → | mark#(XS) | (76) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (77) |
a__take#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (78) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (79) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (80) |
mark#(s(X)) | → | mark#(X) | (81) |
a__u#(pair(YS,ZS),N,X,XS) | → | mark#(ZS) | (82) |
a__fst#(pair(XS,YS)) | → | mark#(XS) | (83) |
a__sel#(N,XS) | → | mark#(N) | (84) |
mark#(pair(X1,X2)) | → | mark#(X2) | (85) |
mark#(fst(X)) | → | a__fst#(mark(X)) | (86) |
a__splitAt#(0,XS) | → | mark#(XS) | (87) |
mark#(natsFrom(X)) | → | mark#(X) | (88) |
The dependency pairs are split into 1 component.
mark#(natsFrom(X)) | → | mark#(X) | (88) |
a__splitAt#(0,XS) | → | mark#(XS) | (87) |
a__take#(N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (63) |
mark#(tail(X)) | → | mark#(X) | (61) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (62) |
mark#(fst(X)) | → | a__fst#(mark(X)) | (86) |
a__splitAt#(s(N),cons(X,XS)) | → | a__splitAt#(mark(N),mark(XS)) | (60) |
mark#(pair(X1,X2)) | → | mark#(X1) | (59) |
mark#(pair(X1,X2)) | → | mark#(X2) | (85) |
a__splitAt#(s(N),cons(X,XS)) | → | mark#(N) | (58) |
a__afterNth#(N,XS) | → | mark#(N) | (57) |
a__sel#(N,XS) | → | mark#(N) | (84) |
a__natsFrom#(N) | → | mark#(N) | (56) |
a__fst#(pair(XS,YS)) | → | mark#(XS) | (83) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (55) |
a__u#(pair(YS,ZS),N,X,XS) | → | mark#(ZS) | (82) |
a__head#(cons(N,XS)) | → | mark#(N) | (54) |
mark#(s(X)) | → | mark#(X) | (81) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (80) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (79) |
a__take#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (78) |
a__afterNth#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (53) |
a__sel#(N,XS) | → | mark#(XS) | (52) |
a__afterNth#(N,XS) | → | mark#(XS) | (51) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (50) |
a__splitAt#(s(N),cons(X,XS)) | → | mark#(XS) | (76) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (77) |
mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | (75) |
mark#(take(X1,X2)) | → | mark#(X1) | (49) |
a__sel#(N,XS) | → | a__head#(a__afterNth(mark(N),mark(XS))) | (48) |
a__take#(N,XS) | → | mark#(N) | (74) |
mark#(sel(X1,X2)) | → | mark#(X2) | (47) |
mark#(head(X)) | → | a__head#(mark(X)) | (73) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (46) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (72) |
a__take#(N,XS) | → | mark#(XS) | (71) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (45) |
a__snd#(pair(XS,YS)) | → | mark#(YS) | (70) |
mark#(fst(X)) | → | mark#(X) | (69) |
mark#(sel(X1,X2)) | → | mark#(X1) | (44) |
mark#(cons(X1,X2)) | → | mark#(X1) | (68) |
mark#(take(X1,X2)) | → | mark#(X2) | (43) |
mark#(u(X1,X2,X3,X4)) | → | a__u#(mark(X1),X2,X3,X4) | (42) |
a__afterNth#(N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (67) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (41) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (66) |
a__sel#(N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (65) |
mark#(head(X)) | → | mark#(X) | (40) |
a__splitAt#(s(N),cons(X,XS)) | → | a__u#(a__splitAt(mark(N),mark(XS)),N,X,XS) | (39) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (38) |
a__u#(pair(YS,ZS),N,X,XS) | → | mark#(X) | (37) |
mark#(snd(X)) | → | mark#(X) | (64) |
[s(x1)] | = | x1 + 0 |
[a__head#(x1)] | = | x1 + 74785 |
[a__natsFrom#(x1)] | = | x1 + 67156 |
[a__snd#(x1)] | = | x1 + 67154 |
[a__afterNth(x1, x2)] | = | max(x1 + 60531, x2 + 60532, 0) |
[u(x1,...,x4)] | = | max(x1 + 0, x2 + 60525, x3 + 60531, x4 + 60527, 0) |
[take(x1, x2)] | = | max(x1 + 60531, x2 + 60532, 0) |
[pair(x1, x2)] | = | max(x1 + 31118, x2 + 60525, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 29407 |
[a__snd(x1)] | = | x1 + 1 |
[splitAt(x1, x2)] | = | max(x1 + 60530, x2 + 60528, 0) |
[a__take#(x1, x2)] | = | max(x1 + 127681, x2 + 127683, 0) |
[a__natsFrom(x1)] | = | x1 + 29407 |
[a__fst(x1)] | = | x1 + 1 |
[tail(x1)] | = | x1 + 2 |
[mark#(x1)] | = | x1 + 67155 |
[0] | = | 21084 |
[a__u(x1,...,x4)] | = | max(x1 + 0, x2 + 60525, x3 + 60531, x4 + 60527, 0) |
[sel(x1, x2)] | = | max(x1 + 68163, x2 + 68164, 0) |
[afterNth(x1, x2)] | = | max(x1 + 60531, x2 + 60532, 0) |
[nil] | = | 12280 |
[a__splitAt(x1, x2)] | = | max(x1 + 60530, x2 + 60528, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 135316, x2 + 135317, 0) |
[mark(x1)] | = | x1 + 0 |
[a__sel(x1, x2)] | = | max(x1 + 68163, x2 + 68164, 0) |
[head(x1)] | = | x1 + 7632 |
[a__afterNth#(x1, x2)] | = | max(x1 + 127685, x2 + 127683, 0) |
[a__splitAt#(x1, x2)] | = | max(x1 + 127680, x2 + 127682, 0) |
[cons(x1, x2)] | = | max(x1 + 29407, x2 + 0, 0) |
[snd(x1)] | = | x1 + 1 |
[a__u#(x1,...,x4)] | = | max(x1 + 36038, x2 + 67156, x3 + 127683, x4 + 127681, 0) |
[a__take(x1, x2)] | = | max(x1 + 60531, x2 + 60532, 0) |
[a__fst#(x1)] | = | x1 + 67150 |
[a__tail(x1)] | = | x1 + 2 |
[a__tail#(x1)] | = | x1 + 67156 |
[a__head(x1)] | = | x1 + 7632 |
mark(tail(X)) | → | a__tail(mark(X)) | (18) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (4) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (15) |
a__tail(cons(N,XS)) | → | mark(XS) | (8) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (1) |
a__snd(pair(XS,YS)) | → | mark(YS) | (3) |
mark(u(X1,X2,X3,X4)) | → | a__u(mark(X1),X2,X3,X4) | (16) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (21) |
a__take(X1,X2) | → | take(X1,X2) | (36) |
mark(nil) | → | nil | (26) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (19) |
a__head(X) | → | head(X) | (32) |
mark(head(X)) | → | a__head(mark(X)) | (17) |
a__natsFrom(X) | → | natsFrom(X) | (27) |
a__sel(X1,X2) | → | sel(X1,X2) | (34) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (22) |
a__fst(X) | → | fst(X) | (28) |
a__splitAt(s(N),cons(X,XS)) | → | a__u(a__splitAt(mark(N),mark(XS)),N,X,XS) | (5) |
a__tail(X) | → | tail(X) | (33) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (10) |
a__head(cons(N,XS)) | → | mark(N) | (7) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (20) |
mark(0) | → | 0 | (25) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (30) |
mark(snd(X)) | → | a__snd(mark(X)) | (14) |
a__u(X1,X2,X3,X4) | → | u(X1,X2,X3,X4) | (31) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (12) |
mark(s(X)) | → | s(mark(X)) | (23) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (24) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (11) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (9) |
mark(fst(X)) | → | a__fst(mark(X)) | (13) |
a__u(pair(YS,ZS),N,X,XS) | → | pair(cons(mark(X),YS),mark(ZS)) | (6) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
a__snd(X) | → | snd(X) | (29) |
a__fst(pair(XS,YS)) | → | mark(XS) | (2) |
mark#(natsFrom(X)) | → | mark#(X) | (88) |
a__splitAt#(0,XS) | → | mark#(XS) | (87) |
a__take#(N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (63) |
mark#(tail(X)) | → | mark#(X) | (61) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (62) |
mark#(fst(X)) | → | a__fst#(mark(X)) | (86) |
mark#(pair(X1,X2)) | → | mark#(X1) | (59) |
mark#(pair(X1,X2)) | → | mark#(X2) | (85) |
a__splitAt#(s(N),cons(X,XS)) | → | mark#(N) | (58) |
a__afterNth#(N,XS) | → | mark#(N) | (57) |
a__sel#(N,XS) | → | mark#(N) | (84) |
a__natsFrom#(N) | → | mark#(N) | (56) |
a__fst#(pair(XS,YS)) | → | mark#(XS) | (83) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (55) |
a__u#(pair(YS,ZS),N,X,XS) | → | mark#(ZS) | (82) |
a__head#(cons(N,XS)) | → | mark#(N) | (54) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (80) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (79) |
a__take#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (78) |
a__afterNth#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (53) |
a__sel#(N,XS) | → | mark#(XS) | (52) |
a__afterNth#(N,XS) | → | mark#(XS) | (51) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (50) |
a__splitAt#(s(N),cons(X,XS)) | → | mark#(XS) | (76) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (77) |
mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | (75) |
mark#(take(X1,X2)) | → | mark#(X1) | (49) |
a__take#(N,XS) | → | mark#(N) | (74) |
mark#(sel(X1,X2)) | → | mark#(X2) | (47) |
mark#(head(X)) | → | a__head#(mark(X)) | (73) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (46) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (72) |
a__take#(N,XS) | → | mark#(XS) | (71) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (45) |
a__snd#(pair(XS,YS)) | → | mark#(YS) | (70) |
mark#(fst(X)) | → | mark#(X) | (69) |
mark#(sel(X1,X2)) | → | mark#(X1) | (44) |
mark#(cons(X1,X2)) | → | mark#(X1) | (68) |
mark#(take(X1,X2)) | → | mark#(X2) | (43) |
mark#(u(X1,X2,X3,X4)) | → | a__u#(mark(X1),X2,X3,X4) | (42) |
a__afterNth#(N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (67) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (41) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (66) |
a__sel#(N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (65) |
mark#(head(X)) | → | mark#(X) | (40) |
a__splitAt#(s(N),cons(X,XS)) | → | a__u#(a__splitAt(mark(N),mark(XS)),N,X,XS) | (39) |
a__u#(pair(YS,ZS),N,X,XS) | → | mark#(X) | (37) |
mark#(snd(X)) | → | mark#(X) | (64) |
The dependency pairs are split into 2 components.
a__splitAt#(s(N),cons(X,XS)) | → | a__splitAt#(mark(N),mark(XS)) | (60) |
π(a__natsFrom#) | = | 1 |
π(mark) | = | 1 |
prec(s) | = | 4 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__head#) | = | 0 | status(a__head#) | = | [] | list-extension(a__head#) | = | Lex | ||
prec(a__snd#) | = | 0 | status(a__snd#) | = | [] | list-extension(a__snd#) | = | Lex | ||
prec(a__afterNth) | = | 6 | status(a__afterNth) | = | [] | list-extension(a__afterNth) | = | Lex | ||
prec(u) | = | 3 | status(u) | = | [4] | list-extension(u) | = | Lex | ||
prec(take) | = | 6 | status(take) | = | [] | list-extension(take) | = | Lex | ||
prec(pair) | = | 2 | status(pair) | = | [2, 1] | list-extension(pair) | = | Lex | ||
prec(fst) | = | 2 | status(fst) | = | [1] | list-extension(fst) | = | Lex | ||
prec(natsFrom) | = | 3 | status(natsFrom) | = | [] | list-extension(natsFrom) | = | Lex | ||
prec(a__snd) | = | 2 | status(a__snd) | = | [1] | list-extension(a__snd) | = | Lex | ||
prec(splitAt) | = | 5 | status(splitAt) | = | [] | list-extension(splitAt) | = | Lex | ||
prec(a__take#) | = | 0 | status(a__take#) | = | [1] | list-extension(a__take#) | = | Lex | ||
prec(a__natsFrom) | = | 3 | status(a__natsFrom) | = | [] | list-extension(a__natsFrom) | = | Lex | ||
prec(a__fst) | = | 2 | status(a__fst) | = | [1] | list-extension(a__fst) | = | Lex | ||
prec(tail) | = | 2 | status(tail) | = | [] | list-extension(tail) | = | Lex | ||
prec(mark#) | = | 0 | status(mark#) | = | [] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__u) | = | 3 | status(a__u) | = | [4] | list-extension(a__u) | = | Lex | ||
prec(sel) | = | 7 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(afterNth) | = | 6 | status(afterNth) | = | [] | list-extension(afterNth) | = | Lex | ||
prec(nil) | = | 6 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(a__splitAt) | = | 5 | status(a__splitAt) | = | [] | list-extension(a__splitAt) | = | Lex | ||
prec(a__sel#) | = | 0 | status(a__sel#) | = | [1, 2] | list-extension(a__sel#) | = | Lex | ||
prec(a__sel) | = | 7 | status(a__sel) | = | [] | list-extension(a__sel) | = | Lex | ||
prec(head) | = | 7 | status(head) | = | [] | list-extension(head) | = | Lex | ||
prec(a__afterNth#) | = | 0 | status(a__afterNth#) | = | [1, 2] | list-extension(a__afterNth#) | = | Lex | ||
prec(a__splitAt#) | = | 0 | status(a__splitAt#) | = | [1] | list-extension(a__splitAt#) | = | Lex | ||
prec(cons) | = | 1 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(snd) | = | 2 | status(snd) | = | [1] | list-extension(snd) | = | Lex | ||
prec(a__u#) | = | 0 | status(a__u#) | = | [] | list-extension(a__u#) | = | Lex | ||
prec(a__take) | = | 6 | status(a__take) | = | [] | list-extension(a__take) | = | Lex | ||
prec(a__fst#) | = | 0 | status(a__fst#) | = | [] | list-extension(a__fst#) | = | Lex | ||
prec(a__tail) | = | 2 | status(a__tail) | = | [] | list-extension(a__tail) | = | Lex | ||
prec(a__tail#) | = | 0 | status(a__tail#) | = | [] | list-extension(a__tail#) | = | Lex | ||
prec(a__head) | = | 7 | status(a__head) | = | [] | list-extension(a__head) | = | Lex |
[s(x1)] | = | x1 + 0 |
[a__head#(x1)] | = | 1 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | x2 + 34525 |
[u(x1,...,x4)] | = | max(x1 + 0, x3 + 8, x4 + 1, 0) |
[take(x1, x2)] | = | x2 + 7 |
[pair(x1, x2)] | = | max(x1 + 3, x2 + 2, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 2451 |
[a__snd(x1)] | = | x1 + 32279 |
[splitAt(x1, x2)] | = | x2 + 5 |
[a__take#(x1, x2)] | = | x1 + 1 |
[a__natsFrom(x1)] | = | x1 + 2451 |
[a__fst(x1)] | = | x1 + 1 |
[tail(x1)] | = | x1 + 1324 |
[mark#(x1)] | = | 1 |
[0] | = | 28886 |
[a__u(x1,...,x4)] | = | max(x1 + 0, x3 + 8, x4 + 1, 0) |
[sel(x1, x2)] | = | x2 + 44252 |
[afterNth(x1, x2)] | = | x2 + 34525 |
[nil] | = | 1 |
[a__splitAt(x1, x2)] | = | x2 + 5 |
[a__sel#(x1, x2)] | = | x1 + x2 + 1 |
[a__sel(x1, x2)] | = | x2 + 44252 |
[head(x1)] | = | x1 + 9726 |
[a__afterNth#(x1, x2)] | = | x1 + x2 + 1 |
[a__splitAt#(x1, x2)] | = | x1 + 0 |
[cons(x1, x2)] | = | max(x1 + 4, x2 + 0, 0) |
[snd(x1)] | = | x1 + 32279 |
[a__u#(x1,...,x4)] | = | x3 + 1 |
[a__take(x1, x2)] | = | x2 + 7 |
[a__fst#(x1)] | = | 1 |
[a__tail(x1)] | = | x1 + 1324 |
[a__tail#(x1)] | = | 1 |
[a__head(x1)] | = | x1 + 9726 |
mark(tail(X)) | → | a__tail(mark(X)) | (18) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (4) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (15) |
a__tail(cons(N,XS)) | → | mark(XS) | (8) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (1) |
a__snd(pair(XS,YS)) | → | mark(YS) | (3) |
mark(u(X1,X2,X3,X4)) | → | a__u(mark(X1),X2,X3,X4) | (16) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (21) |
a__take(X1,X2) | → | take(X1,X2) | (36) |
mark(nil) | → | nil | (26) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (19) |
a__head(X) | → | head(X) | (32) |
mark(head(X)) | → | a__head(mark(X)) | (17) |
a__natsFrom(X) | → | natsFrom(X) | (27) |
a__sel(X1,X2) | → | sel(X1,X2) | (34) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (22) |
a__fst(X) | → | fst(X) | (28) |
a__splitAt(s(N),cons(X,XS)) | → | a__u(a__splitAt(mark(N),mark(XS)),N,X,XS) | (5) |
a__tail(X) | → | tail(X) | (33) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (10) |
a__head(cons(N,XS)) | → | mark(N) | (7) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (20) |
mark(0) | → | 0 | (25) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (30) |
mark(snd(X)) | → | a__snd(mark(X)) | (14) |
a__u(X1,X2,X3,X4) | → | u(X1,X2,X3,X4) | (31) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (12) |
mark(s(X)) | → | s(mark(X)) | (23) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (24) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (11) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (9) |
mark(fst(X)) | → | a__fst(mark(X)) | (13) |
a__u(pair(YS,ZS),N,X,XS) | → | pair(cons(mark(X),YS),mark(ZS)) | (6) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
a__snd(X) | → | snd(X) | (29) |
a__fst(pair(XS,YS)) | → | mark(XS) | (2) |
a__splitAt#(s(N),cons(X,XS)) | → | a__splitAt#(mark(N),mark(XS)) | (60) |
The dependency pairs are split into 0 components.
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (38) |
mark#(s(X)) | → | mark#(X) | (81) |
[s(x1)] | = | x1 + 1 |
[a__head#(x1)] | = | 1 |
[a__natsFrom#(x1)] | = | 0 |
[a__snd#(x1)] | = | 0 |
[a__afterNth(x1, x2)] | = | 1 |
[u(x1,...,x4)] | = | x1 + 2 |
[take(x1, x2)] | = | 2 |
[pair(x1, x2)] | = | 5 |
[fst(x1)] | = | 5 |
[natsFrom(x1)] | = | 5 |
[a__snd(x1)] | = | 2 |
[splitAt(x1, x2)] | = | x1 + 5 |
[a__take#(x1, x2)] | = | 0 |
[a__natsFrom(x1)] | = | 4 |
[a__fst(x1)] | = | 4 |
[tail(x1)] | = | x1 + 3 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 4 |
[a__u(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 1 |
[sel(x1, x2)] | = | x1 + 2 |
[afterNth(x1, x2)] | = | x2 + 2 |
[nil] | = | 4 |
[a__splitAt(x1, x2)] | = | 4 |
[a__sel#(x1, x2)] | = | 0 |
[mark(x1)] | = | 3 |
[a__sel(x1, x2)] | = | x2 + 1 |
[head(x1)] | = | x1 + 5 |
[a__afterNth#(x1, x2)] | = | 0 |
[a__splitAt#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x1 + 2 |
[snd(x1)] | = | x1 + 3 |
[a__u#(x1,...,x4)] | = | 0 |
[a__take(x1, x2)] | = | x2 + 1 |
[a__fst#(x1)] | = | 0 |
[a__tail(x1)] | = | 2 |
[a__tail#(x1)] | = | 1 |
[a__head(x1)] | = | 4 |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (38) |
mark#(s(X)) | → | mark#(X) | (81) |
The dependency pairs are split into 0 components.