The rewrite relation of the following TRS is considered.
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (1) |
active(fst(pair(XS,YS))) | → | mark(XS) | (2) |
active(snd(pair(XS,YS))) | → | mark(YS) | (3) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (4) |
active(splitAt(s(N),cons(X,XS))) | → | mark(u(splitAt(N,XS),N,X,XS)) | (5) |
active(u(pair(YS,ZS),N,X,XS)) | → | mark(pair(cons(X,YS),ZS)) | (6) |
active(head(cons(N,XS))) | → | mark(N) | (7) |
active(tail(cons(N,XS))) | → | mark(XS) | (8) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (9) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (10) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (11) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (12) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (13) |
mark(s(X)) | → | active(s(mark(X))) | (14) |
mark(fst(X)) | → | active(fst(mark(X))) | (15) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (16) |
mark(snd(X)) | → | active(snd(mark(X))) | (17) |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (18) |
mark(0) | → | active(0) | (19) |
mark(nil) | → | active(nil) | (20) |
mark(u(X1,X2,X3,X4)) | → | active(u(mark(X1),X2,X3,X4)) | (21) |
mark(head(X)) | → | active(head(mark(X))) | (22) |
mark(tail(X)) | → | active(tail(mark(X))) | (23) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (24) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (25) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (26) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
s(mark(X)) | → | s(X) | (33) |
s(active(X)) | → | s(X) | (34) |
fst(mark(X)) | → | fst(X) | (35) |
fst(active(X)) | → | fst(X) | (36) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
head(mark(X)) | → | head(X) | (55) |
head(active(X)) | → | head(X) | (56) |
tail(mark(X)) | → | tail(X) | (57) |
tail(active(X)) | → | tail(X) | (58) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
There are 115 ruless (increase limit for explicit display).
The dependency pairs are split into 14 components.
mark#(fst(X)) | → | mark#(X) | (140) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (183) |
mark#(s(X)) | → | active#(s(mark(X))) | (138) |
active#(afterNth(N,XS)) | → | mark#(snd(splitAt(N,XS))) | (136) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (134) |
mark#(snd(X)) | → | mark#(X) | (131) |
mark#(take(X1,X2)) | → | mark#(X2) | (130) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (129) |
active#(fst(pair(XS,YS))) | → | mark#(XS) | (175) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (117) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
active#(splitAt(0,XS)) | → | mark#(pair(nil,XS)) | (115) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (116) |
mark#(head(X)) | → | mark#(X) | (114) |
mark#(sel(X1,X2)) | → | mark#(X1) | (170) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (167) |
mark#(pair(X1,X2)) | → | mark#(X2) | (112) |
active#(tail(cons(N,XS))) | → | mark#(XS) | (165) |
mark#(cons(X1,X2)) | → | mark#(X1) | (166) |
active#(take(N,XS)) | → | mark#(fst(splitAt(N,XS))) | (164) |
mark#(s(X)) | → | mark#(X) | (108) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (101) |
active#(sel(N,XS)) | → | mark#(head(afterNth(N,XS))) | (159) |
active#(head(cons(N,XS))) | → | mark#(N) | (98) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (96) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(head(X)) | → | active#(head(mark(X))) | (95) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (156) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (152) |
mark#(pair(X1,X2)) | → | mark#(X1) | (86) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (84) |
active#(snd(pair(XS,YS))) | → | mark#(YS) | (85) |
mark#(sel(X1,X2)) | → | mark#(X2) | (83) |
mark#(tail(X)) | → | mark#(X) | (82) |
mark#(pair(X1,X2)) | → | active#(pair(mark(X1),mark(X2))) | (81) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (80) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
mark#(natsFrom(X)) | → | mark#(X) | (78) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (144) |
mark#(take(X1,X2)) | → | mark#(X1) | (142) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (72) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | 2 |
[take(x1, x2)] | = | 2 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 1 |
[fst(x1)] | = | 2 |
[natsFrom(x1)] | = | 2 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 2 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 2 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 2 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 2 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | 2 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 2 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
mark#(s(X)) | → | active#(s(mark(X))) | (138) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (117) |
mark#(pair(X1,X2)) | → | active#(pair(mark(X1),mark(X2))) | (81) |
The dependency pairs are split into 1 component.
mark#(splitAt(X1,X2)) | → | mark#(X2) | (80) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (84) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
active#(splitAt(0,XS)) | → | mark#(pair(nil,XS)) | (115) |
mark#(fst(X)) | → | mark#(X) | (140) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (134) |
active#(tail(cons(N,XS))) | → | mark#(XS) | (165) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (167) |
active#(snd(pair(XS,YS))) | → | mark#(YS) | (85) |
mark#(pair(X1,X2)) | → | mark#(X2) | (112) |
mark#(pair(X1,X2)) | → | mark#(X1) | (86) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (116) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
mark#(take(X1,X2)) | → | mark#(X2) | (130) |
mark#(take(X1,X2)) | → | mark#(X1) | (142) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (72) |
mark#(snd(X)) | → | mark#(X) | (131) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (183) |
mark#(head(X)) | → | mark#(X) | (114) |
mark#(head(X)) | → | active#(head(mark(X))) | (95) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
active#(take(N,XS)) | → | mark#(fst(splitAt(N,XS))) | (164) |
active#(head(cons(N,XS))) | → | mark#(N) | (98) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (101) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (96) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (129) |
mark#(s(X)) | → | mark#(X) | (108) |
mark#(natsFrom(X)) | → | mark#(X) | (78) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (152) |
mark#(tail(X)) | → | mark#(X) | (82) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (144) |
mark#(sel(X1,X2)) | → | mark#(X2) | (83) |
mark#(sel(X1,X2)) | → | mark#(X1) | (170) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (156) |
active#(afterNth(N,XS)) | → | mark#(snd(splitAt(N,XS))) | (136) |
active#(sel(N,XS)) | → | mark#(head(afterNth(N,XS))) | (159) |
mark#(cons(X1,X2)) | → | mark#(X1) | (166) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
active#(fst(pair(XS,YS))) | → | mark#(XS) | (175) |
[cons#(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[take#(x1, x2)] | = | max(0) |
[u(x1,...,x4)] | = | max(x1 + 0, x2 + 8, x3 + 6, x4 + 5, 0) |
[take(x1, x2)] | = | max(x1 + 12, x2 + 11, 0) |
[u#(x1,...,x4)] | = | max(0) |
[pair(x1, x2)] | = | max(x1 + 2, x2 + 1, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 3 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | max(x1 + 9, x2 + 5, 0) |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | x1 + 1 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 23979 |
[sel#(x1, x2)] | = | max(0) |
[sel(x1, x2)] | = | max(x1 + 13, x2 + 15, 0) |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | max(x1 + 11, x2 + 13, 0) |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | max(0) |
[mark(x1)] | = | x1 + 0 |
[afterNth#(x1, x2)] | = | max(0) |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | x1 + 1 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | max(x1 + 2, x2 + 0, 0) |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | x1 + 1 |
[pair#(x1, x2)] | = | max(0) |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (18) |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (4) |
mark(fst(X)) | → | active(fst(mark(X))) | (15) |
active(tail(cons(N,XS))) | → | mark(XS) | (8) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (1) |
active(snd(pair(XS,YS))) | → | mark(YS) | (3) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (16) |
mark(u(X1,X2,X3,X4)) | → | active(u(mark(X1),X2,X3,X4)) | (21) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (26) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
mark(0) | → | active(0) | (19) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
mark(snd(X)) | → | active(snd(mark(X))) | (17) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
mark(head(X)) | → | active(head(mark(X))) | (22) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
active(splitAt(s(N),cons(X,XS))) | → | mark(u(splitAt(N,XS),N,X,XS)) | (5) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (10) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
active(head(cons(N,XS))) | → | mark(N) | (7) |
mark(nil) | → | active(nil) | (20) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (25) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
mark(s(X)) | → | active(s(mark(X))) | (14) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (12) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
mark(tail(X)) | → | active(tail(mark(X))) | (23) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (24) |
tail(mark(X)) | → | tail(X) | (57) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (11) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (9) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (13) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
active(u(pair(YS,ZS),N,X,XS)) | → | mark(pair(cons(X,YS),ZS)) | (6) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
active(fst(pair(XS,YS))) | → | mark(XS) | (2) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (80) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (84) |
active#(splitAt(0,XS)) | → | mark#(pair(nil,XS)) | (115) |
mark#(fst(X)) | → | mark#(X) | (140) |
active#(tail(cons(N,XS))) | → | mark#(XS) | (165) |
active#(snd(pair(XS,YS))) | → | mark#(YS) | (85) |
mark#(pair(X1,X2)) | → | mark#(X2) | (112) |
mark#(pair(X1,X2)) | → | mark#(X1) | (86) |
mark#(take(X1,X2)) | → | mark#(X2) | (130) |
mark#(take(X1,X2)) | → | mark#(X1) | (142) |
mark#(snd(X)) | → | mark#(X) | (131) |
mark#(head(X)) | → | mark#(X) | (114) |
active#(take(N,XS)) | → | mark#(fst(splitAt(N,XS))) | (164) |
active#(head(cons(N,XS))) | → | mark#(N) | (98) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (101) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (96) |
mark#(natsFrom(X)) | → | mark#(X) | (78) |
mark#(tail(X)) | → | mark#(X) | (82) |
mark#(sel(X1,X2)) | → | mark#(X2) | (83) |
mark#(sel(X1,X2)) | → | mark#(X1) | (170) |
active#(afterNth(N,XS)) | → | mark#(snd(splitAt(N,XS))) | (136) |
active#(sel(N,XS)) | → | mark#(head(afterNth(N,XS))) | (159) |
mark#(cons(X1,X2)) | → | mark#(X1) | (166) |
active#(fst(pair(XS,YS))) | → | mark#(XS) | (175) |
The dependency pairs are split into 1 component.
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (134) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (167) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (116) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (72) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (183) |
mark#(head(X)) | → | active#(head(mark(X))) | (95) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (129) |
mark#(s(X)) | → | mark#(X) | (108) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (152) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (144) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (156) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x1 + 0 |
[take(x1, x2)] | = | x1 + x2 + 1 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 0 |
[fst(x1)] | = | 1 |
[natsFrom(x1)] | = | 16674 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 0 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | x1 + 1 |
[mark#(x1)] | = | x1 + 1 |
[0] | = | 15943 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x2 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 2 |
[nil] | = | 27376 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 28874 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | 3153 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 0 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 1 |
[snd(x1)] | = | x1 + 1 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
head(mark(X)) | → | head(X) | (55) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (134) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (72) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (183) |
mark#(head(X)) | → | active#(head(mark(X))) | (95) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (129) |
mark#(s(X)) | → | mark#(X) | (108) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (152) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (144) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (156) |
The dependency pairs are split into 1 component.
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (167) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (116) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | 25532 |
[take(x1, x2)] | = | 1 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 1 |
[fst(x1)] | = | 1 |
[natsFrom(x1)] | = | 25533 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 25532 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 25532 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | 1 |
[head(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 1 |
[pair#(x1, x2)] | = | 0 |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (18) |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (4) |
mark(fst(X)) | → | active(fst(mark(X))) | (15) |
active(tail(cons(N,XS))) | → | mark(XS) | (8) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (1) |
active(snd(pair(XS,YS))) | → | mark(YS) | (3) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (16) |
mark(u(X1,X2,X3,X4)) | → | active(u(mark(X1),X2,X3,X4)) | (21) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (26) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
mark(0) | → | active(0) | (19) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
mark(snd(X)) | → | active(snd(mark(X))) | (17) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
mark(head(X)) | → | active(head(mark(X))) | (22) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
active(splitAt(s(N),cons(X,XS))) | → | mark(u(splitAt(N,XS),N,X,XS)) | (5) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (10) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
active(head(cons(N,XS))) | → | mark(N) | (7) |
mark(nil) | → | active(nil) | (20) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (25) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
mark(s(X)) | → | active(s(mark(X))) | (14) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (12) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
mark(tail(X)) | → | active(tail(mark(X))) | (23) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (24) |
tail(mark(X)) | → | tail(X) | (57) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (11) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (9) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (13) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
active(u(pair(YS,ZS),N,X,XS)) | → | mark(pair(cons(X,YS),ZS)) | (6) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
active(fst(pair(XS,YS))) | → | mark(XS) | (2) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (167) |
The dependency pairs are split into 1 component.
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (116) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
π(cons#) | = | 2 |
π(fst) | = | 1 |
π(sel#) | = | 2 |
π(tail#) | = | 1 |
π(splitAt#) | = | 1 |
π(mark) | = | 1 |
π(afterNth#) | = | 1 |
π(active) | = | 1 |
π(snd#) | = | 1 |
π(snd) | = | 1 |
prec(s) | = | 7 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(take#) | = | 0 | status(take#) | = | [] | list-extension(take#) | = | Lex | ||
prec(u) | = | 2 | status(u) | = | [1] | list-extension(u) | = | Lex | ||
prec(take) | = | 3 | status(take) | = | [] | list-extension(take) | = | Lex | ||
prec(u#) | = | 0 | status(u#) | = | [4, 1, 2] | list-extension(u#) | = | Lex | ||
prec(pair) | = | 0 | status(pair) | = | [2] | list-extension(pair) | = | Lex | ||
prec(natsFrom) | = | 7 | status(natsFrom) | = | [] | list-extension(natsFrom) | = | Lex | ||
prec(head#) | = | 0 | status(head#) | = | [] | list-extension(head#) | = | Lex | ||
prec(splitAt) | = | 4 | status(splitAt) | = | [1] | list-extension(splitAt) | = | Lex | ||
prec(fst#) | = | 0 | status(fst#) | = | [] | list-extension(fst#) | = | Lex | ||
prec(tail) | = | 4 | status(tail) | = | [1] | list-extension(tail) | = | Lex | ||
prec(mark#) | = | 1 | status(mark#) | = | [1] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 3 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(sel) | = | 7 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(afterNth) | = | 3 | status(afterNth) | = | [1] | list-extension(afterNth) | = | Lex | ||
prec(nil) | = | 6 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(head) | = | 6 | status(head) | = | [] | list-extension(head) | = | Lex | ||
prec(cons) | = | 6 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(natsFrom#) | = | 0 | status(natsFrom#) | = | [] | list-extension(natsFrom#) | = | Lex | ||
prec(active#) | = | 1 | status(active#) | = | [1] | list-extension(active#) | = | Lex | ||
prec(pair#) | = | 0 | status(pair#) | = | [2, 1] | list-extension(pair#) | = | Lex |
[s(x1)] | = | x1 + 0 |
[take#(x1, x2)] | = | x2 + 1 |
[u(x1,...,x4)] | = | max(x1 + 0, x2 + 25534, x3 + 102138, x4 + 51069, 0) |
[take(x1, x2)] | = | x1 + x2 + 76606 |
[u#(x1,...,x4)] | = | max(x1 + 1, x2 + 1, x4 + 1, 0) |
[pair(x1, x2)] | = | max(x1 + 76603, x2 + 25532, 0) |
[natsFrom(x1)] | = | x1 + 25536 |
[head#(x1)] | = | 1 |
[splitAt(x1, x2)] | = | x1 + x2 + 76605 |
[fst#(x1)] | = | 1 |
[tail(x1)] | = | x1 + 5969 |
[mark#(x1)] | = | x1 + 51070 |
[0] | = | 0 |
[sel(x1, x2)] | = | x1 + x2 + 97709 |
[s#(x1)] | = | 1 |
[afterNth(x1, x2)] | = | x1 + x2 + 94130 |
[nil] | = | 0 |
[head(x1)] | = | x1 + 3578 |
[cons(x1, x2)] | = | max(x1 + 25535, x2 + 0, 0) |
[natsFrom#(x1)] | = | 1 |
[active#(x1)] | = | x1 + 51070 |
[pair#(x1, x2)] | = | max(x1 + 1, x2 + 1, 0) |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (18) |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (4) |
mark(fst(X)) | → | active(fst(mark(X))) | (15) |
active(tail(cons(N,XS))) | → | mark(XS) | (8) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (1) |
active(snd(pair(XS,YS))) | → | mark(YS) | (3) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (16) |
mark(u(X1,X2,X3,X4)) | → | active(u(mark(X1),X2,X3,X4)) | (21) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (26) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
mark(0) | → | active(0) | (19) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
mark(snd(X)) | → | active(snd(mark(X))) | (17) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
mark(head(X)) | → | active(head(mark(X))) | (22) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
active(splitAt(s(N),cons(X,XS))) | → | mark(u(splitAt(N,XS),N,X,XS)) | (5) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (10) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
active(head(cons(N,XS))) | → | mark(N) | (7) |
mark(nil) | → | active(nil) | (20) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (25) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
mark(s(X)) | → | active(s(mark(X))) | (14) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (12) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
mark(tail(X)) | → | active(tail(mark(X))) | (23) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (24) |
tail(mark(X)) | → | tail(X) | (57) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (11) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (9) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (13) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
active(u(pair(YS,ZS),N,X,XS)) | → | mark(pair(cons(X,YS),ZS)) | (6) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
active(fst(pair(XS,YS))) | → | mark(XS) | (2) |
mark#(u(X1,X2,X3,X4)) | → | mark#(X1) | (116) |
The dependency pairs are split into 1 component.
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | 31250 |
[take(x1, x2)] | = | x1 + x2 + 1 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 31249 |
[fst(x1)] | = | 1 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + 31251 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 8855 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + x2 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + 1 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | 1 |
[head(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 31250 |
[snd(x1)] | = | 1 |
[pair#(x1, x2)] | = | 0 |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (18) |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (4) |
mark(fst(X)) | → | active(fst(mark(X))) | (15) |
active(tail(cons(N,XS))) | → | mark(XS) | (8) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (1) |
active(snd(pair(XS,YS))) | → | mark(YS) | (3) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (16) |
mark(u(X1,X2,X3,X4)) | → | active(u(mark(X1),X2,X3,X4)) | (21) |
fst(active(X)) | → | fst(X) | (36) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (26) |
mark(0) | → | active(0) | (19) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
mark(snd(X)) | → | active(snd(mark(X))) | (17) |
mark(head(X)) | → | active(head(mark(X))) | (22) |
active(splitAt(s(N),cons(X,XS))) | → | mark(u(splitAt(N,XS),N,X,XS)) | (5) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (10) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
active(head(cons(N,XS))) | → | mark(N) | (7) |
mark(nil) | → | active(nil) | (20) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (25) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
mark(s(X)) | → | active(s(mark(X))) | (14) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (12) |
mark(tail(X)) | → | active(tail(mark(X))) | (23) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (24) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (11) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (9) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (13) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
head(mark(X)) | → | head(X) | (55) |
active(u(pair(YS,ZS),N,X,XS)) | → | mark(pair(cons(X,YS),ZS)) | (6) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
active(fst(pair(XS,YS))) | → | mark(XS) | (2) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
active#(u(pair(YS,ZS),N,X,XS)) | → | mark#(pair(cons(X,YS),ZS)) | (172) |
The dependency pairs are split into 1 component.
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | 1 |
[take(x1, x2)] | = | 1 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 1 |
[fst(x1)] | = | 1 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 3 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | 1 |
[head(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 1 |
[pair#(x1, x2)] | = | 0 |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (18) |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (4) |
mark(fst(X)) | → | active(fst(mark(X))) | (15) |
active(tail(cons(N,XS))) | → | mark(XS) | (8) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (1) |
active(snd(pair(XS,YS))) | → | mark(YS) | (3) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (16) |
mark(u(X1,X2,X3,X4)) | → | active(u(mark(X1),X2,X3,X4)) | (21) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (26) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
mark(0) | → | active(0) | (19) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
mark(snd(X)) | → | active(snd(mark(X))) | (17) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
mark(head(X)) | → | active(head(mark(X))) | (22) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
active(splitAt(s(N),cons(X,XS))) | → | mark(u(splitAt(N,XS),N,X,XS)) | (5) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (10) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
active(head(cons(N,XS))) | → | mark(N) | (7) |
mark(nil) | → | active(nil) | (20) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (25) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
mark(s(X)) | → | active(s(mark(X))) | (14) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (12) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
mark(tail(X)) | → | active(tail(mark(X))) | (23) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (24) |
tail(mark(X)) | → | tail(X) | (57) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (11) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (9) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (13) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
active(u(pair(YS,ZS),N,X,XS)) | → | mark(pair(cons(X,YS),ZS)) | (6) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
active(fst(pair(XS,YS))) | → | mark(XS) | (2) |
mark#(u(X1,X2,X3,X4)) | → | active#(u(mark(X1),X2,X3,X4)) | (146) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(u(splitAt(N,XS),N,X,XS)) | (169) |
The dependency pairs are split into 0 components.
sel#(X1,active(X2)) | → | sel#(X1,X2) | (137) |
sel#(active(X1),X2) | → | sel#(X1,X2) | (133) |
sel#(X1,mark(X2)) | → | sel#(X1,X2) | (128) |
sel#(mark(X1),X2) | → | sel#(X1,X2) | (163) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 26980 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 26796 |
[take(x1, x2)] | = | 1 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 26798 |
[fst(x1)] | = | 30929 |
[natsFrom(x1)] | = | 20694 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 26794 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 42394 |
[mark#(x1)] | = | 2 |
[0] | = | 60401 |
[sel#(x1, x2)] | = | x1 + x2 + 0 |
[sel(x1, x2)] | = | 36347 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 49619 |
[nil] | = | 5082 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 36349 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 20696 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 49621 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
sel#(X1,active(X2)) | → | sel#(X1,X2) | (137) |
sel#(active(X1),X2) | → | sel#(X1,X2) | (133) |
sel#(X1,mark(X2)) | → | sel#(X1,X2) | (128) |
sel#(mark(X1),X2) | → | sel#(X1,X2) | (163) |
The dependency pairs are split into 0 components.
tail#(active(X)) | → | tail#(X) | (109) |
tail#(mark(X)) | → | tail#(X) | (149) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 32755 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 29193 |
[take(x1, x2)] | = | 38411 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 29195 |
[fst(x1)] | = | 38413 |
[natsFrom(x1)] | = | 3010 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 29191 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 36330 |
[mark#(x1)] | = | 2 |
[0] | = | 60401 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 26538 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 55531 |
[nil] | = | 31354 |
[tail#(x1)] | = | x1 + 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 26540 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 3012 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 55533 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
tail#(active(X)) | → | tail#(X) | (109) |
tail#(mark(X)) | → | tail#(X) | (149) |
The dependency pairs are split into 0 components.
afterNth#(mark(X1),X2) | → | afterNth#(X1,X2) | (168) |
afterNth#(X1,active(X2)) | → | afterNth#(X1,X2) | (151) |
afterNth#(active(X1),X2) | → | afterNth#(X1,X2) | (150) |
afterNth#(X1,mark(X2)) | → | afterNth#(X1,X2) | (77) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 63507 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 3 |
[take(x1, x2)] | = | 31797 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 29195 |
[fst(x1)] | = | 62525 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 46181 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 7362 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 24194 |
[nil] | = | 44051 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | x1 + 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 26985 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 3 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 24196 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
afterNth#(mark(X1),X2) | → | afterNth#(X1,X2) | (168) |
afterNth#(active(X1),X2) | → | afterNth#(X1,X2) | (150) |
The dependency pairs are split into 1 component.
afterNth#(X1,mark(X2)) | → | afterNth#(X1,X2) | (77) |
afterNth#(X1,active(X2)) | → | afterNth#(X1,X2) | (151) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 98239 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 33474 |
[take(x1, x2)] | = | 31797 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 33476 |
[fst(x1)] | = | 58870 |
[natsFrom(x1)] | = | 11403 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 33472 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 55220 |
[mark#(x1)] | = | 2 |
[0] | = | 46181 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 31521 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 50839 |
[nil] | = | 37639 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | x2 + 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 31523 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 11405 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 50841 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
afterNth#(X1,mark(X2)) | → | afterNth#(X1,X2) | (77) |
afterNth#(X1,active(X2)) | → | afterNth#(X1,X2) | (151) |
The dependency pairs are split into 0 components.
snd#(mark(X)) | → | snd#(X) | (177) |
snd#(active(X)) | → | snd#(X) | (143) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 16688 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 43689 |
[take(x1, x2)] | = | 21358 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 43691 |
[fst(x1)] | = | 21360 |
[natsFrom(x1)] | = | 29663 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 43687 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 31161 |
[mark#(x1)] | = | 2 |
[0] | = | 40562 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 37698 |
[nil] | = | 27514 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 31584 |
[snd#(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | 29665 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 37700 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
snd#(mark(X)) | → | snd#(X) | (177) |
snd#(active(X)) | → | snd#(X) | (143) |
The dependency pairs are split into 0 components.
u#(X1,X2,X3,active(X4)) | → | u#(X1,X2,X3,X4) | (182) |
u#(X1,X2,X3,mark(X4)) | → | u#(X1,X2,X3,X4) | (132) |
u#(X1,mark(X2),X3,X4) | → | u#(X1,X2,X3,X4) | (126) |
u#(X1,active(X2),X3,X4) | → | u#(X1,X2,X3,X4) | (176) |
u#(active(X1),X2,X3,X4) | → | u#(X1,X2,X3,X4) | (119) |
u#(X1,X2,active(X3),X4) | → | u#(X1,X2,X3,X4) | (111) |
u#(X1,X2,mark(X3),X4) | → | u#(X1,X2,X3,X4) | (103) |
u#(mark(X1),X2,X3,X4) | → | u#(X1,X2,X3,X4) | (145) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 4685 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 24911 |
[take(x1, x2)] | = | 13701 |
[u#(x1,...,x4)] | = | x1 + x2 + 0 |
[pair(x1, x2)] | = | 24913 |
[fst(x1)] | = | 13703 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 24909 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 23539 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 43242 |
[nil] | = | 1315 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 3 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 3 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 43244 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
u#(X1,mark(X2),X3,X4) | → | u#(X1,X2,X3,X4) | (126) |
u#(X1,active(X2),X3,X4) | → | u#(X1,X2,X3,X4) | (176) |
u#(active(X1),X2,X3,X4) | → | u#(X1,X2,X3,X4) | (119) |
u#(mark(X1),X2,X3,X4) | → | u#(X1,X2,X3,X4) | (145) |
The dependency pairs are split into 1 component.
u#(X1,X2,X3,mark(X4)) | → | u#(X1,X2,X3,X4) | (132) |
u#(X1,X2,X3,active(X4)) | → | u#(X1,X2,X3,X4) | (182) |
u#(X1,X2,mark(X3),X4) | → | u#(X1,X2,X3,X4) | (103) |
u#(X1,X2,active(X3),X4) | → | u#(X1,X2,X3,X4) | (111) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 13068 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 17039 |
[take(x1, x2)] | = | 47538 |
[u#(x1,...,x4)] | = | x3 + 0 |
[pair(x1, x2)] | = | 46695 |
[fst(x1)] | = | 47540 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 17412 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 54392 |
[nil] | = | 45153 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 19316 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 31826 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 54394 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
u#(X1,X2,mark(X3),X4) | → | u#(X1,X2,X3,X4) | (103) |
u#(X1,X2,active(X3),X4) | → | u#(X1,X2,X3,X4) | (111) |
The dependency pairs are split into 1 component.
u#(X1,X2,X3,mark(X4)) | → | u#(X1,X2,X3,X4) | (132) |
u#(X1,X2,X3,active(X4)) | → | u#(X1,X2,X3,X4) | (182) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 34933 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x3 + x4 + 5105 |
[take(x1, x2)] | = | 35494 |
[u#(x1,...,x4)] | = | x4 + 0 |
[pair(x1, x2)] | = | 5107 |
[fst(x1)] | = | 35496 |
[natsFrom(x1)] | = | 12760 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 5103 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 50256 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 31657 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 28438 |
[nil] | = | 29140 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 31659 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 12762 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 28440 |
[pair#(x1, x2)] | = | 0 |
u(X1,X2,X3,mark(X4)) | → | u(X1,X2,X3,X4) | (50) |
u(X1,X2,X3,active(X4)) | → | u(X1,X2,X3,X4) | (54) |
fst(active(X)) | → | fst(X) | (36) |
take(X1,mark(X2)) | → | take(X1,X2) | (68) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (63) |
cons(X1,active(X2)) | → | cons(X1,X2) | (32) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (60) |
natsFrom(mark(X)) | → | natsFrom(X) | (27) |
s(active(X)) | → | s(X) | (34) |
natsFrom(active(X)) | → | natsFrom(X) | (28) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (65) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (33) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (64) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
u(X1,X2,mark(X3),X4) | → | u(X1,X2,X3,X4) | (49) |
u(X1,active(X2),X3,X4) | → | u(X1,X2,X3,X4) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (30) |
sel(X1,active(X2)) | → | sel(X1,X2) | (62) |
head(active(X)) | → | head(X) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (31) |
take(active(X1),X2) | → | take(X1,X2) | (69) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (45) |
take(X1,active(X2)) | → | take(X1,X2) | (70) |
tail(mark(X)) | → | tail(X) | (57) |
u(active(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (51) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
take(mark(X1),X2) | → | take(X1,X2) | (67) |
head(mark(X)) | → | head(X) | (55) |
sel(mark(X1),X2) | → | sel(X1,X2) | (59) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
sel(active(X1),X2) | → | sel(X1,X2) | (61) |
tail(active(X)) | → | tail(X) | (58) |
u(X1,mark(X2),X3,X4) | → | u(X1,X2,X3,X4) | (48) |
u(X1,X2,active(X3),X4) | → | u(X1,X2,X3,X4) | (53) |
u(mark(X1),X2,X3,X4) | → | u(X1,X2,X3,X4) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
snd(mark(X)) | → | snd(X) | (41) |
snd(active(X)) | → | snd(X) | (42) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (46) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (66) |
fst(mark(X)) | → | fst(X) | (35) |
cons(mark(X1),X2) | → | cons(X1,X2) | (29) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (43) |
u#(X1,X2,X3,mark(X4)) | → | u#(X1,X2,X3,X4) | (132) |
u#(X1,X2,X3,active(X4)) | → | u#(X1,X2,X3,X4) | (182) |
The dependency pairs are split into 0 components.
cons#(mark(X1),X2) | → | cons#(X1,X2) | (173) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (90) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (89) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (76) |
[cons#(x1, x2)] | = | x1 + x2 + 0 |
[s(x1)] | = | 29350 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x1 + x2 + x4 + 31327 |
[take(x1, x2)] | = | 43096 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | x1 + 1 |
[fst(x1)] | = | 74423 |
[natsFrom(x1)] | = | x1 + 30470 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 20374 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 54753 |
[mark#(x1)] | = | 2 |
[0] | = | 42507 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + x2 + 42351 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 12770 |
[nil] | = | 51700 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 31327 |
[head(x1)] | = | x1 + 60908 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 62654 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 23723 |
[pair#(x1, x2)] | = | 0 |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (173) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (90) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (89) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (76) |
The dependency pairs are split into 0 components.
natsFrom#(mark(X)) | → | natsFrom#(X) | (121) |
natsFrom#(active(X)) | → | natsFrom#(X) | (88) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 27667 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x4 + 82012 |
[take(x1, x2)] | = | 31241 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 82014 |
[fst(x1)] | = | x1 + 24327 |
[natsFrom(x1)] | = | 23691 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 30650 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 40630 |
[mark#(x1)] | = | 2 |
[0] | = | 1602 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 42117 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 33810 |
[nil] | = | 61135 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 42119 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 23693 |
[natsFrom#(x1)] | = | x1 + 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 3162 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
natsFrom#(mark(X)) | → | natsFrom#(X) | (121) |
natsFrom#(active(X)) | → | natsFrom#(X) | (88) |
The dependency pairs are split into 0 components.
s#(active(X)) | → | s#(X) | (174) |
s#(mark(X)) | → | s#(X) | (104) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x4 + 7 |
[take(x1, x2)] | = | 44866 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 9 |
[fst(x1)] | = | x1 + 44867 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 1 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 28766 |
[mark#(x1)] | = | 2 |
[0] | = | 6 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 13772 |
[s#(x1)] | = | x1 + 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 43546 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 13774 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 3 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 2 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
s#(active(X)) | → | s#(X) | (174) |
s#(mark(X)) | → | s#(X) | (104) |
The dependency pairs are split into 0 components.
fst#(mark(X)) | → | fst#(X) | (181) |
fst#(active(X)) | → | fst#(X) | (87) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 14258 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x4 + 20230 |
[take(x1, x2)] | = | 7282 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 20232 |
[fst(x1)] | = | x1 + 7283 |
[natsFrom(x1)] | = | 5967 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 1 |
[fst#(x1)] | = | x1 + 0 |
[tail(x1)] | = | 48234 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 54044 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 31370 |
[nil] | = | 48123 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 54046 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 5969 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 31371 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
fst#(mark(X)) | → | fst#(X) | (181) |
fst#(active(X)) | → | fst#(X) | (87) |
The dependency pairs are split into 0 components.
pair#(active(X1),X2) | → | pair#(X1,X2) | (135) |
pair#(X1,mark(X2)) | → | pair#(X1,X2) | (178) |
pair#(mark(X1),X2) | → | pair#(X1,X2) | (110) |
pair#(X1,active(X2)) | → | pair#(X1,X2) | (155) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x4 + 7 |
[take(x1, x2)] | = | 37051 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 9 |
[fst(x1)] | = | x1 + 37052 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 1 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 6 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 31668 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 25319 |
[nil] | = | 22279 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 31670 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 3 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 25320 |
[pair#(x1, x2)] | = | x1 + x2 + 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
pair#(active(X1),X2) | → | pair#(X1,X2) | (135) |
pair#(X1,mark(X2)) | → | pair#(X1,X2) | (178) |
pair#(mark(X1),X2) | → | pair#(X1,X2) | (110) |
pair#(X1,active(X2)) | → | pair#(X1,X2) | (155) |
The dependency pairs are split into 0 components.
take#(mark(X1),X2) | → | take#(X1,X2) | (171) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (106) |
take#(X1,active(X2)) | → | take#(X1,X2) | (99) |
take#(active(X1),X2) | → | take#(X1,X2) | (73) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | x2 + 0 |
[u(x1,...,x4)] | = | x2 + x4 + 10 |
[take(x1, x2)] | = | 48056 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 12 |
[fst(x1)] | = | x1 + 48056 |
[natsFrom(x1)] | = | 3 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 2 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 3 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 29114 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 2 |
[nil] | = | 22279 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 29116 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 5 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 2 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (106) |
take#(X1,active(X2)) | → | take#(X1,X2) | (99) |
The dependency pairs are split into 1 component.
take#(active(X1),X2) | → | take#(X1,X2) | (73) |
take#(mark(X1),X2) | → | take#(X1,X2) | (171) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | x1 + 0 |
[u(x1,...,x4)] | = | x2 + x4 + 15821 |
[take(x1, x2)] | = | 1 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 15823 |
[fst(x1)] | = | x1 + 8092 |
[natsFrom(x1)] | = | 15815 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 1 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 24841 |
[mark#(x1)] | = | 2 |
[0] | = | 14469 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 36730 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 48336 |
[nil] | = | 14426 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 36732 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 15817 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 48337 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
take#(active(X1),X2) | → | take#(X1,X2) | (73) |
take#(mark(X1),X2) | → | take#(X1,X2) | (171) |
The dependency pairs are split into 0 components.
splitAt#(X1,active(X2)) | → | splitAt#(X1,X2) | (100) |
splitAt#(X1,mark(X2)) | → | splitAt#(X1,X2) | (91) |
splitAt#(active(X1),X2) | → | splitAt#(X1,X2) | (79) |
splitAt#(mark(X1),X2) | → | splitAt#(X1,X2) | (71) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x4 + 35739 |
[take(x1, x2)] | = | 12606 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 35741 |
[fst(x1)] | = | x1 + 3031 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 9577 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 2 |
[0] | = | 4029 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 37294 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | x1 + x2 + 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 31000 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 26159 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 27719 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
splitAt#(X1,active(X2)) | → | splitAt#(X1,X2) | (100) |
splitAt#(X1,mark(X2)) | → | splitAt#(X1,X2) | (91) |
splitAt#(active(X1),X2) | → | splitAt#(X1,X2) | (79) |
splitAt#(mark(X1),X2) | → | splitAt#(X1,X2) | (71) |
The dependency pairs are split into 0 components.
head#(active(X)) | → | head#(X) | (92) |
head#(mark(X)) | → | head#(X) | (141) |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[take#(x1, x2)] | = | 0 |
[u(x1,...,x4)] | = | x2 + x4 + 49835 |
[take(x1, x2)] | = | 33741 |
[u#(x1,...,x4)] | = | 0 |
[pair(x1, x2)] | = | 49837 |
[fst(x1)] | = | x1 + 25137 |
[natsFrom(x1)] | = | 41224 |
[head#(x1)] | = | x1 + 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 8606 |
[fst#(x1)] | = | 0 |
[tail(x1)] | = | 3362 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 15026 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 52823 |
[nil] | = | 26641 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 15028 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 41226 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 0 |
[snd(x1)] | = | x1 + 44219 |
[pair#(x1, x2)] | = | 0 |
s(active(X)) | → | s(X) | (34) |
s(mark(X)) | → | s(X) | (33) |
pair(active(X1),X2) | → | pair(X1,X2) | (39) |
pair(X1,active(X2)) | → | pair(X1,X2) | (40) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (38) |
pair(mark(X1),X2) | → | pair(X1,X2) | (37) |
head#(active(X)) | → | head#(X) | (92) |
head#(mark(X)) | → | head#(X) | (141) |
The dependency pairs are split into 0 components.