The rewrite relation of the following TRS is considered.
a__U11(tt,N,X,XS) | → | a__U12(a__splitAt(mark(N),mark(XS)),X) | (1) |
a__U12(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (2) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (3) |
a__and(tt,X) | → | mark(X) | (4) |
a__fst(pair(X,Y)) | → | mark(X) | (5) |
a__head(cons(N,XS)) | → | mark(N) | (6) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (7) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
a__snd(pair(X,Y)) | → | mark(Y) | (9) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (10) |
a__splitAt(s(N),cons(X,XS)) | → | a__U11(tt,N,X,XS) | (11) |
a__tail(cons(N,XS)) | → | mark(XS) | (12) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (13) |
mark(U11(X1,X2,X3,X4)) | → | a__U11(mark(X1),X2,X3,X4) | (14) |
mark(U12(X1,X2)) | → | a__U12(mark(X1),X2) | (15) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (16) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (17) |
mark(snd(X)) | → | a__snd(mark(X)) | (18) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (19) |
mark(fst(X)) | → | a__fst(mark(X)) | (20) |
mark(head(X)) | → | a__head(mark(X)) | (21) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (22) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (23) |
mark(tail(X)) | → | a__tail(mark(X)) | (24) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (25) |
mark(tt) | → | tt | (26) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (27) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (28) |
mark(s(X)) | → | s(mark(X)) | (29) |
mark(0) | → | 0 | (30) |
mark(nil) | → | nil | (31) |
a__U11(X1,X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
a__U12(X1,X2) | → | U12(X1,X2) | (33) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (34) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
a__snd(X) | → | snd(X) | (36) |
a__and(X1,X2) | → | and(X1,X2) | (37) |
a__fst(X) | → | fst(X) | (38) |
a__head(X) | → | head(X) | (39) |
a__natsFrom(X) | → | natsFrom(X) | (40) |
a__sel(X1,X2) | → | sel(X1,X2) | (41) |
a__tail(X) | → | tail(X) | (42) |
a__take(X1,X2) | → | take(X1,X2) | (43) |
a__U12#(pair(YS,ZS),X) | → | mark#(ZS) | (44) |
a__afterNth#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (45) |
mark#(natsFrom(X)) | → | mark#(X) | (46) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (47) |
a__U11#(tt,N,X,XS) | → | a__U12#(a__splitAt(mark(N),mark(XS)),X) | (48) |
a__afterNth#(N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (49) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (50) |
mark#(head(X)) | → | a__head#(mark(X)) | (51) |
a__U11#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (52) |
a__sel#(N,XS) | → | mark#(XS) | (53) |
a__U11#(tt,N,X,XS) | → | mark#(N) | (54) |
mark#(snd(X)) | → | mark#(X) | (55) |
mark#(head(X)) | → | mark#(X) | (56) |
a__take#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (57) |
mark#(U12(X1,X2)) | → | mark#(X1) | (58) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (59) |
a__sel#(N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (60) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (61) |
a__snd#(pair(X,Y)) | → | mark#(Y) | (62) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (63) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (64) |
a__natsFrom#(N) | → | mark#(N) | (65) |
mark#(fst(X)) | → | mark#(X) | (66) |
a__afterNth#(N,XS) | → | mark#(XS) | (67) |
mark#(tail(X)) | → | mark#(X) | (68) |
mark#(pair(X1,X2)) | → | mark#(X2) | (69) |
a__and#(tt,X) | → | mark#(X) | (70) |
mark#(sel(X1,X2)) | → | mark#(X1) | (71) |
mark#(pair(X1,X2)) | → | mark#(X1) | (72) |
a__sel#(N,XS) | → | mark#(N) | (73) |
a__U11#(tt,N,X,XS) | → | mark#(XS) | (74) |
a__splitAt#(0,XS) | → | mark#(XS) | (75) |
mark#(take(X1,X2)) | → | mark#(X1) | (76) |
a__take#(N,XS) | → | mark#(N) | (77) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (78) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U11#(tt,N,X,XS) | (79) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (80) |
a__take#(N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (81) |
a__afterNth#(N,XS) | → | mark#(N) | (82) |
mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | (83) |
mark#(fst(X)) | → | a__fst#(mark(X)) | (84) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (85) |
mark#(cons(X1,X2)) | → | mark#(X1) | (86) |
mark#(U11(X1,X2,X3,X4)) | → | a__U11#(mark(X1),X2,X3,X4) | (87) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (88) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (89) |
a__fst#(pair(X,Y)) | → | mark#(X) | (90) |
mark#(and(X1,X2)) | → | mark#(X1) | (91) |
mark#(take(X1,X2)) | → | mark#(X2) | (92) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (93) |
mark#(s(X)) | → | mark#(X) | (94) |
a__U12#(pair(YS,ZS),X) | → | mark#(X) | (95) |
mark#(U12(X1,X2)) | → | a__U12#(mark(X1),X2) | (96) |
a__take#(N,XS) | → | mark#(XS) | (97) |
mark#(sel(X1,X2)) | → | mark#(X2) | (98) |
a__head#(cons(N,XS)) | → | mark#(N) | (99) |
a__sel#(N,XS) | → | a__head#(a__afterNth(mark(N),mark(XS))) | (100) |
mark#(U11(X1,X2,X3,X4)) | → | mark#(X1) | (101) |
The dependency pairs are split into 1 component.
mark#(U11(X1,X2,X3,X4)) | → | mark#(X1) | (101) |
a__sel#(N,XS) | → | a__head#(a__afterNth(mark(N),mark(XS))) | (100) |
a__splitAt#(0,XS) | → | mark#(XS) | (75) |
a__sel#(N,XS) | → | mark#(N) | (73) |
a__U11#(tt,N,X,XS) | → | mark#(XS) | (74) |
a__head#(cons(N,XS)) | → | mark#(N) | (99) |
mark#(pair(X1,X2)) | → | mark#(X1) | (72) |
mark#(sel(X1,X2)) | → | mark#(X1) | (71) |
mark#(sel(X1,X2)) | → | mark#(X2) | (98) |
a__and#(tt,X) | → | mark#(X) | (70) |
mark#(pair(X1,X2)) | → | mark#(X2) | (69) |
mark#(tail(X)) | → | mark#(X) | (68) |
a__take#(N,XS) | → | mark#(XS) | (97) |
a__afterNth#(N,XS) | → | mark#(XS) | (67) |
mark#(U12(X1,X2)) | → | a__U12#(mark(X1),X2) | (96) |
a__U12#(pair(YS,ZS),X) | → | mark#(X) | (95) |
mark#(fst(X)) | → | mark#(X) | (66) |
mark#(s(X)) | → | mark#(X) | (94) |
a__natsFrom#(N) | → | mark#(N) | (65) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (93) |
mark#(take(X1,X2)) | → | mark#(X2) | (92) |
mark#(and(X1,X2)) | → | mark#(X1) | (91) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (64) |
a__fst#(pair(X,Y)) | → | mark#(X) | (90) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (63) |
a__snd#(pair(X,Y)) | → | mark#(Y) | (62) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (61) |
a__sel#(N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (60) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (88) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (89) |
mark#(U11(X1,X2,X3,X4)) | → | a__U11#(mark(X1),X2,X3,X4) | (87) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (59) |
mark#(U12(X1,X2)) | → | mark#(X1) | (58) |
a__take#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (57) |
mark#(cons(X1,X2)) | → | mark#(X1) | (86) |
mark#(head(X)) | → | mark#(X) | (56) |
mark#(snd(X)) | → | mark#(X) | (55) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (85) |
a__U11#(tt,N,X,XS) | → | mark#(N) | (54) |
mark#(fst(X)) | → | a__fst#(mark(X)) | (84) |
a__sel#(N,XS) | → | mark#(XS) | (53) |
mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | (83) |
a__U11#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (52) |
a__afterNth#(N,XS) | → | mark#(N) | (82) |
a__take#(N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (81) |
mark#(head(X)) | → | a__head#(mark(X)) | (51) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (80) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (50) |
a__afterNth#(N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (49) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U11#(tt,N,X,XS) | (79) |
a__U11#(tt,N,X,XS) | → | a__U12#(a__splitAt(mark(N),mark(XS)),X) | (48) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (78) |
a__take#(N,XS) | → | mark#(N) | (77) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (47) |
mark#(natsFrom(X)) | → | mark#(X) | (46) |
a__afterNth#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (45) |
a__U12#(pair(YS,ZS),X) | → | mark#(ZS) | (44) |
mark#(take(X1,X2)) | → | mark#(X1) | (76) |
[U11(x1,...,x4)] | = | max(x1 + 37657, x2 + 37656, x3 + 37656, x4 + 37656, 0) |
[s(x1)] | = | x1 + 0 |
[a__head#(x1)] | = | x1 + 58481 |
[a__natsFrom#(x1)] | = | x1 + 87762 |
[a__snd#(x1)] | = | x1 + 37895 |
[a__afterNth(x1, x2)] | = | max(x1 + 37657, x2 + 37659, 0) |
[take(x1, x2)] | = | max(x1 + 37658, x2 + 37657, 0) |
[and(x1, x2)] | = | max(x1 + 7631, x2 + 7630, 0) |
[pair(x1, x2)] | = | max(x1 + 20588, x2 + 20588, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 29280 |
[a__snd(x1)] | = | x1 + 1 |
[splitAt(x1, x2)] | = | max(x1 + 37656, x2 + 37656, 0) |
[a__U11#(x1,...,x4)] | = | max(x1 + 79071, x2 + 96136, x3 + 96135, x4 + 96137, 0) |
[a__take#(x1, x2)] | = | max(x1 + 96138, x2 + 96138, 0) |
[U12(x1, x2)] | = | max(x1 + 0, x2 + 37656, 0) |
[a__U12#(x1, x2)] | = | max(x1 + 37894, x2 + 96135, 0) |
[a__fst(x1)] | = | x1 + 1 |
[a__natsFrom(x1)] | = | x1 + 29280 |
[tail(x1)] | = | x1 + 0 |
[mark#(x1)] | = | x1 + 58482 |
[0] | = | 60516 |
[a__and#(x1, x2)] | = | max(x1 + 41416, x2 + 58482, 0) |
[sel(x1, x2)] | = | max(x1 + 37658, x2 + 37659, 0) |
[afterNth(x1, x2)] | = | max(x1 + 37657, x2 + 37659, 0) |
[nil] | = | 12280 |
[a__splitAt(x1, x2)] | = | max(x1 + 37656, x2 + 37656, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 96139, x2 + 96141, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U11(x1,...,x4)] | = | max(x1 + 37657, x2 + 37656, x3 + 37656, x4 + 37656, 0) |
[a__sel(x1, x2)] | = | max(x1 + 37658, x2 + 37659, 0) |
[a__U12(x1, x2)] | = | max(x1 + 0, x2 + 37656, 0) |
[head(x1)] | = | x1 + 0 |
[a__afterNth#(x1, x2)] | = | max(x1 + 96138, x2 + 96140, 0) |
[a__splitAt#(x1, x2)] | = | max(x1 + 96136, x2 + 96137, 0) |
[cons(x1, x2)] | = | max(x1 + 17068, x2 + 0, 0) |
[snd(x1)] | = | x1 + 1 |
[a__take(x1, x2)] | = | max(x1 + 37658, x2 + 37657, 0) |
[tt] | = | 17067 |
[a__fst#(x1)] | = | x1 + 37895 |
[a__and(x1, x2)] | = | max(x1 + 7631, x2 + 7630, 0) |
[a__tail(x1)] | = | x1 + 0 |
[a__tail#(x1)] | = | x1 + 58482 |
[a__head(x1)] | = | x1 + 0 |
mark(snd(X)) | → | a__snd(mark(X)) | (18) |
a__and(tt,X) | → | mark(X) | (4) |
mark(U12(X1,X2)) | → | a__U12(mark(X1),X2) | (15) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
a__U11(tt,N,X,XS) | → | a__U12(a__splitAt(mark(N),mark(XS)),X) | (1) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (3) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (16) |
mark(head(X)) | → | a__head(mark(X)) | (21) |
a__snd(X) | → | snd(X) | (36) |
mark(tt) | → | tt | (26) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (19) |
a__U11(X1,X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (17) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (27) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (34) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (22) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (28) |
a__fst(pair(X,Y)) | → | mark(X) | (5) |
a__U12(X1,X2) | → | U12(X1,X2) | (33) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (10) |
a__head(X) | → | head(X) | (39) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (7) |
mark(fst(X)) | → | a__fst(mark(X)) | (20) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (25) |
mark(0) | → | 0 | (30) |
mark(U11(X1,X2,X3,X4)) | → | a__U11(mark(X1),X2,X3,X4) | (14) |
mark(nil) | → | nil | (31) |
a__tail(cons(N,XS)) | → | mark(XS) | (12) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (23) |
mark(tail(X)) | → | a__tail(mark(X)) | (24) |
a__splitAt(s(N),cons(X,XS)) | → | a__U11(tt,N,X,XS) | (11) |
a__snd(pair(X,Y)) | → | mark(Y) | (9) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (13) |
a__natsFrom(X) | → | natsFrom(X) | (40) |
a__head(cons(N,XS)) | → | mark(N) | (6) |
a__fst(X) | → | fst(X) | (38) |
a__and(X1,X2) | → | and(X1,X2) | (37) |
a__sel(X1,X2) | → | sel(X1,X2) | (41) |
a__tail(X) | → | tail(X) | (42) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
mark(s(X)) | → | s(mark(X)) | (29) |
a__take(X1,X2) | → | take(X1,X2) | (43) |
a__U12(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (2) |
mark#(U11(X1,X2,X3,X4)) | → | mark#(X1) | (101) |
a__sel#(N,XS) | → | a__head#(a__afterNth(mark(N),mark(XS))) | (100) |
a__splitAt#(0,XS) | → | mark#(XS) | (75) |
a__sel#(N,XS) | → | mark#(N) | (73) |
a__U11#(tt,N,X,XS) | → | mark#(XS) | (74) |
a__head#(cons(N,XS)) | → | mark#(N) | (99) |
mark#(pair(X1,X2)) | → | mark#(X1) | (72) |
mark#(sel(X1,X2)) | → | mark#(X1) | (71) |
mark#(sel(X1,X2)) | → | mark#(X2) | (98) |
mark#(pair(X1,X2)) | → | mark#(X2) | (69) |
a__take#(N,XS) | → | mark#(XS) | (97) |
a__afterNth#(N,XS) | → | mark#(XS) | (67) |
mark#(U12(X1,X2)) | → | a__U12#(mark(X1),X2) | (96) |
a__U12#(pair(YS,ZS),X) | → | mark#(X) | (95) |
mark#(fst(X)) | → | mark#(X) | (66) |
a__natsFrom#(N) | → | mark#(N) | (65) |
mark#(take(X1,X2)) | → | mark#(X2) | (92) |
mark#(and(X1,X2)) | → | mark#(X1) | (91) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (64) |
a__fst#(pair(X,Y)) | → | mark#(X) | (90) |
a__snd#(pair(X,Y)) | → | mark#(Y) | (62) |
a__sel#(N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (60) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (88) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (89) |
mark#(U11(X1,X2,X3,X4)) | → | a__U11#(mark(X1),X2,X3,X4) | (87) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (59) |
a__take#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (57) |
mark#(cons(X1,X2)) | → | mark#(X1) | (86) |
mark#(snd(X)) | → | mark#(X) | (55) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (85) |
a__U11#(tt,N,X,XS) | → | mark#(N) | (54) |
mark#(fst(X)) | → | a__fst#(mark(X)) | (84) |
a__sel#(N,XS) | → | mark#(XS) | (53) |
a__afterNth#(N,XS) | → | mark#(N) | (82) |
a__take#(N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (81) |
mark#(head(X)) | → | a__head#(mark(X)) | (51) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (80) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (50) |
a__afterNth#(N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (49) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (78) |
a__take#(N,XS) | → | mark#(N) | (77) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (47) |
mark#(natsFrom(X)) | → | mark#(X) | (46) |
a__afterNth#(N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (45) |
mark#(take(X1,X2)) | → | mark#(X1) | (76) |
The dependency pairs are split into 2 components.
a__U11#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (52) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U11#(tt,N,X,XS) | (79) |
π(a__natsFrom#) | = | 1 |
π(and) | = | 2 |
π(fst) | = | 1 |
π(a__snd) | = | 1 |
π(a__fst) | = | 1 |
π(mark#) | = | 1 |
π(mark) | = | 1 |
π(snd) | = | 1 |
π(a__and) | = | 2 |
π(a__tail#) | = | 1 |
prec(U11) | = | 6 | status(U11) | = | [] | list-extension(U11) | = | Lex | ||
prec(s) | = | 6 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__head#) | = | 0 | status(a__head#) | = | [] | list-extension(a__head#) | = | Lex | ||
prec(a__snd#) | = | 0 | status(a__snd#) | = | [] | list-extension(a__snd#) | = | Lex | ||
prec(a__afterNth) | = | 4 | status(a__afterNth) | = | [] | list-extension(a__afterNth) | = | Lex | ||
prec(take) | = | 4 | status(take) | = | [1] | list-extension(take) | = | Lex | ||
prec(pair) | = | 0 | status(pair) | = | [] | list-extension(pair) | = | Lex | ||
prec(natsFrom) | = | 5 | status(natsFrom) | = | [] | list-extension(natsFrom) | = | Lex | ||
prec(splitAt) | = | 6 | status(splitAt) | = | [2] | list-extension(splitAt) | = | Lex | ||
prec(a__U11#) | = | 3 | status(a__U11#) | = | [2] | list-extension(a__U11#) | = | Lex | ||
prec(a__take#) | = | 0 | status(a__take#) | = | [1, 2] | list-extension(a__take#) | = | Lex | ||
prec(U12) | = | 1 | status(U12) | = | [] | list-extension(U12) | = | Lex | ||
prec(a__U12#) | = | 0 | status(a__U12#) | = | [1] | list-extension(a__U12#) | = | Lex | ||
prec(a__natsFrom) | = | 5 | status(a__natsFrom) | = | [] | list-extension(a__natsFrom) | = | Lex | ||
prec(tail) | = | 4 | status(tail) | = | [] | list-extension(tail) | = | Lex | ||
prec(0) | = | 5 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__and#) | = | 0 | status(a__and#) | = | [] | list-extension(a__and#) | = | Lex | ||
prec(sel) | = | 3 | status(sel) | = | [2] | list-extension(sel) | = | Lex | ||
prec(afterNth) | = | 4 | status(afterNth) | = | [] | list-extension(afterNth) | = | Lex | ||
prec(nil) | = | 6 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(a__splitAt) | = | 6 | status(a__splitAt) | = | [2] | list-extension(a__splitAt) | = | Lex | ||
prec(a__sel#) | = | 0 | status(a__sel#) | = | [] | list-extension(a__sel#) | = | Lex | ||
prec(a__U11) | = | 6 | status(a__U11) | = | [] | list-extension(a__U11) | = | Lex | ||
prec(a__sel) | = | 3 | status(a__sel) | = | [2] | list-extension(a__sel) | = | Lex | ||
prec(a__U12) | = | 1 | status(a__U12) | = | [] | list-extension(a__U12) | = | Lex | ||
prec(head) | = | 2 | status(head) | = | [] | list-extension(head) | = | Lex | ||
prec(a__afterNth#) | = | 0 | status(a__afterNth#) | = | [2] | list-extension(a__afterNth#) | = | Lex | ||
prec(a__splitAt#) | = | 3 | status(a__splitAt#) | = | [1] | list-extension(a__splitAt#) | = | Lex | ||
prec(cons) | = | 2 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(a__take) | = | 4 | status(a__take) | = | [1] | list-extension(a__take) | = | Lex | ||
prec(tt) | = | 6 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(a__fst#) | = | 0 | status(a__fst#) | = | [] | list-extension(a__fst#) | = | Lex | ||
prec(a__tail) | = | 4 | status(a__tail) | = | [] | list-extension(a__tail) | = | Lex | ||
prec(a__head) | = | 2 | status(a__head) | = | [] | list-extension(a__head) | = | Lex |
[U11(x1,...,x4)] | = | max(x1 + 24567, x3 + 24568, x4 + 24570, 0) |
[s(x1)] | = | x1 + 0 |
[a__head#(x1)] | = | 1 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | x2 + 24571 |
[take(x1, x2)] | = | x1 + x2 + 24571 |
[pair(x1, x2)] | = | max(x1 + 12284, x2 + 24569, 0) |
[natsFrom(x1)] | = | x1 + 12284 |
[splitAt(x1, x2)] | = | max(x2 + 24570, 0) |
[a__U11#(x1,...,x4)] | = | max(x1 + 0, x2 + 12282, x3 + 12285, x4 + 12284, 0) |
[a__take#(x1, x2)] | = | x1 + x2 + 1 |
[U12(x1, x2)] | = | max(x1 + 0, x2 + 24568, 0) |
[a__U12#(x1, x2)] | = | max(x1 + 1, 0) |
[a__natsFrom(x1)] | = | x1 + 12284 |
[tail(x1)] | = | x1 + 1 |
[0] | = | 0 |
[a__and#(x1, x2)] | = | x1 + 1 |
[sel(x1, x2)] | = | x2 + 38080 |
[afterNth(x1, x2)] | = | x2 + 24571 |
[nil] | = | 0 |
[a__splitAt(x1, x2)] | = | max(x2 + 24570, 0) |
[a__sel#(x1, x2)] | = | x2 + 1 |
[a__U11(x1,...,x4)] | = | max(x1 + 24567, x3 + 24568, x4 + 24570, 0) |
[a__sel(x1, x2)] | = | x2 + 38080 |
[a__U12(x1, x2)] | = | max(x1 + 0, x2 + 24568, 0) |
[head(x1)] | = | x1 + 13508 |
[a__afterNth#(x1, x2)] | = | x2 + 1 |
[a__splitAt#(x1, x2)] | = | max(x1 + 12282, x2 + 12284, 0) |
[cons(x1, x2)] | = | max(x1 + 12283, x2 + 0, 0) |
[a__take(x1, x2)] | = | x1 + x2 + 24571 |
[tt] | = | 12283 |
[a__fst#(x1)] | = | 1 |
[a__tail(x1)] | = | x1 + 1 |
[a__head(x1)] | = | x1 + 13508 |
mark(snd(X)) | → | a__snd(mark(X)) | (18) |
a__and(tt,X) | → | mark(X) | (4) |
mark(U12(X1,X2)) | → | a__U12(mark(X1),X2) | (15) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
a__U11(tt,N,X,XS) | → | a__U12(a__splitAt(mark(N),mark(XS)),X) | (1) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (3) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (16) |
mark(head(X)) | → | a__head(mark(X)) | (21) |
a__snd(X) | → | snd(X) | (36) |
mark(tt) | → | tt | (26) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (19) |
a__U11(X1,X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (17) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (27) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (34) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (22) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (28) |
a__fst(pair(X,Y)) | → | mark(X) | (5) |
a__U12(X1,X2) | → | U12(X1,X2) | (33) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (10) |
a__head(X) | → | head(X) | (39) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (7) |
mark(fst(X)) | → | a__fst(mark(X)) | (20) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (25) |
mark(0) | → | 0 | (30) |
mark(U11(X1,X2,X3,X4)) | → | a__U11(mark(X1),X2,X3,X4) | (14) |
mark(nil) | → | nil | (31) |
a__tail(cons(N,XS)) | → | mark(XS) | (12) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (23) |
mark(tail(X)) | → | a__tail(mark(X)) | (24) |
a__splitAt(s(N),cons(X,XS)) | → | a__U11(tt,N,X,XS) | (11) |
a__snd(pair(X,Y)) | → | mark(Y) | (9) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (13) |
a__natsFrom(X) | → | natsFrom(X) | (40) |
a__head(cons(N,XS)) | → | mark(N) | (6) |
a__fst(X) | → | fst(X) | (38) |
a__and(X1,X2) | → | and(X1,X2) | (37) |
a__sel(X1,X2) | → | sel(X1,X2) | (41) |
a__tail(X) | → | tail(X) | (42) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
mark(s(X)) | → | s(mark(X)) | (29) |
a__take(X1,X2) | → | take(X1,X2) | (43) |
a__U12(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (2) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U11#(tt,N,X,XS) | (79) |
The dependency pairs are split into 0 components.
mark#(U12(X1,X2)) | → | mark#(X1) | (58) |
mark#(head(X)) | → | mark#(X) | (56) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (93) |
mark#(tail(X)) | → | mark#(X) | (68) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (63) |
mark#(s(X)) | → | mark#(X) | (94) |
[U11(x1,...,x4)] | = | max(x1 + 4, x3 + 3, x4 + 2, 0) |
[s(x1)] | = | x1 + 0 |
[a__head#(x1)] | = | 58481 |
[a__natsFrom#(x1)] | = | 87762 |
[a__snd#(x1)] | = | 37895 |
[a__afterNth(x1, x2)] | = | max(x1 + 3, x2 + 4, 0) |
[take(x1, x2)] | = | max(x1 + 3, x2 + 4, 0) |
[and(x1, x2)] | = | max(x2 + 1, 0) |
[pair(x1, x2)] | = | max(x1 + 1, x2 + 2, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 9049 |
[a__snd(x1)] | = | x1 + 1 |
[splitAt(x1, x2)] | = | max(x2 + 2, 0) |
[a__U11#(x1,...,x4)] | = | max(0) |
[a__take#(x1, x2)] | = | max(0) |
[U12(x1, x2)] | = | max(x1 + 0, x2 + 3, 0) |
[a__U12#(x1, x2)] | = | max(0) |
[a__fst(x1)] | = | x1 + 1 |
[a__natsFrom(x1)] | = | x1 + 9049 |
[tail(x1)] | = | x1 + 2 |
[mark#(x1)] | = | x1 + 58481 |
[0] | = | 25828 |
[a__and#(x1, x2)] | = | max(0) |
[sel(x1, x2)] | = | max(x1 + 4, x2 + 5, 0) |
[afterNth(x1, x2)] | = | max(x1 + 3, x2 + 4, 0) |
[nil] | = | 1 |
[a__splitAt(x1, x2)] | = | max(x2 + 2, 0) |
[a__sel#(x1, x2)] | = | max(0) |
[mark(x1)] | = | x1 + 0 |
[a__U11(x1,...,x4)] | = | max(x1 + 4, x3 + 3, x4 + 2, 0) |
[a__sel(x1, x2)] | = | max(x1 + 4, x2 + 5, 0) |
[a__U12(x1, x2)] | = | max(x1 + 0, x2 + 3, 0) |
[head(x1)] | = | x1 + 1 |
[a__afterNth#(x1, x2)] | = | max(0) |
[a__splitAt#(x1, x2)] | = | max(0) |
[cons(x1, x2)] | = | max(x1 + 2, x2 + 0, 0) |
[snd(x1)] | = | x1 + 1 |
[a__take(x1, x2)] | = | max(x1 + 3, x2 + 4, 0) |
[tt] | = | 0 |
[a__fst#(x1)] | = | 37895 |
[a__and(x1, x2)] | = | max(x2 + 1, 0) |
[a__tail(x1)] | = | x1 + 2 |
[a__tail#(x1)] | = | x1 + 58482 |
[a__head(x1)] | = | x1 + 1 |
mark(snd(X)) | → | a__snd(mark(X)) | (18) |
a__and(tt,X) | → | mark(X) | (4) |
mark(U12(X1,X2)) | → | a__U12(mark(X1),X2) | (15) |
a__sel(N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
a__U11(tt,N,X,XS) | → | a__U12(a__splitAt(mark(N),mark(XS)),X) | (1) |
a__afterNth(N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (3) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (16) |
mark(head(X)) | → | a__head(mark(X)) | (21) |
a__snd(X) | → | snd(X) | (36) |
mark(tt) | → | tt | (26) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (19) |
a__U11(X1,X2,X3,X4) | → | U11(X1,X2,X3,X4) | (32) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (17) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (27) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (34) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (22) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (28) |
a__fst(pair(X,Y)) | → | mark(X) | (5) |
a__U12(X1,X2) | → | U12(X1,X2) | (33) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (10) |
a__head(X) | → | head(X) | (39) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (7) |
mark(fst(X)) | → | a__fst(mark(X)) | (20) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (25) |
mark(0) | → | 0 | (30) |
mark(U11(X1,X2,X3,X4)) | → | a__U11(mark(X1),X2,X3,X4) | (14) |
mark(nil) | → | nil | (31) |
a__tail(cons(N,XS)) | → | mark(XS) | (12) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (23) |
mark(tail(X)) | → | a__tail(mark(X)) | (24) |
a__splitAt(s(N),cons(X,XS)) | → | a__U11(tt,N,X,XS) | (11) |
a__snd(pair(X,Y)) | → | mark(Y) | (9) |
a__take(N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (13) |
a__natsFrom(X) | → | natsFrom(X) | (40) |
a__head(cons(N,XS)) | → | mark(N) | (6) |
a__fst(X) | → | fst(X) | (38) |
a__and(X1,X2) | → | and(X1,X2) | (37) |
a__sel(X1,X2) | → | sel(X1,X2) | (41) |
a__tail(X) | → | tail(X) | (42) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (35) |
mark(s(X)) | → | s(mark(X)) | (29) |
a__take(X1,X2) | → | take(X1,X2) | (43) |
a__U12(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (2) |
mark#(head(X)) | → | mark#(X) | (56) |
a__tail#(cons(N,XS)) | → | mark#(XS) | (93) |
mark#(tail(X)) | → | mark#(X) | (68) |
mark#(tail(X)) | → | a__tail#(mark(X)) | (63) |
The dependency pairs are split into 1 component.
mark#(U12(X1,X2)) | → | mark#(X1) | (58) |
mark#(s(X)) | → | mark#(X) | (94) |
[U11(x1,...,x4)] | = | x1 + 6 |
[s(x1)] | = | x1 + 1 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 0 |
[a__snd#(x1)] | = | 0 |
[a__afterNth(x1, x2)] | = | x2 + 1 |
[take(x1, x2)] | = | x2 + 5 |
[and(x1, x2)] | = | x1 + x2 + 5 |
[pair(x1, x2)] | = | x1 + 1 |
[fst(x1)] | = | 2 |
[natsFrom(x1)] | = | 5 |
[a__snd(x1)] | = | 2 |
[splitAt(x1, x2)] | = | x1 + 5 |
[a__U11#(x1,...,x4)] | = | 0 |
[a__take#(x1, x2)] | = | 0 |
[U12(x1, x2)] | = | x1 + x2 + 3 |
[a__U12#(x1, x2)] | = | 0 |
[a__fst(x1)] | = | x1 + 1 |
[a__natsFrom(x1)] | = | 4 |
[tail(x1)] | = | x1 + 5 |
[mark#(x1)] | = | x1 + 1 |
[0] | = | 4 |
[a__and#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | x1 + 2 |
[afterNth(x1, x2)] | = | x1 + 2 |
[nil] | = | 4 |
[a__splitAt(x1, x2)] | = | 4 |
[a__sel#(x1, x2)] | = | 0 |
[mark(x1)] | = | 3 |
[a__U11(x1,...,x4)] | = | x4 + 5 |
[a__sel(x1, x2)] | = | x2 + 1 |
[a__U12(x1, x2)] | = | x1 + 2 |
[head(x1)] | = | 5 |
[a__afterNth#(x1, x2)] | = | 0 |
[a__splitAt#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 5 |
[snd(x1)] | = | 3 |
[a__take(x1, x2)] | = | 4 |
[tt] | = | 4 |
[a__fst#(x1)] | = | 0 |
[a__and(x1, x2)] | = | 4 |
[a__tail(x1)] | = | 4 |
[a__tail#(x1)] | = | 0 |
[a__head(x1)] | = | x1 + 4 |
mark#(U12(X1,X2)) | → | mark#(X1) | (58) |
mark#(s(X)) | → | mark#(X) | (94) |
The dependency pairs are split into 0 components.