The rewrite relation of the following TRS is considered.
active(U11(tt,N,X,XS)) | → | mark(U12(splitAt(N,XS),X)) | (1) |
active(U12(pair(YS,ZS),X)) | → | mark(pair(cons(X,YS),ZS)) | (2) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (3) |
active(and(tt,X)) | → | mark(X) | (4) |
active(fst(pair(X,Y))) | → | mark(X) | (5) |
active(head(cons(N,XS))) | → | mark(N) | (6) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (7) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (8) |
active(snd(pair(X,Y))) | → | mark(Y) | (9) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (10) |
active(splitAt(s(N),cons(X,XS))) | → | mark(U11(tt,N,X,XS)) | (11) |
active(tail(cons(N,XS))) | → | mark(XS) | (12) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (13) |
mark(U11(X1,X2,X3,X4)) | → | active(U11(mark(X1),X2,X3,X4)) | (14) |
mark(tt) | → | active(tt) | (15) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (16) |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (17) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (18) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (19) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (20) |
mark(snd(X)) | → | active(snd(mark(X))) | (21) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(fst(X)) | → | active(fst(mark(X))) | (23) |
mark(head(X)) | → | active(head(mark(X))) | (24) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (25) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (27) |
mark(0) | → | active(0) | (28) |
mark(nil) | → | active(nil) | (29) |
mark(tail(X)) | → | active(tail(mark(X))) | (30) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (31) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (56) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (57) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (58) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (59) |
snd(mark(X)) | → | snd(X) | (60) |
snd(active(X)) | → | snd(X) | (61) |
and(mark(X1),X2) | → | and(X1,X2) | (62) |
and(X1,mark(X2)) | → | and(X1,X2) | (63) |
and(active(X1),X2) | → | and(X1,X2) | (64) |
and(X1,active(X2)) | → | and(X1,X2) | (65) |
fst(mark(X)) | → | fst(X) | (66) |
fst(active(X)) | → | fst(X) | (67) |
head(mark(X)) | → | head(X) | (68) |
head(active(X)) | → | head(X) | (69) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
sel(mark(X1),X2) | → | sel(X1,X2) | (74) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (75) |
sel(active(X1),X2) | → | sel(X1,X2) | (76) |
sel(X1,active(X2)) | → | sel(X1,X2) | (77) |
tail(mark(X)) | → | tail(X) | (78) |
tail(active(X)) | → | tail(X) | (79) |
take(mark(X1),X2) | → | take(X1,X2) | (80) |
take(X1,mark(X2)) | → | take(X1,X2) | (81) |
take(active(X1),X2) | → | take(X1,X2) | (82) |
take(X1,active(X2)) | → | take(X1,X2) | (83) |
There are 133 ruless (increase limit for explicit display).
The dependency pairs are split into 16 components.
mark#(pair(X1,X2)) | → | active#(pair(mark(X1),mark(X2))) | (159) |
mark#(s(X)) | → | active#(s(mark(X))) | (213) |
mark#(take(X1,X2)) | → | mark#(X2) | (156) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (157) |
mark#(tail(X)) | → | mark#(X) | (154) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(cons(X1,X2)) | → | mark#(X1) | (210) |
mark#(snd(X)) | → | mark#(X) | (151) |
active#(fst(pair(X,Y))) | → | mark#(X) | (150) |
mark#(pair(X1,X2)) | → | mark#(X2) | (149) |
mark#(U11(X1,X2,X3,X4)) | → | active#(U11(mark(X1),X2,X3,X4)) | (147) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
active#(head(cons(N,XS))) | → | mark#(N) | (135) |
active#(splitAt(0,XS)) | → | mark#(pair(nil,XS)) | (203) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (134) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (131) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (197) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (194) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (128) |
mark#(take(X1,X2)) | → | mark#(X1) | (124) |
active#(snd(pair(X,Y))) | → | mark#(Y) | (188) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (122) |
mark#(natsFrom(X)) | → | mark#(X) | (120) |
mark#(pair(X1,X2)) | → | mark#(X1) | (118) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (185) |
mark#(U11(X1,X2,X3,X4)) | → | mark#(X1) | (110) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (108) |
active#(sel(N,XS)) | → | mark#(head(afterNth(N,XS))) | (106) |
active#(tail(cons(N,XS))) | → | mark#(XS) | (105) |
active#(and(tt,X)) | → | mark#(X) | (180) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (104) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (177) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (99) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (173) |
mark#(head(X)) | → | active#(head(mark(X))) | (96) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
mark#(sel(X1,X2)) | → | mark#(X2) | (170) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (95) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
active#(afterNth(N,XS)) | → | mark#(snd(splitAt(N,XS))) | (93) |
mark#(sel(X1,X2)) | → | mark#(X1) | (168) |
mark#(head(X)) | → | mark#(X) | (166) |
mark#(and(X1,X2)) | → | mark#(X1) | (164) |
active#(take(N,XS)) | → | mark#(fst(splitAt(N,XS))) | (87) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
mark#(fst(X)) | → | mark#(X) | (86) |
[U11(x1,...,x4)] | = | 2 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 2 |
[and(x1, x2)] | = | 2 |
[pair(x1, x2)] | = | 1 |
[fst(x1)] | = | 2 |
[natsFrom(x1)] | = | 2 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 2 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 2 |
[mark#(x1)] | = | 2 |
[0] | = | 4 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 2 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 2 |
[nil] | = | 28941 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | 3 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | 2 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 2 |
[tt] | = | 3027 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
take(mark(X1),X2) | → | take(X1,X2) | (80) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
sel(X1,active(X2)) | → | sel(X1,X2) | (77) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
head(mark(X)) | → | head(X) | (68) |
and(X1,mark(X2)) | → | and(X1,X2) | (63) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
snd(mark(X)) | → | snd(X) | (60) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
and(X1,active(X2)) | → | and(X1,X2) | (65) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (72) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
and(active(X1),X2) | → | and(X1,X2) | (64) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
and(mark(X1),X2) | → | and(X1,X2) | (62) |
take(active(X1),X2) | → | take(X1,X2) | (82) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (56) |
tail(active(X)) | → | tail(X) | (79) |
head(active(X)) | → | head(X) | (69) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
tail(mark(X)) | → | tail(X) | (78) |
take(X1,mark(X2)) | → | take(X1,X2) | (81) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
sel(active(X1),X2) | → | sel(X1,X2) | (76) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (57) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
fst(active(X)) | → | fst(X) | (67) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (59) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
snd(active(X)) | → | snd(X) | (61) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (58) |
sel(mark(X1),X2) | → | sel(X1,X2) | (74) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (75) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
s(active(X)) | → | s(X) | (73) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (66) |
take(X1,active(X2)) | → | take(X1,X2) | (83) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
mark#(pair(X1,X2)) | → | active#(pair(mark(X1),mark(X2))) | (159) |
mark#(s(X)) | → | active#(s(mark(X))) | (213) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (194) |
The dependency pairs are split into 1 component.
mark#(pair(X1,X2)) | → | mark#(X2) | (149) |
mark#(pair(X1,X2)) | → | mark#(X1) | (118) |
active#(and(tt,X)) | → | mark#(X) | (180) |
active#(sel(N,XS)) | → | mark#(head(afterNth(N,XS))) | (106) |
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
active#(afterNth(N,XS)) | → | mark#(snd(splitAt(N,XS))) | (93) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (108) |
mark#(snd(X)) | → | mark#(X) | (151) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (131) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(cons(X1,X2)) | → | mark#(X1) | (210) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (128) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (99) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(sel(X1,X2)) | → | mark#(X2) | (170) |
mark#(sel(X1,X2)) | → | mark#(X1) | (168) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (122) |
mark#(and(X1,X2)) | → | mark#(X1) | (164) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
active#(fst(pair(X,Y))) | → | mark#(X) | (150) |
active#(splitAt(0,XS)) | → | mark#(pair(nil,XS)) | (203) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (173) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (104) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (134) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (197) |
mark#(natsFrom(X)) | → | mark#(X) | (120) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (177) |
mark#(tail(X)) | → | mark#(X) | (154) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (185) |
mark#(U11(X1,X2,X3,X4)) | → | mark#(X1) | (110) |
mark#(U11(X1,X2,X3,X4)) | → | active#(U11(mark(X1),X2,X3,X4)) | (147) |
mark#(take(X1,X2)) | → | mark#(X2) | (156) |
mark#(take(X1,X2)) | → | mark#(X1) | (124) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (157) |
active#(tail(cons(N,XS))) | → | mark#(XS) | (105) |
mark#(fst(X)) | → | mark#(X) | (86) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (95) |
mark#(head(X)) | → | mark#(X) | (166) |
mark#(head(X)) | → | active#(head(mark(X))) | (96) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(snd(pair(X,Y))) | → | mark#(Y) | (188) |
active#(take(N,XS)) | → | mark#(fst(splitAt(N,XS))) | (87) |
active#(head(cons(N,XS))) | → | mark#(N) | (135) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
[U11(x1,...,x4)] | = | max(x1 + 12280, x2 + 52186, x3 + 81592, x4 + 52185, 0) |
[cons#(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[take#(x1, x2)] | = | max(0) |
[take(x1, x2)] | = | max(x1 + 80411, x2 + 80412, 0) |
[and(x1, x2)] | = | max(x1 + 31394, x2 + 31393, 0) |
[pair(x1, x2)] | = | max(x1 + 52183, x2 + 52182, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 41620 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | max(x1 + 52186, x2 + 52185, 0) |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | max(x1 + 0, x2 + 81591, 0) |
[U12#(x1, x2)] | = | max(0) |
[tail(x1)] | = | x1 + 31112 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 31967 |
[sel#(x1, x2)] | = | max(0) |
[sel(x1, x2)] | = | max(x1 + 76886, x2 + 76887, 0) |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | max(x1 + 59817, x2 + 59818, 0) |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | max(0) |
[mark(x1)] | = | x1 + 0 |
[afterNth#(x1, x2)] | = | max(0) |
[U11#(x1,...,x4)] | = | max(0) |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | x1 + 17067 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | max(x1 + 29407, x2 + 0, 0) |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | x1 + 7630 |
[tt] | = | 39904 |
[pair#(x1, x2)] | = | max(0) |
[and#(x1, x2)] | = | max(0) |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (18) |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
take(mark(X1),X2) | → | take(X1,X2) | (80) |
active(and(tt,X)) | → | mark(X) | (4) |
mark(tt) | → | active(tt) | (15) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (8) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
active(U11(tt,N,X,XS)) | → | mark(U12(splitAt(N,XS),X)) | (1) |
sel(X1,active(X2)) | → | sel(X1,X2) | (77) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (3) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (16) |
mark(snd(X)) | → | active(snd(mark(X))) | (21) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
head(mark(X)) | → | head(X) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
and(X1,mark(X2)) | → | and(X1,X2) | (63) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (19) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (17) |
snd(mark(X)) | → | snd(X) | (60) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (27) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(0) | → | active(0) | (28) |
and(X1,active(X2)) | → | and(X1,X2) | (65) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
active(fst(pair(X,Y))) | → | mark(X) | (5) |
s(mark(X)) | → | s(X) | (72) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
and(active(X1),X2) | → | and(X1,X2) | (64) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (10) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (7) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (20) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (25) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
mark(tail(X)) | → | active(tail(mark(X))) | (30) |
and(mark(X1),X2) | → | and(X1,X2) | (62) |
mark(U11(X1,X2,X3,X4)) | → | active(U11(mark(X1),X2,X3,X4)) | (14) |
take(active(X1),X2) | → | take(X1,X2) | (82) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (56) |
tail(active(X)) | → | tail(X) | (79) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (31) |
active(tail(cons(N,XS))) | → | mark(XS) | (12) |
head(active(X)) | → | head(X) | (69) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
tail(mark(X)) | → | tail(X) | (78) |
take(X1,mark(X2)) | → | take(X1,X2) | (81) |
mark(fst(X)) | → | active(fst(mark(X))) | (23) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
mark(head(X)) | → | active(head(mark(X))) | (24) |
sel(active(X1),X2) | → | sel(X1,X2) | (76) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (57) |
active(splitAt(s(N),cons(X,XS))) | → | mark(U11(tt,N,X,XS)) | (11) |
active(snd(pair(X,Y))) | → | mark(Y) | (9) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (13) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
fst(active(X)) | → | fst(X) | (67) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (59) |
active(head(cons(N,XS))) | → | mark(N) | (6) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
snd(active(X)) | → | snd(X) | (61) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (58) |
sel(mark(X1),X2) | → | sel(X1,X2) | (74) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (75) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
s(active(X)) | → | s(X) | (73) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (66) |
take(X1,active(X2)) | → | take(X1,X2) | (83) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
mark(nil) | → | active(nil) | (29) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
active(U12(pair(YS,ZS),X)) | → | mark(pair(cons(X,YS),ZS)) | (2) |
mark#(pair(X1,X2)) | → | mark#(X2) | (149) |
mark#(pair(X1,X2)) | → | mark#(X1) | (118) |
active#(and(tt,X)) | → | mark#(X) | (180) |
active#(sel(N,XS)) | → | mark#(head(afterNth(N,XS))) | (106) |
active#(afterNth(N,XS)) | → | mark#(snd(splitAt(N,XS))) | (93) |
mark#(snd(X)) | → | mark#(X) | (151) |
mark#(cons(X1,X2)) | → | mark#(X1) | (210) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (128) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (99) |
mark#(sel(X1,X2)) | → | mark#(X2) | (170) |
mark#(sel(X1,X2)) | → | mark#(X1) | (168) |
mark#(and(X1,X2)) | → | mark#(X1) | (164) |
active#(fst(pair(X,Y))) | → | mark#(X) | (150) |
active#(splitAt(0,XS)) | → | mark#(pair(nil,XS)) | (203) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (104) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (134) |
mark#(natsFrom(X)) | → | mark#(X) | (120) |
mark#(tail(X)) | → | mark#(X) | (154) |
mark#(U11(X1,X2,X3,X4)) | → | mark#(X1) | (110) |
mark#(take(X1,X2)) | → | mark#(X2) | (156) |
mark#(take(X1,X2)) | → | mark#(X1) | (124) |
active#(tail(cons(N,XS))) | → | mark#(XS) | (105) |
mark#(fst(X)) | → | mark#(X) | (86) |
mark#(head(X)) | → | mark#(X) | (166) |
active#(snd(pair(X,Y))) | → | mark#(Y) | (188) |
active#(take(N,XS)) | → | mark#(fst(splitAt(N,XS))) | (87) |
active#(head(cons(N,XS))) | → | mark#(N) | (135) |
The dependency pairs are split into 1 component.
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (108) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (131) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (122) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (173) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (197) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (177) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (185) |
mark#(U11(X1,X2,X3,X4)) | → | active#(U11(mark(X1),X2,X3,X4)) | (147) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (157) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (95) |
mark#(head(X)) | → | active#(head(mark(X))) | (96) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
[U11(x1,...,x4)] | = | 4 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 21098 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 1 |
[and(x1, x2)] | = | 3 |
[pair(x1, x2)] | = | 0 |
[fst(x1)] | = | 3 |
[natsFrom(x1)] | = | 4 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 4 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 4 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 3 |
[mark#(x1)] | = | 4 |
[0] | = | 3 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 3 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | 2 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | 3 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 1771 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[snd(x1)] | = | 3 |
[tt] | = | 0 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
take(mark(X1),X2) | → | take(X1,X2) | (80) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
sel(X1,active(X2)) | → | sel(X1,X2) | (77) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
head(mark(X)) | → | head(X) | (68) |
and(X1,mark(X2)) | → | and(X1,X2) | (63) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
snd(mark(X)) | → | snd(X) | (60) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
and(X1,active(X2)) | → | and(X1,X2) | (65) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (72) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
and(active(X1),X2) | → | and(X1,X2) | (64) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
and(mark(X1),X2) | → | and(X1,X2) | (62) |
take(active(X1),X2) | → | take(X1,X2) | (82) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (56) |
tail(active(X)) | → | tail(X) | (79) |
head(active(X)) | → | head(X) | (69) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
tail(mark(X)) | → | tail(X) | (78) |
take(X1,mark(X2)) | → | take(X1,X2) | (81) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
sel(active(X1),X2) | → | sel(X1,X2) | (76) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (57) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
fst(active(X)) | → | fst(X) | (67) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (59) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
snd(active(X)) | → | snd(X) | (61) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (58) |
sel(mark(X1),X2) | → | sel(X1,X2) | (74) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (75) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
s(active(X)) | → | s(X) | (73) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (66) |
take(X1,active(X2)) | → | take(X1,X2) | (83) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
mark#(snd(X)) | → | active#(snd(mark(X))) | (131) |
mark#(sel(X1,X2)) | → | active#(sel(mark(X1),mark(X2))) | (122) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
mark#(afterNth(X1,X2)) | → | active#(afterNth(mark(X1),mark(X2))) | (197) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (185) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (157) |
mark#(fst(X)) | → | active#(fst(mark(X))) | (95) |
mark#(head(X)) | → | active#(head(mark(X))) | (96) |
The dependency pairs are split into 1 component.
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (108) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (173) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (177) |
mark#(U11(X1,X2,X3,X4)) | → | active#(U11(mark(X1),X2,X3,X4)) | (147) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
[U11(x1,...,x4)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 26557 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 49055 |
[and(x1, x2)] | = | x2 + 40856 |
[pair(x1, x2)] | = | 0 |
[fst(x1)] | = | 73873 |
[natsFrom(x1)] | = | x1 + 16494 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 0 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 0 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 20683 |
[mark#(x1)] | = | x1 + 4 |
[0] | = | 0 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + x2 + 0 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 11842 |
[nil] | = | 50756 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 24818 |
[head(x1)] | = | 24818 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 0 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 4 |
[snd(x1)] | = | x1 + 36660 |
[tt] | = | 6168 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
head(mark(X)) | → | head(X) | (68) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
snd(mark(X)) | → | snd(X) | (60) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
head(active(X)) | → | head(X) | (69) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
fst(active(X)) | → | fst(X) | (67) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
snd(active(X)) | → | snd(X) | (61) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (66) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(natsFrom(X)) | → | active#(natsFrom(mark(X))) | (177) |
The dependency pairs are split into 1 component.
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (108) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (173) |
mark#(U11(X1,X2,X3,X4)) | → | active#(U11(mark(X1),X2,X3,X4)) | (147) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
[U11(x1,...,x4)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 2 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 1 |
[and(x1, x2)] | = | 2 |
[pair(x1, x2)] | = | 1 |
[fst(x1)] | = | 4 |
[natsFrom(x1)] | = | 2 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 1 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 4 |
[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)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | 4 |
[head(x1)] | = | 20261 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | 0 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | x1 + 3 |
[snd(x1)] | = | 25472 |
[tt] | = | 2 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
take(mark(X1),X2) | → | take(X1,X2) | (80) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
sel(X1,active(X2)) | → | sel(X1,X2) | (77) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
head(mark(X)) | → | head(X) | (68) |
and(X1,mark(X2)) | → | and(X1,X2) | (63) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
snd(mark(X)) | → | snd(X) | (60) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
and(X1,active(X2)) | → | and(X1,X2) | (65) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
s(mark(X)) | → | s(X) | (72) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
and(active(X1),X2) | → | and(X1,X2) | (64) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
and(mark(X1),X2) | → | and(X1,X2) | (62) |
take(active(X1),X2) | → | take(X1,X2) | (82) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (56) |
tail(active(X)) | → | tail(X) | (79) |
head(active(X)) | → | head(X) | (69) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
tail(mark(X)) | → | tail(X) | (78) |
take(X1,mark(X2)) | → | take(X1,X2) | (81) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
sel(active(X1),X2) | → | sel(X1,X2) | (76) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (57) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
fst(active(X)) | → | fst(X) | (67) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (59) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
snd(active(X)) | → | snd(X) | (61) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (58) |
sel(mark(X1),X2) | → | sel(X1,X2) | (74) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (75) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
s(active(X)) | → | s(X) | (73) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (66) |
take(X1,active(X2)) | → | take(X1,X2) | (83) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
active#(natsFrom(N)) | → | mark#(cons(N,natsFrom(s(N)))) | (173) |
The dependency pairs are split into 1 component.
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (108) |
mark#(splitAt(X1,X2)) | → | active#(splitAt(mark(X1),mark(X2))) | (94) |
mark#(U11(X1,X2,X3,X4)) | → | active#(U11(mark(X1),X2,X3,X4)) | (147) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
π(head#) | = | 1 |
π(fst#) | = | 1 |
π(mark#) | = | 1 |
π(mark) | = | 1 |
π(afterNth#) | = | 1 |
π(active) | = | 1 |
π(active#) | = | 1 |
prec(U11) | = | 6 | status(U11) | = | [2, 3] | list-extension(U11) | = | Lex | ||
prec(cons#) | = | 0 | status(cons#) | = | [] | list-extension(cons#) | = | Lex | ||
prec(s) | = | 0 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(take#) | = | 0 | status(take#) | = | [2] | list-extension(take#) | = | Lex | ||
prec(take) | = | 2 | status(take) | = | [] | list-extension(take) | = | Lex | ||
prec(and) | = | 4 | status(and) | = | [2, 1] | list-extension(and) | = | Lex | ||
prec(pair) | = | 1 | status(pair) | = | [2, 1] | list-extension(pair) | = | Lex | ||
prec(fst) | = | 4 | status(fst) | = | [] | list-extension(fst) | = | Lex | ||
prec(natsFrom) | = | 5 | status(natsFrom) | = | [] | list-extension(natsFrom) | = | Lex | ||
prec(splitAt) | = | 6 | status(splitAt) | = | [1] | list-extension(splitAt) | = | Lex | ||
prec(U12) | = | 2 | status(U12) | = | [1] | list-extension(U12) | = | Lex | ||
prec(U12#) | = | 0 | status(U12#) | = | [] | list-extension(U12#) | = | Lex | ||
prec(tail) | = | 4 | status(tail) | = | [] | list-extension(tail) | = | Lex | ||
prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(sel#) | = | 0 | status(sel#) | = | [1] | list-extension(sel#) | = | Lex | ||
prec(sel) | = | 4 | status(sel) | = | [1, 2] | list-extension(sel) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(afterNth) | = | 4 | status(afterNth) | = | [2, 1] | list-extension(afterNth) | = | Lex | ||
prec(nil) | = | 7 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(tail#) | = | 0 | status(tail#) | = | [] | list-extension(tail#) | = | Lex | ||
prec(splitAt#) | = | 0 | status(splitAt#) | = | [2, 1] | list-extension(splitAt#) | = | Lex | ||
prec(U11#) | = | 0 | status(U11#) | = | [1, 4, 2, 3] | list-extension(U11#) | = | Lex | ||
prec(head) | = | 3 | status(head) | = | [] | list-extension(head) | = | Lex | ||
prec(snd#) | = | 0 | status(snd#) | = | [] | list-extension(snd#) | = | Lex | ||
prec(cons) | = | 4 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(natsFrom#) | = | 0 | status(natsFrom#) | = | [] | list-extension(natsFrom#) | = | Lex | ||
prec(snd) | = | 2 | status(snd) | = | [] | list-extension(snd) | = | Lex | ||
prec(tt) | = | 8 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(pair#) | = | 0 | status(pair#) | = | [1, 2] | list-extension(pair#) | = | Lex | ||
prec(and#) | = | 0 | status(and#) | = | [1, 2] | list-extension(and#) | = | Lex |
[U11(x1,...,x4)] | = | max(x1 + 69708, x2 + 0, x3 + 69708, x4 + 69708, 0) |
[cons#(x1, x2)] | = | max(x1 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[take#(x1, x2)] | = | x2 + 1 |
[take(x1, x2)] | = | x1 + x2 + 95995 |
[and(x1, x2)] | = | x1 + x2 + 21656 |
[pair(x1, x2)] | = | max(x1 + 34854, x2 + 34853, 0) |
[fst(x1)] | = | x1 + 26286 |
[natsFrom(x1)] | = | x1 + 2998 |
[splitAt(x1, x2)] | = | max(x1 + 0, x2 + 69708, 0) |
[U12(x1, x2)] | = | max(x1 + 0, x2 + 34855, 0) |
[U12#(x1, x2)] | = | max(x2 + 1, 0) |
[tail(x1)] | = | x1 + 14681 |
[0] | = | 34852 |
[sel#(x1, x2)] | = | x1 + 1 |
[sel(x1, x2)] | = | x1 + x2 + 141036 |
[s#(x1)] | = | 1 |
[afterNth(x1, x2)] | = | x1 + x2 + 101601 |
[nil] | = | 34853 |
[tail#(x1)] | = | 1 |
[splitAt#(x1, x2)] | = | max(x1 + 1, x2 + 1, 0) |
[U11#(x1,...,x4)] | = | max(x1 + 1, x2 + 1, x3 + 1, x4 + 1, 0) |
[head(x1)] | = | x1 + 39434 |
[snd#(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[natsFrom#(x1)] | = | 1 |
[snd(x1)] | = | x1 + 31892 |
[tt] | = | 0 |
[pair#(x1, x2)] | = | max(x1 + 1, x2 + 1, 0) |
[and#(x1, x2)] | = | x1 + x2 + 1 |
mark(pair(X1,X2)) | → | active(pair(mark(X1),mark(X2))) | (18) |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
take(mark(X1),X2) | → | take(X1,X2) | (80) |
active(and(tt,X)) | → | mark(X) | (4) |
mark(tt) | → | active(tt) | (15) |
active(sel(N,XS)) | → | mark(head(afterNth(N,XS))) | (8) |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
active(U11(tt,N,X,XS)) | → | mark(U12(splitAt(N,XS),X)) | (1) |
sel(X1,active(X2)) | → | sel(X1,X2) | (77) |
active(afterNth(N,XS)) | → | mark(snd(splitAt(N,XS))) | (3) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (16) |
mark(snd(X)) | → | active(snd(mark(X))) | (21) |
U11(active(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (36) |
head(mark(X)) | → | head(X) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
and(X1,mark(X2)) | → | and(X1,X2) | (63) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (19) |
U11(mark(X1),X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
mark(splitAt(X1,X2)) | → | active(splitAt(mark(X1),mark(X2))) | (17) |
snd(mark(X)) | → | snd(X) | (60) |
mark(sel(X1,X2)) | → | active(sel(mark(X1),mark(X2))) | (27) |
U11(X1,X2,mark(X3),X4) | → | U11(X1,X2,X3,X4) | (34) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(0) | → | active(0) | (28) |
and(X1,active(X2)) | → | and(X1,X2) | (65) |
splitAt(mark(X1),X2) | → | splitAt(X1,X2) | (44) |
active(fst(pair(X,Y))) | → | mark(X) | (5) |
s(mark(X)) | → | s(X) | (72) |
U11(X1,mark(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (33) |
and(active(X1),X2) | → | and(X1,X2) | (64) |
active(splitAt(0,XS)) | → | mark(pair(nil,XS)) | (10) |
U11(X1,X2,X3,active(X4)) | → | U11(X1,X2,X3,X4) | (39) |
active(natsFrom(N)) | → | mark(cons(N,natsFrom(s(N)))) | (7) |
mark(afterNth(X1,X2)) | → | active(afterNth(mark(X1),mark(X2))) | (20) |
mark(natsFrom(X)) | → | active(natsFrom(mark(X))) | (25) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
mark(tail(X)) | → | active(tail(mark(X))) | (30) |
and(mark(X1),X2) | → | and(X1,X2) | (62) |
mark(U11(X1,X2,X3,X4)) | → | active(U11(mark(X1),X2,X3,X4)) | (14) |
take(active(X1),X2) | → | take(X1,X2) | (82) |
afterNth(mark(X1),X2) | → | afterNth(X1,X2) | (56) |
tail(active(X)) | → | tail(X) | (79) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (31) |
active(tail(cons(N,XS))) | → | mark(XS) | (12) |
head(active(X)) | → | head(X) | (69) |
splitAt(X1,mark(X2)) | → | splitAt(X1,X2) | (45) |
tail(mark(X)) | → | tail(X) | (78) |
take(X1,mark(X2)) | → | take(X1,X2) | (81) |
mark(fst(X)) | → | active(fst(mark(X))) | (23) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
mark(head(X)) | → | active(head(mark(X))) | (24) |
sel(active(X1),X2) | → | sel(X1,X2) | (76) |
afterNth(X1,mark(X2)) | → | afterNth(X1,X2) | (57) |
active(splitAt(s(N),cons(X,XS))) | → | mark(U11(tt,N,X,XS)) | (11) |
active(snd(pair(X,Y))) | → | mark(Y) | (9) |
active(take(N,XS)) | → | mark(fst(splitAt(N,XS))) | (13) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
U12(mark(X1),X2) | → | U12(X1,X2) | (40) |
fst(active(X)) | → | fst(X) | (67) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
afterNth(X1,active(X2)) | → | afterNth(X1,X2) | (59) |
active(head(cons(N,XS))) | → | mark(N) | (6) |
U11(X1,X2,active(X3),X4) | → | U11(X1,X2,X3,X4) | (38) |
snd(active(X)) | → | snd(X) | (61) |
afterNth(active(X1),X2) | → | afterNth(X1,X2) | (58) |
sel(mark(X1),X2) | → | sel(X1,X2) | (74) |
sel(X1,mark(X2)) | → | sel(X1,X2) | (75) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
splitAt(X1,active(X2)) | → | splitAt(X1,X2) | (47) |
s(active(X)) | → | s(X) | (73) |
U11(X1,active(X2),X3,X4) | → | U11(X1,X2,X3,X4) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (41) |
U12(active(X1),X2) | → | U12(X1,X2) | (42) |
splitAt(active(X1),X2) | → | splitAt(X1,X2) | (46) |
fst(mark(X)) | → | fst(X) | (66) |
take(X1,active(X2)) | → | take(X1,X2) | (83) |
U11(X1,X2,X3,mark(X4)) | → | U11(X1,X2,X3,X4) | (35) |
mark(nil) | → | active(nil) | (29) |
U12(X1,active(X2)) | → | U12(X1,X2) | (43) |
active(U12(pair(YS,ZS),X)) | → | mark(pair(cons(X,YS),ZS)) | (2) |
active#(U11(tt,N,X,XS)) | → | mark#(U12(splitAt(N,XS),X)) | (169) |
mark#(U12(X1,X2)) | → | mark#(X1) | (97) |
active#(splitAt(s(N),cons(X,XS))) | → | mark#(U11(tt,N,X,XS)) | (172) |
active#(U12(pair(YS,ZS),X)) | → | mark#(pair(cons(X,YS),ZS)) | (204) |
The dependency pairs are split into 0 components.
take#(mark(X1),X2) | → | take#(X1,X2) | (136) |
take#(active(X1),X2) | → | take#(X1,X2) | (119) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (176) |
take#(X1,active(X2)) | → | take#(X1,X2) | (165) |
[U11(x1,...,x4)] | = | x1 + x3 + x4 + 9999 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 21331 |
[take#(x1, x2)] | = | x1 + x2 + 0 |
[take(x1, x2)] | = | x1 + x2 + 52739 |
[and(x1, x2)] | = | 35083 |
[pair(x1, x2)] | = | 23726 |
[fst(x1)] | = | x1 + 29021 |
[natsFrom(x1)] | = | 8136 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 23720 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 23724 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 21220 |
[mark#(x1)] | = | 3 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 62118 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 38885 |
[nil] | = | 7193 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 23235 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 8138 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 15167 |
[tt] | = | 13723 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
take#(mark(X1),X2) | → | take#(X1,X2) | (136) |
take#(active(X1),X2) | → | take#(X1,X2) | (119) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (176) |
take#(X1,active(X2)) | → | take#(X1,X2) | (165) |
The dependency pairs are split into 0 components.
fst#(mark(X)) | → | fst#(X) | (207) |
fst#(active(X)) | → | fst#(X) | (193) |
[U11(x1,...,x4)] | = | x1 + x3 + x4 + 1327 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 28587 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 36987 |
[and(x1, x2)] | = | 22267 |
[pair(x1, x2)] | = | 23726 |
[fst(x1)] | = | x1 + 31437 |
[natsFrom(x1)] | = | 31852 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 5552 |
[fst#(x1)] | = | x1 + 0 |
[U12(x1, x2)] | = | 5556 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 40582 |
[mark#(x1)] | = | 3 |
[0] | = | 33242 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 50410 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 49097 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 1315 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 31854 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 43547 |
[tt] | = | 4227 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
fst#(mark(X)) | → | fst#(X) | (207) |
fst#(active(X)) | → | fst#(X) | (193) |
The dependency pairs are split into 0 components.
tail#(mark(X)) | → | tail#(X) | (140) |
tail#(active(X)) | → | tail#(X) | (103) |
[U11(x1,...,x4)] | = | x1 + x3 + x4 + 592 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 23743 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 37950 |
[and(x1, x2)] | = | 42802 |
[pair(x1, x2)] | = | 3961 |
[fst(x1)] | = | x1 + 33997 |
[natsFrom(x1)] | = | 23296 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 3955 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 3959 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 24542 |
[mark#(x1)] | = | 3 |
[0] | = | 19049 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 9481 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 4000 |
[nil] | = | 1 |
[tail#(x1)] | = | x1 + 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 5483 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 23298 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 47 |
[tt] | = | 3365 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
tail#(mark(X)) | → | tail#(X) | (140) |
tail#(active(X)) | → | tail#(X) | (103) |
The dependency pairs are split into 0 components.
U11#(active(X1),X2,X3,X4) | → | U11#(X1,X2,X3,X4) | (160) |
U11#(X1,mark(X2),X3,X4) | → | U11#(X1,X2,X3,X4) | (214) |
U11#(X1,X2,mark(X3),X4) | → | U11#(X1,X2,X3,X4) | (148) |
U11#(X1,active(X2),X3,X4) | → | U11#(X1,X2,X3,X4) | (144) |
U11#(X1,X2,X3,active(X4)) | → | U11#(X1,X2,X3,X4) | (130) |
U11#(X1,X2,X3,mark(X4)) | → | U11#(X1,X2,X3,X4) | (115) |
U11#(X1,X2,active(X3),X4) | → | U11#(X1,X2,X3,X4) | (179) |
U11#(mark(X1),X2,X3,X4) | → | U11#(X1,X2,X3,X4) | (98) |
[U11(x1,...,x4)] | = | x1 + x3 + x4 + 2 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 1 |
[and(x1, x2)] | = | 39784 |
[pair(x1, x2)] | = | 8 |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 2 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 6 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 3 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 16422 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 13963 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 3752 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 16422 |
[tt] | = | 2 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
U11#(active(X1),X2,X3,X4) | → | U11#(X1,X2,X3,X4) | (160) |
U11#(X1,mark(X2),X3,X4) | → | U11#(X1,X2,X3,X4) | (214) |
U11#(X1,X2,mark(X3),X4) | → | U11#(X1,X2,X3,X4) | (148) |
U11#(X1,active(X2),X3,X4) | → | U11#(X1,X2,X3,X4) | (144) |
U11#(X1,X2,X3,active(X4)) | → | U11#(X1,X2,X3,X4) | (130) |
U11#(X1,X2,X3,mark(X4)) | → | U11#(X1,X2,X3,X4) | (115) |
U11#(X1,X2,active(X3),X4) | → | U11#(X1,X2,X3,X4) | (179) |
U11#(mark(X1),X2,X3,X4) | → | U11#(X1,X2,X3,X4) | (98) |
The dependency pairs are split into 0 components.
and#(X1,mark(X2)) | → | and#(X1,X2) | (211) |
and#(active(X1),X2) | → | and#(X1,X2) | (146) |
and#(mark(X1),X2) | → | and#(X1,X2) | (116) |
and#(X1,active(X2)) | → | and#(X1,X2) | (182) |
[U11(x1,...,x4)] | = | x1 + x3 + x4 + 3 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 1 |
[and(x1, x2)] | = | 1 |
[pair(x1, x2)] | = | 8 |
[fst(x1)] | = | x1 + 8785 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 2 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 6 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 3 |
[0] | = | 35361 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 1 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 30300 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 23709 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 1 |
[tt] | = | 1 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | x1 + x2 + 0 |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
and#(X1,mark(X2)) | → | and#(X1,X2) | (211) |
and#(active(X1),X2) | → | and#(X1,X2) | (146) |
and#(mark(X1),X2) | → | and#(X1,X2) | (116) |
and#(X1,active(X2)) | → | and#(X1,X2) | (182) |
The dependency pairs are split into 0 components.
natsFrom#(active(X)) | → | natsFrom#(X) | (201) |
natsFrom#(mark(X)) | → | natsFrom#(X) | (121) |
[U11(x1,...,x4)] | = | x1 + x3 + x4 + 1327 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 53157 |
[and(x1, x2)] | = | 1 |
[pair(x1, x2)] | = | 23038 |
[fst(x1)] | = | x1 + 30127 |
[natsFrom(x1)] | = | 21965 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 23032 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | 23036 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 3 |
[0] | = | 33775 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 53817 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + x2 + 44521 |
[nil] | = | 25971 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 9298 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 21967 |
[natsFrom#(x1)] | = | x1 + 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 21491 |
[tt] | = | 21707 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
s(mark(X)) | → | s(X) | (72) |
s(active(X)) | → | s(X) | (73) |
natsFrom#(active(X)) | → | natsFrom#(X) | (201) |
natsFrom#(mark(X)) | → | natsFrom#(X) | (121) |
The dependency pairs are split into 0 components.
sel#(X1,mark(X2)) | → | sel#(X1,X2) | (216) |
sel#(X1,active(X2)) | → | sel#(X1,X2) | (138) |
sel#(active(X1),X2) | → | sel#(X1,X2) | (199) |
sel#(mark(X1),X2) | → | sel#(X1,X2) | (189) |
[U11(x1,...,x4)] | = | x1 + 65024 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 31408 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 24649 |
[and(x1, x2)] | = | x1 + x2 + 7847 |
[pair(x1, x2)] | = | x1 + x2 + 296 |
[fst(x1)] | = | 24651 |
[natsFrom(x1)] | = | x1 + 26610 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | x1 + x2 + 692 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 69706 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | 43866 |
[mark#(x1)] | = | 3 |
[0] | = | 1 |
[sel#(x1, x2)] | = | x2 + 0 |
[sel(x1, x2)] | = | 46833 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | x1 + 26696 |
[nil] | = | 399 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | x1 + 20139 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 38294 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 26006 |
[tt] | = | 5372 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (54) |
s(mark(X)) | → | s(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (52) |
natsFrom(mark(X)) | → | natsFrom(X) | (70) |
cons(X1,active(X2)) | → | cons(X1,X2) | (55) |
natsFrom(active(X)) | → | natsFrom(X) | (71) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (53) |
s(active(X)) | → | s(X) | (73) |
sel#(X1,mark(X2)) | → | sel#(X1,X2) | (216) |
sel#(X1,active(X2)) | → | sel#(X1,X2) | (138) |
The dependency pairs are split into 1 component.
sel#(active(X1),X2) | → | sel#(X1,X2) | (199) |
sel#(mark(X1),X2) | → | sel#(X1,X2) | (189) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 1995 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 27727 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 23485 |
[and(x1, x2)] | = | 45942 |
[pair(x1, x2)] | = | x2 + 4715 |
[fst(x1)] | = | x1 + 18778 |
[natsFrom(x1)] | = | 40346 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 4709 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 4713 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 38367 |
[mark#(x1)] | = | 3 |
[0] | = | 1836 |
[sel#(x1, x2)] | = | x1 + 0 |
[sel(x1, x2)] | = | x1 + 55375 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 32962 |
[nil] | = | 52245 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 55377 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 10596 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 28255 |
[tt] | = | 2716 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
sel#(active(X1),X2) | → | sel#(X1,X2) | (199) |
sel#(mark(X1),X2) | → | sel#(X1,X2) | (189) |
The dependency pairs are split into 0 components.
cons#(X1,active(X2)) | → | cons#(X1,X2) | (158) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (209) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (196) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (191) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 1 |
[cons#(x1, x2)] | = | x1 + x2 + 0 |
[s(x1)] | = | 15114 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 1 |
[and(x1, x2)] | = | 1 |
[pair(x1, x2)] | = | x2 + 7 |
[fst(x1)] | = | x1 + 4634 |
[natsFrom(x1)] | = | 36200 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 5 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 1 |
[mark#(x1)] | = | 3 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 30322 |
[nil] | = | 37535 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 3 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 2 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 30323 |
[tt] | = | 2 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (158) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (209) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (196) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (191) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (137) |
s#(active(X)) | → | s#(X) | (125) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 122 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 30389 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 30746 |
[and(x1, x2)] | = | 23357 |
[pair(x1, x2)] | = | x2 + 10028 |
[fst(x1)] | = | x1 + 20726 |
[natsFrom(x1)] | = | 31754 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 10022 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 10026 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 38435 |
[mark#(x1)] | = | 3 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 42827 |
[s#(x1)] | = | x1 + 0 |
[afterNth(x1, x2)] | = | 18015 |
[nil] | = | 51347 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 42829 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 27298 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 7995 |
[tt] | = | 9902 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
s#(mark(X)) | → | s#(X) | (137) |
s#(active(X)) | → | s#(X) | (125) |
The dependency pairs are split into 0 components.
splitAt#(X1,active(X2)) | → | splitAt#(X1,X2) | (152) |
splitAt#(active(X1),X2) | → | splitAt#(X1,X2) | (126) |
splitAt#(X1,mark(X2)) | → | splitAt#(X1,X2) | (91) |
splitAt#(mark(X1),X2) | → | splitAt#(X1,X2) | (89) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 3 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 27114 |
[and(x1, x2)] | = | 32810 |
[pair(x1, x2)] | = | x2 + 8 |
[fst(x1)] | = | x1 + 27114 |
[natsFrom(x1)] | = | 32615 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 2 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 6 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 1 |
[mark#(x1)] | = | 3 |
[0] | = | 1 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 51347 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | x1 + x2 + 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 3 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 22135 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 12699 |
[tt] | = | 1 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
splitAt#(X1,active(X2)) | → | splitAt#(X1,X2) | (152) |
splitAt#(active(X1),X2) | → | splitAt#(X1,X2) | (126) |
splitAt#(X1,mark(X2)) | → | splitAt#(X1,X2) | (91) |
splitAt#(mark(X1),X2) | → | splitAt#(X1,X2) | (89) |
The dependency pairs are split into 0 components.
snd#(mark(X)) | → | snd#(X) | (132) |
snd#(active(X)) | → | snd#(X) | (200) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 458 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 28631 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 14114 |
[and(x1, x2)] | = | 61300 |
[pair(x1, x2)] | = | x2 + 464 |
[fst(x1)] | = | x1 + 13658 |
[natsFrom(x1)] | = | 26378 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 458 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 462 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 51797 |
[mark#(x1)] | = | 3 |
[0] | = | 13507 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 39676 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 12473 |
[nil] | = | 20153 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 39678 |
[snd#(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + x2 + 12146 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 12017 |
[tt] | = | 2 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
snd#(mark(X)) | → | snd#(X) | (132) |
snd#(active(X)) | → | snd#(X) | (200) |
The dependency pairs are split into 0 components.
head#(mark(X)) | → | head#(X) | (123) |
head#(active(X)) | → | head#(X) | (102) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 2 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 13314 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 35607 |
[and(x1, x2)] | = | 36329 |
[pair(x1, x2)] | = | x2 + 7 |
[fst(x1)] | = | x1 + 35608 |
[natsFrom(x1)] | = | 26058 |
[head#(x1)] | = | x1 + 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 5 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 43359 |
[mark#(x1)] | = | 3 |
[0] | = | 11654 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 52904 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 38641 |
[nil] | = | 27829 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 52906 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 27366 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 38642 |
[tt] | = | 1 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
head#(mark(X)) | → | head#(X) | (123) |
head#(active(X)) | → | head#(X) | (102) |
The dependency pairs are split into 0 components.
U12#(X1,active(X2)) | → | U12#(X1,X2) | (212) |
U12#(X1,mark(X2)) | → | U12#(X1,X2) | (127) |
U12#(mark(X1),X2) | → | U12#(X1,X2) | (184) |
U12#(active(X1),X2) | → | U12#(X1,X2) | (167) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 30427 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 20719 |
[and(x1, x2)] | = | 1 |
[pair(x1, x2)] | = | x2 + 32027 |
[fst(x1)] | = | x1 + 20720 |
[natsFrom(x1)] | = | 20992 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 32025 |
[U12#(x1, x2)] | = | x1 + x2 + 0 |
[tail(x1)] | = | x1 + 20966 |
[mark#(x1)] | = | 3 |
[0] | = | 11654 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 49250 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 28072 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 49252 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 32224 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 28073 |
[tt] | = | 1596 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
U12#(X1,active(X2)) | → | U12#(X1,X2) | (212) |
U12#(X1,mark(X2)) | → | U12#(X1,X2) | (127) |
U12#(mark(X1),X2) | → | U12#(X1,X2) | (184) |
U12#(active(X1),X2) | → | U12#(X1,X2) | (167) |
The dependency pairs are split into 0 components.
pair#(active(X1),X2) | → | pair#(X1,X2) | (161) |
pair#(mark(X1),X2) | → | pair#(X1,X2) | (187) |
pair#(X1,active(X2)) | → | pair#(X1,X2) | (178) |
pair#(X1,mark(X2)) | → | pair#(X1,X2) | (171) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 1 |
[and(x1, x2)] | = | 1 |
[pair(x1, x2)] | = | x2 + 7 |
[fst(x1)] | = | x1 + 2 |
[natsFrom(x1)] | = | 40158 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 5 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 4115 |
[mark#(x1)] | = | 3 |
[0] | = | 11654 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 1 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 3 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 28110 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 2 |
[tt] | = | 2 |
[pair#(x1, x2)] | = | x1 + x2 + 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
pair#(active(X1),X2) | → | pair#(X1,X2) | (161) |
pair#(mark(X1),X2) | → | pair#(X1,X2) | (187) |
pair#(X1,active(X2)) | → | pair#(X1,X2) | (178) |
pair#(X1,mark(X2)) | → | pair#(X1,X2) | (171) |
The dependency pairs are split into 0 components.
afterNth#(mark(X1),X2) | → | afterNth#(X1,X2) | (206) |
afterNth#(X1,active(X2)) | → | afterNth#(X1,X2) | (133) |
afterNth#(X1,mark(X2)) | → | afterNth#(X1,X2) | (88) |
afterNth#(active(X1),X2) | → | afterNth#(X1,X2) | (162) |
[U11(x1,...,x4)] | = | x1 + x2 + x4 + 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 9542 |
[take#(x1, x2)] | = | 0 |
[take(x1, x2)] | = | 1 |
[and(x1, x2)] | = | 24764 |
[pair(x1, x2)] | = | x2 + 7 |
[fst(x1)] | = | x1 + 15687 |
[natsFrom(x1)] | = | 30500 |
[head#(x1)] | = | 0 |
[splitAt(x1, x2)] | = | 1 |
[fst#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 5 |
[U12#(x1, x2)] | = | 0 |
[tail(x1)] | = | x1 + 1 |
[mark#(x1)] | = | 3 |
[0] | = | 11654 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 1 |
[nil] | = | 43654 |
[tail#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[afterNth#(x1, x2)] | = | x1 + x2 + 0 |
[U11#(x1,...,x4)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[head(x1)] | = | 3 |
[snd#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 2 |
[natsFrom#(x1)] | = | 0 |
[active#(x1)] | = | 3 |
[snd(x1)] | = | x1 + 2 |
[tt] | = | 2 |
[pair#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
pair(active(X1),X2) | → | pair(X1,X2) | (50) |
s(mark(X)) | → | s(X) | (72) |
pair(X1,mark(X2)) | → | pair(X1,X2) | (49) |
pair(X1,active(X2)) | → | pair(X1,X2) | (51) |
pair(mark(X1),X2) | → | pair(X1,X2) | (48) |
s(active(X)) | → | s(X) | (73) |
afterNth#(mark(X1),X2) | → | afterNth#(X1,X2) | (206) |
afterNth#(X1,active(X2)) | → | afterNth#(X1,X2) | (133) |
afterNth#(X1,mark(X2)) | → | afterNth#(X1,X2) | (88) |
afterNth#(active(X1),X2) | → | afterNth#(X1,X2) | (162) |
The dependency pairs are split into 0 components.