The rewrite relation of the following TRS is considered.
a__U11(tt,N,XS) | → | a__U12(tt,N,XS) | (1) |
a__U12(tt,N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (2) |
a__U21(tt,X) | → | a__U22(tt,X) | (3) |
a__U22(tt,X) | → | mark(X) | (4) |
a__U31(tt,N) | → | a__U32(tt,N) | (5) |
a__U32(tt,N) | → | mark(N) | (6) |
a__U41(tt,N,XS) | → | a__U42(tt,N,XS) | (7) |
a__U42(tt,N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
a__U51(tt,Y) | → | a__U52(tt,Y) | (9) |
a__U52(tt,Y) | → | mark(Y) | (10) |
a__U61(tt,N,X,XS) | → | a__U62(tt,N,X,XS) | (11) |
a__U62(tt,N,X,XS) | → | a__U63(tt,N,X,XS) | (12) |
a__U63(tt,N,X,XS) | → | a__U64(a__splitAt(mark(N),mark(XS)),X) | (13) |
a__U64(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (14) |
a__U71(tt,XS) | → | a__U72(tt,XS) | (15) |
a__U72(tt,XS) | → | mark(XS) | (16) |
a__U81(tt,N,XS) | → | a__U82(tt,N,XS) | (17) |
a__U82(tt,N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (18) |
a__afterNth(N,XS) | → | a__U11(tt,N,XS) | (19) |
a__fst(pair(X,Y)) | → | a__U21(tt,X) | (20) |
a__head(cons(N,XS)) | → | a__U31(tt,N) | (21) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (22) |
a__sel(N,XS) | → | a__U41(tt,N,XS) | (23) |
a__snd(pair(X,Y)) | → | a__U51(tt,Y) | (24) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (25) |
a__splitAt(s(N),cons(X,XS)) | → | a__U61(tt,N,X,XS) | (26) |
a__tail(cons(N,XS)) | → | a__U71(tt,XS) | (27) |
a__take(N,XS) | → | a__U81(tt,N,XS) | (28) |
mark(U11(X1,X2,X3)) | → | a__U11(mark(X1),X2,X3) | (29) |
mark(U12(X1,X2,X3)) | → | a__U12(mark(X1),X2,X3) | (30) |
mark(snd(X)) | → | a__snd(mark(X)) | (31) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (32) |
mark(U21(X1,X2)) | → | a__U21(mark(X1),X2) | (33) |
mark(U22(X1,X2)) | → | a__U22(mark(X1),X2) | (34) |
mark(U31(X1,X2)) | → | a__U31(mark(X1),X2) | (35) |
mark(U32(X1,X2)) | → | a__U32(mark(X1),X2) | (36) |
mark(U41(X1,X2,X3)) | → | a__U41(mark(X1),X2,X3) | (37) |
mark(U42(X1,X2,X3)) | → | a__U42(mark(X1),X2,X3) | (38) |
mark(head(X)) | → | a__head(mark(X)) | (39) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (40) |
mark(U51(X1,X2)) | → | a__U51(mark(X1),X2) | (41) |
mark(U52(X1,X2)) | → | a__U52(mark(X1),X2) | (42) |
mark(U61(X1,X2,X3,X4)) | → | a__U61(mark(X1),X2,X3,X4) | (43) |
mark(U62(X1,X2,X3,X4)) | → | a__U62(mark(X1),X2,X3,X4) | (44) |
mark(U63(X1,X2,X3,X4)) | → | a__U63(mark(X1),X2,X3,X4) | (45) |
mark(U64(X1,X2)) | → | a__U64(mark(X1),X2) | (46) |
mark(U71(X1,X2)) | → | a__U71(mark(X1),X2) | (47) |
mark(U72(X1,X2)) | → | a__U72(mark(X1),X2) | (48) |
mark(U81(X1,X2,X3)) | → | a__U81(mark(X1),X2,X3) | (49) |
mark(U82(X1,X2,X3)) | → | a__U82(mark(X1),X2,X3) | (50) |
mark(fst(X)) | → | a__fst(mark(X)) | (51) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (52) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (53) |
mark(tail(X)) | → | a__tail(mark(X)) | (54) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (55) |
mark(tt) | → | tt | (56) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (57) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (58) |
mark(s(X)) | → | s(mark(X)) | (59) |
mark(0) | → | 0 | (60) |
mark(nil) | → | nil | (61) |
a__U11(X1,X2,X3) | → | U11(X1,X2,X3) | (62) |
a__U12(X1,X2,X3) | → | U12(X1,X2,X3) | (63) |
a__snd(X) | → | snd(X) | (64) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (65) |
a__U21(X1,X2) | → | U21(X1,X2) | (66) |
a__U22(X1,X2) | → | U22(X1,X2) | (67) |
a__U31(X1,X2) | → | U31(X1,X2) | (68) |
a__U32(X1,X2) | → | U32(X1,X2) | (69) |
a__U41(X1,X2,X3) | → | U41(X1,X2,X3) | (70) |
a__U42(X1,X2,X3) | → | U42(X1,X2,X3) | (71) |
a__head(X) | → | head(X) | (72) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (73) |
a__U51(X1,X2) | → | U51(X1,X2) | (74) |
a__U52(X1,X2) | → | U52(X1,X2) | (75) |
a__U61(X1,X2,X3,X4) | → | U61(X1,X2,X3,X4) | (76) |
a__U62(X1,X2,X3,X4) | → | U62(X1,X2,X3,X4) | (77) |
a__U63(X1,X2,X3,X4) | → | U63(X1,X2,X3,X4) | (78) |
a__U64(X1,X2) | → | U64(X1,X2) | (79) |
a__U71(X1,X2) | → | U71(X1,X2) | (80) |
a__U72(X1,X2) | → | U72(X1,X2) | (81) |
a__U81(X1,X2,X3) | → | U81(X1,X2,X3) | (82) |
a__U82(X1,X2,X3) | → | U82(X1,X2,X3) | (83) |
a__fst(X) | → | fst(X) | (84) |
a__natsFrom(X) | → | natsFrom(X) | (85) |
a__sel(X1,X2) | → | sel(X1,X2) | (86) |
a__tail(X) | → | tail(X) | (87) |
a__take(X1,X2) | → | take(X1,X2) | (88) |
There are 103 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
There are 103 ruless (increase limit for explicit display).
[a__U63(x1,...,x4)] | = | max(x1 + 16, x2 + 22, x3 + 23, x4 + 35, 0) |
[U21(x1, x2)] | = | max(x1 + 17, x2 + 18, 0) |
[a__U82#(x1, x2, x3)] | = | max(x1 + 61, x2 + 60, x3 + 59, 0) |
[a__U72#(x1, x2)] | = | max(x1 + 26, x2 + 23, 0) |
[a__U71#(x1, x2)] | = | max(x1 + 26, x2 + 24, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 43, x2 + 42, x3 + 45, 0) |
[U64(x1, x2)] | = | max(x1 + 0, x2 + 23, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2)] | = | max(x1 + 21, x2 + 24, 0) |
[a__head#(x1)] | = | x1 + 26 |
[a__natsFrom#(x1)] | = | x1 + 22 |
[a__snd#(x1)] | = | x1 + 5 |
[a__afterNth(x1, x2)] | = | max(x1 + 42, x2 + 48, 0) |
[U42(x1, x2, x3)] | = | max(x1 + 62, x2 + 61, x3 + 63, 0) |
[a__U82(x1, x2, x3)] | = | max(x1 + 39, x2 + 38, x3 + 37, 0) |
[take(x1, x2)] | = | max(x1 + 48, x2 + 25586, 0) |
[U71(x1, x2)] | = | max(x1 + 4, x2 + 3, 0) |
[a__U62(x1,...,x4)] | = | max(x1 + 29, x2 + 22, x3 + 29, x4 + 35, 0) |
[pair(x1, x2)] | = | max(x1 + 20, x2 + 27, 0) |
[fst(x1)] | = | x1 + 1 |
[natsFrom(x1)] | = | x1 + 18005 |
[a__snd(x1)] | = | x1 + 6 |
[a__U51#(x1, x2)] | = | max(x1 + 19, x2 + 24, 0) |
[U63(x1,...,x4)] | = | max(x1 + 16, x2 + 22, x3 + 23, x4 + 35, 0) |
[a__U22(x1, x2)] | = | max(x1 + 14, x2 + 1, 0) |
[splitAt(x1, x2)] | = | max(x1 + 22, x2 + 35, 0) |
[a__U64(x1, x2)] | = | max(x1 + 0, x2 + 23, 0) |
[U72(x1, x2)] | = | max(x1 + 4, x2 + 3, 0) |
[a__U11#(x1, x2, x3)] | = | max(x2 + 51, x3 + 42, 0) |
[a__U31(x1, x2)] | = | max(x1 + 7, x2 + 3, 0) |
[a__U51(x1, x2)] | = | max(x1 + 23, x2 + 29, 0) |
[a__U81(x1, x2, x3)] | = | max(x1 + 44, x2 + 46, x3 + 45, 0) |
[a__take#(x1, x2)] | = | max(x1 + 69, x2 + 14033, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 22, x2 + 42, x3 + 41, 0) |
[a__U62#(x1,...,x4)] | = | max(x1 + 34, x2 + 39, x3 + 23, x4 + 37, 0) |
[a__U42#(x1, x2, x3)] | = | max(x1 + 72, x2 + 76, x3 + 74, 0) |
[a__U41(x1, x2, x3)] | = | max(x1 + 55, x2 + 3090, x3 + 63, 0) |
[a__U64#(x1, x2)] | = | max(x1 + 1, x2 + 22, 0) |
[a__U12#(x1, x2, x3)] | = | max(x1 + 16, x2 + 43, x3 + 41, 0) |
[a__U21#(x1, x2)] | = | max(x1 + 39, x2 + 40, 0) |
[a__U81#(x1, x2, x3)] | = | max(x1 + 66, x2 + 68, x3 + 67, 0) |
[a__U61#(x1,...,x4)] | = | max(x1 + 34, x2 + 39, x3 + 23, x4 + 37, 0) |
[a__fst(x1)] | = | x1 + 1 |
[a__natsFrom(x1)] | = | x1 + 18005 |
[tail(x1)] | = | x1 + 10 |
[mark#(x1)] | = | x1 + 22 |
[0] | = | 4 |
[a__U21(x1, x2)] | = | max(x1 + 17, x2 + 18, 0) |
[a__U32(x1, x2)] | = | max(x1 + 5, x2 + 2, 0) |
[sel(x1, x2)] | = | max(x1 + 3090, x2 + 63, 0) |
[afterNth(x1, x2)] | = | max(x1 + 42, x2 + 48, 0) |
[nil] | = | 7 |
[a__splitAt(x1, x2)] | = | max(x1 + 22, x2 + 35, 0) |
[U62(x1,...,x4)] | = | max(x1 + 29, x2 + 22, x3 + 29, x4 + 35, 0) |
[a__U52#(x1, x2)] | = | max(x2 + 23, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 3112, x2 + 85, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U72(x1, x2)] | = | max(x1 + 4, x2 + 3, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 43, x2 + 42, x3 + 45, 0) |
[U32(x1, x2)] | = | max(x1 + 5, x2 + 2, 0) |
[a__sel(x1, x2)] | = | max(x1 + 3090, x2 + 63, 0) |
[a__U42(x1, x2, x3)] | = | max(x1 + 62, x2 + 61, x3 + 63, 0) |
[a__U52(x1, x2)] | = | max(x1 + 24, x2 + 1, 0) |
[a__U12(x1, x2, x3)] | = | max(x1 + 22, x2 + 42, x3 + 41, 0) |
[a__U63#(x1,...,x4)] | = | max(x1 + 34, x2 + 39, x3 + 22, x4 + 37, 0) |
[U52(x1, x2)] | = | max(x1 + 24, x2 + 1, 0) |
[U61(x1,...,x4)] | = | max(x1 + 23, x2 + 22, x3 + 30, x4 + 35, 0) |
[a__U22#(x1, x2)] | = | max(x2 + 23, 0) |
[U31(x1, x2)] | = | max(x1 + 7, x2 + 3, 0) |
[a__U71(x1, x2)] | = | max(x1 + 4, x2 + 3, 0) |
[head(x1)] | = | x1 + 15 |
[a__afterNth#(x1, x2)] | = | max(x1 + 51, x2 + 69, 0) |
[a__splitAt#(x1, x2)] | = | max(x1 + 39, x2 + 37, 0) |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U61(x1,...,x4)] | = | max(x1 + 23, x2 + 22, x3 + 30, x4 + 35, 0) |
[snd(x1)] | = | x1 + 6 |
[a__take(x1, x2)] | = | max(x1 + 48, x2 + 25586, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 44, x2 + 46, x3 + 45, 0) |
[a__U41#(x1, x2, x3)] | = | max(x1 + 77, x2 + 76, x3 + 75, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 39, x2 + 38, x3 + 37, 0) |
[tt] | = | 5 |
[a__fst#(x1)] | = | x1 + 23 |
[U22(x1, x2)] | = | max(x1 + 14, x2 + 1, 0) |
[U51(x1, x2)] | = | max(x1 + 23, x2 + 29, 0) |
[a__tail(x1)] | = | x1 + 10 |
[U41(x1, x2, x3)] | = | max(x1 + 55, x2 + 3090, x3 + 63, 0) |
[a__tail#(x1)] | = | x1 + 32 |
[a__U32#(x1, x2)] | = | max(x1 + 20, x2 + 23, 0) |
[a__head(x1)] | = | x1 + 15 |
a__U82(tt,N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (18) |
mark(U82(X1,X2,X3)) | → | a__U82(mark(X1),X2,X3) | (50) |
a__U71(X1,X2) | → | U71(X1,X2) | (80) |
a__U22(tt,X) | → | mark(X) | (4) |
a__U71(tt,XS) | → | a__U72(tt,XS) | (15) |
a__U42(tt,N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
mark(tail(X)) | → | a__tail(mark(X)) | (54) |
a__U11(tt,N,XS) | → | a__U12(tt,N,XS) | (1) |
a__U62(X1,X2,X3,X4) | → | U62(X1,X2,X3,X4) | (77) |
a__U21(tt,X) | → | a__U22(tt,X) | (3) |
a__U72(tt,XS) | → | mark(XS) | (16) |
a__head(cons(N,XS)) | → | a__U31(tt,N) | (21) |
mark(U32(X1,X2)) | → | a__U32(mark(X1),X2) | (36) |
a__U31(X1,X2) | → | U31(X1,X2) | (68) |
a__natsFrom(X) | → | natsFrom(X) | (85) |
a__splitAt(s(N),cons(X,XS)) | → | a__U61(tt,N,X,XS) | (26) |
a__U12(X1,X2,X3) | → | U12(X1,X2,X3) | (63) |
a__afterNth(N,XS) | → | a__U11(tt,N,XS) | (19) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (32) |
a__U81(tt,N,XS) | → | a__U82(tt,N,XS) | (17) |
mark(0) | → | 0 | (60) |
a__tail(cons(N,XS)) | → | a__U71(tt,XS) | (27) |
a__tail(X) | → | tail(X) | (87) |
a__fst(X) | → | fst(X) | (84) |
mark(U22(X1,X2)) | → | a__U22(mark(X1),X2) | (34) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (22) |
a__take(N,XS) | → | a__U81(tt,N,XS) | (28) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (65) |
mark(U62(X1,X2,X3,X4)) | → | a__U62(mark(X1),X2,X3,X4) | (44) |
a__U31(tt,N) | → | a__U32(tt,N) | (5) |
a__head(X) | → | head(X) | (72) |
mark(U21(X1,X2)) | → | a__U21(mark(X1),X2) | (33) |
a__snd(X) | → | snd(X) | (64) |
a__U52(tt,Y) | → | mark(Y) | (10) |
mark(head(X)) | → | a__head(mark(X)) | (39) |
a__U41(tt,N,XS) | → | a__U42(tt,N,XS) | (7) |
a__take(X1,X2) | → | take(X1,X2) | (88) |
a__fst(pair(X,Y)) | → | a__U21(tt,X) | (20) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (25) |
mark(U81(X1,X2,X3)) | → | a__U81(mark(X1),X2,X3) | (49) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (52) |
mark(U12(X1,X2,X3)) | → | a__U12(mark(X1),X2,X3) | (30) |
a__U11(X1,X2,X3) | → | U11(X1,X2,X3) | (62) |
a__U64(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (14) |
a__U81(X1,X2,X3) | → | U81(X1,X2,X3) | (82) |
mark(tt) | → | tt | (56) |
a__U64(X1,X2) | → | U64(X1,X2) | (79) |
mark(snd(X)) | → | a__snd(mark(X)) | (31) |
a__U62(tt,N,X,XS) | → | a__U63(tt,N,X,XS) | (12) |
a__U32(X1,X2) | → | U32(X1,X2) | (69) |
mark(U63(X1,X2,X3,X4)) | → | a__U63(mark(X1),X2,X3,X4) | (45) |
a__U63(X1,X2,X3,X4) | → | U63(X1,X2,X3,X4) | (78) |
a__U72(X1,X2) | → | U72(X1,X2) | (81) |
a__sel(N,XS) | → | a__U41(tt,N,XS) | (23) |
a__U41(X1,X2,X3) | → | U41(X1,X2,X3) | (70) |
a__snd(pair(X,Y)) | → | a__U51(tt,Y) | (24) |
a__U61(X1,X2,X3,X4) | → | U61(X1,X2,X3,X4) | (76) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (57) |
a__U61(tt,N,X,XS) | → | a__U62(tt,N,X,XS) | (11) |
a__U51(tt,Y) | → | a__U52(tt,Y) | (9) |
a__U63(tt,N,X,XS) | → | a__U64(a__splitAt(mark(N),mark(XS)),X) | (13) |
mark(fst(X)) | → | a__fst(mark(X)) | (51) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (40) |
a__U22(X1,X2) | → | U22(X1,X2) | (67) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (55) |
mark(s(X)) | → | s(mark(X)) | (59) |
a__U32(tt,N) | → | mark(N) | (6) |
mark(U42(X1,X2,X3)) | → | a__U42(mark(X1),X2,X3) | (38) |
mark(nil) | → | nil | (61) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (58) |
a__U51(X1,X2) | → | U51(X1,X2) | (74) |
a__U52(X1,X2) | → | U52(X1,X2) | (75) |
mark(U72(X1,X2)) | → | a__U72(mark(X1),X2) | (48) |
a__U42(X1,X2,X3) | → | U42(X1,X2,X3) | (71) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (53) |
mark(U71(X1,X2)) | → | a__U71(mark(X1),X2) | (47) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (73) |
mark(U41(X1,X2,X3)) | → | a__U41(mark(X1),X2,X3) | (37) |
mark(U51(X1,X2)) | → | a__U51(mark(X1),X2) | (41) |
mark(U52(X1,X2)) | → | a__U52(mark(X1),X2) | (42) |
mark(U64(X1,X2)) | → | a__U64(mark(X1),X2) | (46) |
a__U21(X1,X2) | → | U21(X1,X2) | (66) |
a__U82(X1,X2,X3) | → | U82(X1,X2,X3) | (83) |
mark(U31(X1,X2)) | → | a__U31(mark(X1),X2) | (35) |
mark(U11(X1,X2,X3)) | → | a__U11(mark(X1),X2,X3) | (29) |
mark(U61(X1,X2,X3,X4)) | → | a__U61(mark(X1),X2,X3,X4) | (43) |
a__sel(X1,X2) | → | sel(X1,X2) | (86) |
a__U12(tt,N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (2) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (191) |
mark#(splitAt(X1,X2)) | → | mark#(X1) | (189) |
mark#(U63(X1,X2,X3,X4)) | → | mark#(X1) | (190) |
mark#(U72(X1,X2)) | → | mark#(X1) | (148) |
mark#(snd(X)) | → | a__snd#(mark(X)) | (146) |
mark#(U63(X1,X2,X3,X4)) | → | a__U63#(mark(X1),X2,X3,X4) | (147) |
a__U12#(tt,N,XS) | → | mark#(XS) | (188) |
a__splitAt#(0,XS) | → | mark#(XS) | (144) |
a__U82#(tt,N,XS) | → | mark#(XS) | (187) |
a__U82#(tt,N,XS) | → | mark#(N) | (186) |
mark#(U52(X1,X2)) | → | mark#(X1) | (143) |
mark#(U51(X1,X2)) | → | a__U51#(mark(X1),X2) | (185) |
a__U11#(tt,N,XS) | → | a__U12#(tt,N,XS) | (141) |
mark#(splitAt(X1,X2)) | → | a__splitAt#(mark(X1),mark(X2)) | (139) |
mark#(U12(X1,X2,X3)) | → | a__U12#(mark(X1),X2,X3) | (140) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (138) |
a__U82#(tt,N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (136) |
mark#(U21(X1,X2)) | → | mark#(X1) | (135) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (184) |
mark#(pair(X1,X2)) | → | mark#(X1) | (133) |
a__U81#(tt,N,XS) | → | a__U82#(tt,N,XS) | (132) |
mark#(splitAt(X1,X2)) | → | mark#(X2) | (131) |
a__U12#(tt,N,XS) | → | a__snd#(a__splitAt(mark(N),mark(XS))) | (182) |
mark#(sel(X1,X2)) | → | mark#(X2) | (130) |
a__tail#(cons(N,XS)) | → | a__U71#(tt,XS) | (181) |
a__U31#(tt,N) | → | a__U32#(tt,N) | (129) |
a__U12#(tt,N,XS) | → | mark#(N) | (180) |
mark#(U51(X1,X2)) | → | mark#(X1) | (179) |
a__U42#(tt,N,XS) | → | mark#(N) | (127) |
mark#(U22(X1,X2)) | → | mark#(X1) | (126) |
mark#(afterNth(X1,X2)) | → | mark#(X2) | (177) |
mark#(U12(X1,X2,X3)) | → | mark#(X1) | (125) |
mark#(U32(X1,X2)) | → | mark#(X1) | (175) |
a__U82#(tt,N,XS) | → | a__fst#(a__splitAt(mark(N),mark(XS))) | (174) |
mark#(U64(X1,X2)) | → | a__U64#(mark(X1),X2) | (123) |
mark#(U31(X1,X2)) | → | a__U31#(mark(X1),X2) | (122) |
a__fst#(pair(X,Y)) | → | a__U21#(tt,X) | (172) |
mark#(take(X1,X2)) | → | mark#(X1) | (170) |
a__U52#(tt,Y) | → | mark#(Y) | (117) |
a__U64#(pair(YS,ZS),X) | → | mark#(ZS) | (116) |
mark#(natsFrom(X)) | → | mark#(X) | (115) |
mark#(U61(X1,X2,X3,X4)) | → | mark#(X1) | (114) |
mark#(U42(X1,X2,X3)) | → | a__U42#(mark(X1),X2,X3) | (167) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (112) |
mark#(fst(X)) | → | mark#(X) | (113) |
a__U72#(tt,XS) | → | mark#(XS) | (166) |
mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | (111) |
mark#(U32(X1,X2)) | → | a__U32#(mark(X1),X2) | (165) |
mark#(afterNth(X1,X2)) | → | a__afterNth#(mark(X1),mark(X2)) | (164) |
a__sel#(N,XS) | → | a__U41#(tt,N,XS) | (108) |
mark#(U62(X1,X2,X3,X4)) | → | a__U62#(mark(X1),X2,X3,X4) | (107) |
mark#(sel(X1,X2)) | → | mark#(X1) | (163) |
mark#(snd(X)) | → | mark#(X) | (106) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (162) |
mark#(head(X)) | → | a__head#(mark(X)) | (161) |
a__take#(N,XS) | → | a__U81#(tt,N,XS) | (104) |
a__snd#(pair(X,Y)) | → | a__U51#(tt,Y) | (105) |
mark#(tail(X)) | → | mark#(X) | (103) |
mark#(U61(X1,X2,X3,X4)) | → | a__U61#(mark(X1),X2,X3,X4) | (159) |
a__U22#(tt,X) | → | mark#(X) | (102) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (101) |
mark#(U62(X1,X2,X3,X4)) | → | mark#(X1) | (158) |
mark#(take(X1,X2)) | → | mark#(X2) | (157) |
a__U42#(tt,N,XS) | → | a__afterNth#(mark(N),mark(XS)) | (155) |
a__U63#(tt,N,X,XS) | → | mark#(N) | (99) |
a__U42#(tt,N,XS) | → | mark#(XS) | (98) |
a__U63#(tt,N,X,XS) | → | mark#(XS) | (97) |
mark#(U31(X1,X2)) | → | mark#(X1) | (153) |
mark#(pair(X1,X2)) | → | mark#(X2) | (96) |
mark#(head(X)) | → | mark#(X) | (95) |
a__U21#(tt,X) | → | a__U22#(tt,X) | (150) |
mark#(U11(X1,X2,X3)) | → | a__U11#(mark(X1),X2,X3) | (151) |
mark#(afterNth(X1,X2)) | → | mark#(X1) | (93) |
a__U32#(tt,N) | → | mark#(N) | (92) |
a__U51#(tt,Y) | → | a__U52#(tt,Y) | (91) |
a__U12#(tt,N,XS) | → | a__splitAt#(mark(N),mark(XS)) | (89) |
mark#(U71(X1,X2)) | → | mark#(X1) | (149) |
The dependency pairs are split into 2 components.
a__splitAt#(s(N),cons(X,XS)) | → | a__U61#(tt,N,X,XS) | (94) |
a__U62#(tt,N,X,XS) | → | a__U63#(tt,N,X,XS) | (120) |
a__U61#(tt,N,X,XS) | → | a__U62#(tt,N,X,XS) | (160) |
a__U63#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (118) |
π(a__U71#) | = | 2 |
π(a__U31#) | = | 2 |
π(a__natsFrom#) | = | 1 |
π(fst) | = | 1 |
π(a__U42#) | = | 2 |
π(a__fst) | = | 1 |
π(mark) | = | 1 |
prec(a__U63) | = | 2 | status(a__U63) | = | [2, 3] | list-extension(a__U63) | = | Lex | ||
prec(U21) | = | 1 | status(U21) | = | [] | list-extension(U21) | = | Lex | ||
prec(a__U82#) | = | 0 | status(a__U82#) | = | [1, 2, 3] | list-extension(a__U82#) | = | Lex | ||
prec(a__U72#) | = | 0 | status(a__U72#) | = | [1] | list-extension(a__U72#) | = | Lex | ||
prec(U11) | = | 8 | status(U11) | = | [] | list-extension(U11) | = | Lex | ||
prec(U64) | = | 2 | status(U64) | = | [] | list-extension(U64) | = | 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) | = | 9 | status(a__afterNth) | = | [1, 2] | list-extension(a__afterNth) | = | Lex | ||
prec(U42) | = | 1 | status(U42) | = | [] | list-extension(U42) | = | Lex | ||
prec(a__U82) | = | 6 | status(a__U82) | = | [] | list-extension(a__U82) | = | Lex | ||
prec(take) | = | 7 | status(take) | = | [] | list-extension(take) | = | Lex | ||
prec(U71) | = | 7 | status(U71) | = | [] | list-extension(U71) | = | Lex | ||
prec(a__U62) | = | 5 | status(a__U62) | = | [] | list-extension(a__U62) | = | Lex | ||
prec(pair) | = | 2 | status(pair) | = | [] | list-extension(pair) | = | Lex | ||
prec(natsFrom) | = | 5 | status(natsFrom) | = | [] | list-extension(natsFrom) | = | Lex | ||
prec(a__snd) | = | 7 | status(a__snd) | = | [] | list-extension(a__snd) | = | Lex | ||
prec(a__U51#) | = | 0 | status(a__U51#) | = | [] | list-extension(a__U51#) | = | Lex | ||
prec(U63) | = | 2 | status(U63) | = | [2, 3] | list-extension(U63) | = | Lex | ||
prec(a__U22) | = | 1 | status(a__U22) | = | [] | list-extension(a__U22) | = | Lex | ||
prec(splitAt) | = | 6 | status(splitAt) | = | [] | list-extension(splitAt) | = | Lex | ||
prec(a__U64) | = | 2 | status(a__U64) | = | [] | list-extension(a__U64) | = | Lex | ||
prec(U72) | = | 6 | status(U72) | = | [2] | list-extension(U72) | = | Lex | ||
prec(a__U11#) | = | 0 | status(a__U11#) | = | [1] | list-extension(a__U11#) | = | Lex | ||
prec(a__U31) | = | 2 | status(a__U31) | = | [2] | list-extension(a__U31) | = | Lex | ||
prec(a__U51) | = | 7 | status(a__U51) | = | [] | list-extension(a__U51) | = | Lex | ||
prec(a__U81) | = | 6 | status(a__U81) | = | [] | list-extension(a__U81) | = | Lex | ||
prec(a__take#) | = | 0 | status(a__take#) | = | [1, 2] | list-extension(a__take#) | = | Lex | ||
prec(U12) | = | 7 | status(U12) | = | [2, 3] | list-extension(U12) | = | Lex | ||
prec(a__U62#) | = | 5 | status(a__U62#) | = | [1, 2] | list-extension(a__U62#) | = | Lex | ||
prec(a__U41) | = | 2 | status(a__U41) | = | [2] | list-extension(a__U41) | = | Lex | ||
prec(a__U64#) | = | 0 | status(a__U64#) | = | [1] | list-extension(a__U64#) | = | Lex | ||
prec(a__U12#) | = | 0 | status(a__U12#) | = | [2, 1, 3] | list-extension(a__U12#) | = | Lex | ||
prec(a__U21#) | = | 0 | status(a__U21#) | = | [2, 1] | list-extension(a__U21#) | = | Lex | ||
prec(a__U81#) | = | 0 | status(a__U81#) | = | [2, 3, 1] | list-extension(a__U81#) | = | Lex | ||
prec(a__U61#) | = | 5 | status(a__U61#) | = | [1, 2] | list-extension(a__U61#) | = | Lex | ||
prec(a__natsFrom) | = | 5 | status(a__natsFrom) | = | [] | list-extension(a__natsFrom) | = | Lex | ||
prec(tail) | = | 7 | status(tail) | = | [] | list-extension(tail) | = | Lex | ||
prec(mark#) | = | 0 | status(mark#) | = | [] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 7 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__U21) | = | 1 | status(a__U21) | = | [] | list-extension(a__U21) | = | Lex | ||
prec(a__U32) | = | 2 | status(a__U32) | = | [] | list-extension(a__U32) | = | Lex | ||
prec(sel) | = | 7 | status(sel) | = | [2, 1] | list-extension(sel) | = | Lex | ||
prec(afterNth) | = | 9 | status(afterNth) | = | [1, 2] | list-extension(afterNth) | = | Lex | ||
prec(nil) | = | 7 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(a__splitAt) | = | 6 | status(a__splitAt) | = | [] | list-extension(a__splitAt) | = | Lex | ||
prec(U62) | = | 5 | status(U62) | = | [] | list-extension(U62) | = | Lex | ||
prec(a__U52#) | = | 0 | status(a__U52#) | = | [] | list-extension(a__U52#) | = | Lex | ||
prec(a__sel#) | = | 0 | status(a__sel#) | = | [] | list-extension(a__sel#) | = | Lex | ||
prec(a__U72) | = | 6 | status(a__U72) | = | [2] | list-extension(a__U72) | = | Lex | ||
prec(a__U11) | = | 8 | status(a__U11) | = | [] | list-extension(a__U11) | = | Lex | ||
prec(U32) | = | 2 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(a__sel) | = | 7 | status(a__sel) | = | [2, 1] | list-extension(a__sel) | = | Lex | ||
prec(a__U42) | = | 1 | status(a__U42) | = | [] | list-extension(a__U42) | = | Lex | ||
prec(a__U52) | = | 5 | status(a__U52) | = | [2, 1] | list-extension(a__U52) | = | Lex | ||
prec(a__U12) | = | 7 | status(a__U12) | = | [2, 3] | list-extension(a__U12) | = | Lex | ||
prec(a__U63#) | = | 5 | status(a__U63#) | = | [1, 2] | list-extension(a__U63#) | = | Lex | ||
prec(U52) | = | 5 | status(U52) | = | [2, 1] | list-extension(U52) | = | Lex | ||
prec(U61) | = | 6 | status(U61) | = | [] | list-extension(U61) | = | Lex | ||
prec(a__U22#) | = | 0 | status(a__U22#) | = | [2, 1] | list-extension(a__U22#) | = | Lex | ||
prec(U31) | = | 2 | status(U31) | = | [2] | list-extension(U31) | = | Lex | ||
prec(a__U71) | = | 7 | status(a__U71) | = | [] | list-extension(a__U71) | = | Lex | ||
prec(head) | = | 0 | status(head) | = | [1] | list-extension(head) | = | Lex | ||
prec(a__afterNth#) | = | 0 | status(a__afterNth#) | = | [] | list-extension(a__afterNth#) | = | Lex | ||
prec(a__splitAt#) | = | 4 | status(a__splitAt#) | = | [1] | list-extension(a__splitAt#) | = | Lex | ||
prec(cons) | = | 4 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(a__U61) | = | 6 | status(a__U61) | = | [] | list-extension(a__U61) | = | Lex | ||
prec(snd) | = | 7 | status(snd) | = | [] | list-extension(snd) | = | Lex | ||
prec(a__take) | = | 7 | status(a__take) | = | [] | list-extension(a__take) | = | Lex | ||
prec(U81) | = | 6 | status(U81) | = | [] | list-extension(U81) | = | Lex | ||
prec(a__U41#) | = | 0 | status(a__U41#) | = | [2, 3, 1] | list-extension(a__U41#) | = | Lex | ||
prec(U82) | = | 6 | status(U82) | = | [] | list-extension(U82) | = | Lex | ||
prec(tt) | = | 3 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(a__fst#) | = | 0 | status(a__fst#) | = | [] | list-extension(a__fst#) | = | Lex | ||
prec(U22) | = | 1 | status(U22) | = | [] | list-extension(U22) | = | Lex | ||
prec(U51) | = | 7 | status(U51) | = | [] | list-extension(U51) | = | Lex | ||
prec(a__tail) | = | 7 | status(a__tail) | = | [] | list-extension(a__tail) | = | Lex | ||
prec(U41) | = | 2 | status(U41) | = | [2] | list-extension(U41) | = | Lex | ||
prec(a__tail#) | = | 0 | status(a__tail#) | = | [] | list-extension(a__tail#) | = | Lex | ||
prec(a__U32#) | = | 0 | status(a__U32#) | = | [1, 2] | list-extension(a__U32#) | = | Lex | ||
prec(a__head) | = | 0 | status(a__head) | = | [1] | list-extension(a__head) | = | Lex |
[a__U63(x1,...,x4)] | = | max(x1 + 44589, x2 + 44589, x3 + 44581, x4 + 44586, 0) |
[U21(x1, x2)] | = | x2 + 22290 |
[a__U82#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U72#(x1, x2)] | = | x1 + 1 |
[U11(x1, x2, x3)] | = | x2 + x3 + 48041 |
[U64(x1, x2)] | = | max(x1 + 0, x2 + 44581, 0) |
[s(x1)] | = | x1 + 0 |
[a__head#(x1)] | = | 1 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | x1 + x2 + 48042 |
[U42(x1, x2, x3)] | = | x2 + x3 + 62799 |
[a__U82(x1, x2, x3)] | = | x2 + x3 + 44590 |
[take(x1, x2)] | = | x1 + x2 + 44592 |
[U71(x1, x2)] | = | x2 + 13436 |
[a__U62(x1,...,x4)] | = | max(x1 + 44585, x2 + 44589, x3 + 44582, x4 + 44586, 0) |
[pair(x1, x2)] | = | max(x1 + 22290, x2 + 18842, 0) |
[natsFrom(x1)] | = | x1 + 22292 |
[a__snd(x1)] | = | x1 + 3450 |
[a__U51#(x1, x2)] | = | x1 + 1 |
[U63(x1,...,x4)] | = | max(x1 + 44589, x2 + 44589, x3 + 44581, x4 + 44586, 0) |
[a__U22(x1, x2)] | = | x2 + 3916 |
[splitAt(x1, x2)] | = | max(x1 + 44589, x2 + 44586, 0) |
[a__U64(x1, x2)] | = | max(x1 + 0, x2 + 44581, 0) |
[U72(x1, x2)] | = | x2 + 13435 |
[a__U11#(x1, x2, x3)] | = | x1 + 1 |
[a__U31(x1, x2)] | = | x2 + 14757 |
[a__U51(x1, x2)] | = | x1 + x2 + 22291 |
[a__U81(x1, x2, x3)] | = | x2 + x3 + 44591 |
[a__take#(x1, x2)] | = | x1 + x2 + 0 |
[U12(x1, x2, x3)] | = | x2 + x3 + 48040 |
[a__U62#(x1,...,x4)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U41(x1, x2, x3)] | = | x2 + x3 + 62800 |
[a__U64#(x1, x2)] | = | max(x1 + 1, 0) |
[a__U12#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U21#(x1, x2)] | = | x1 + x2 + 1 |
[a__U81#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U61#(x1,...,x4)] | = | max(x1 + 0, x2 + 0, 0) |
[a__natsFrom(x1)] | = | x1 + 22292 |
[tail(x1)] | = | x1 + 13437 |
[mark#(x1)] | = | 1 |
[0] | = | 18841 |
[a__U21(x1, x2)] | = | x2 + 22290 |
[a__U32(x1, x2)] | = | x1 + x2 + 14757 |
[sel(x1, x2)] | = | x1 + x2 + 62801 |
[afterNth(x1, x2)] | = | x1 + x2 + 48042 |
[nil] | = | 0 |
[a__splitAt(x1, x2)] | = | max(x1 + 44589, x2 + 44586, 0) |
[U62(x1,...,x4)] | = | max(x1 + 44585, x2 + 44589, x3 + 44582, x4 + 44586, 0) |
[a__U52#(x1, x2)] | = | 1 |
[a__sel#(x1, x2)] | = | 1 |
[a__U72(x1, x2)] | = | x2 + 13435 |
[a__U11(x1, x2, x3)] | = | x2 + x3 + 48041 |
[U32(x1, x2)] | = | x1 + x2 + 14757 |
[a__sel(x1, x2)] | = | x1 + x2 + 62801 |
[a__U42(x1, x2, x3)] | = | x2 + x3 + 62799 |
[a__U52(x1, x2)] | = | x1 + x2 + 1 |
[a__U12(x1, x2, x3)] | = | x2 + x3 + 48040 |
[a__U63#(x1,...,x4)] | = | max(x1 + 0, x2 + 0, 0) |
[U52(x1, x2)] | = | x1 + x2 + 1 |
[U61(x1,...,x4)] | = | max(x1 + 44583, x2 + 44589, x3 + 44584, x4 + 44586, 0) |
[a__U22#(x1, x2)] | = | x1 + x2 + 1 |
[U31(x1, x2)] | = | x2 + 14757 |
[a__U71(x1, x2)] | = | x2 + 13436 |
[head(x1)] | = | x1 + 14756 |
[a__afterNth#(x1, x2)] | = | x2 + 0 |
[a__splitAt#(x1, x2)] | = | max(x1 + 0, 0) |
[cons(x1, x2)] | = | max(x1 + 22291, x2 + 0, 0) |
[a__U61(x1,...,x4)] | = | max(x1 + 44583, x2 + 44589, x3 + 44584, x4 + 44586, 0) |
[snd(x1)] | = | x1 + 3450 |
[a__take(x1, x2)] | = | x1 + x2 + 44592 |
[U81(x1, x2, x3)] | = | x2 + x3 + 44591 |
[a__U41#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[U82(x1, x2, x3)] | = | x2 + x3 + 44590 |
[tt] | = | 0 |
[a__fst#(x1)] | = | 1 |
[U22(x1, x2)] | = | x2 + 3916 |
[U51(x1, x2)] | = | x1 + x2 + 22291 |
[a__tail(x1)] | = | x1 + 13437 |
[U41(x1, x2, x3)] | = | x2 + x3 + 62800 |
[a__tail#(x1)] | = | 1 |
[a__U32#(x1, x2)] | = | x1 + x2 + 1 |
[a__head(x1)] | = | x1 + 14756 |
a__U82(tt,N,XS) | → | a__fst(a__splitAt(mark(N),mark(XS))) | (18) |
mark(U82(X1,X2,X3)) | → | a__U82(mark(X1),X2,X3) | (50) |
a__U71(X1,X2) | → | U71(X1,X2) | (80) |
a__U22(tt,X) | → | mark(X) | (4) |
a__U71(tt,XS) | → | a__U72(tt,XS) | (15) |
a__U42(tt,N,XS) | → | a__head(a__afterNth(mark(N),mark(XS))) | (8) |
mark(tail(X)) | → | a__tail(mark(X)) | (54) |
a__U11(tt,N,XS) | → | a__U12(tt,N,XS) | (1) |
a__U62(X1,X2,X3,X4) | → | U62(X1,X2,X3,X4) | (77) |
a__U21(tt,X) | → | a__U22(tt,X) | (3) |
a__U72(tt,XS) | → | mark(XS) | (16) |
a__head(cons(N,XS)) | → | a__U31(tt,N) | (21) |
mark(U32(X1,X2)) | → | a__U32(mark(X1),X2) | (36) |
a__U31(X1,X2) | → | U31(X1,X2) | (68) |
a__natsFrom(X) | → | natsFrom(X) | (85) |
a__splitAt(s(N),cons(X,XS)) | → | a__U61(tt,N,X,XS) | (26) |
a__U12(X1,X2,X3) | → | U12(X1,X2,X3) | (63) |
a__afterNth(N,XS) | → | a__U11(tt,N,XS) | (19) |
mark(splitAt(X1,X2)) | → | a__splitAt(mark(X1),mark(X2)) | (32) |
a__U81(tt,N,XS) | → | a__U82(tt,N,XS) | (17) |
mark(0) | → | 0 | (60) |
a__tail(cons(N,XS)) | → | a__U71(tt,XS) | (27) |
a__tail(X) | → | tail(X) | (87) |
a__fst(X) | → | fst(X) | (84) |
mark(U22(X1,X2)) | → | a__U22(mark(X1),X2) | (34) |
a__natsFrom(N) | → | cons(mark(N),natsFrom(s(N))) | (22) |
a__take(N,XS) | → | a__U81(tt,N,XS) | (28) |
a__splitAt(X1,X2) | → | splitAt(X1,X2) | (65) |
mark(U62(X1,X2,X3,X4)) | → | a__U62(mark(X1),X2,X3,X4) | (44) |
a__U31(tt,N) | → | a__U32(tt,N) | (5) |
a__head(X) | → | head(X) | (72) |
mark(U21(X1,X2)) | → | a__U21(mark(X1),X2) | (33) |
a__snd(X) | → | snd(X) | (64) |
a__U52(tt,Y) | → | mark(Y) | (10) |
mark(head(X)) | → | a__head(mark(X)) | (39) |
a__U41(tt,N,XS) | → | a__U42(tt,N,XS) | (7) |
a__take(X1,X2) | → | take(X1,X2) | (88) |
a__fst(pair(X,Y)) | → | a__U21(tt,X) | (20) |
a__splitAt(0,XS) | → | pair(nil,mark(XS)) | (25) |
mark(U81(X1,X2,X3)) | → | a__U81(mark(X1),X2,X3) | (49) |
mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | (52) |
mark(U12(X1,X2,X3)) | → | a__U12(mark(X1),X2,X3) | (30) |
a__U11(X1,X2,X3) | → | U11(X1,X2,X3) | (62) |
a__U64(pair(YS,ZS),X) | → | pair(cons(mark(X),YS),mark(ZS)) | (14) |
a__U81(X1,X2,X3) | → | U81(X1,X2,X3) | (82) |
mark(tt) | → | tt | (56) |
a__U64(X1,X2) | → | U64(X1,X2) | (79) |
mark(snd(X)) | → | a__snd(mark(X)) | (31) |
a__U62(tt,N,X,XS) | → | a__U63(tt,N,X,XS) | (12) |
a__U32(X1,X2) | → | U32(X1,X2) | (69) |
mark(U63(X1,X2,X3,X4)) | → | a__U63(mark(X1),X2,X3,X4) | (45) |
a__U63(X1,X2,X3,X4) | → | U63(X1,X2,X3,X4) | (78) |
a__U72(X1,X2) | → | U72(X1,X2) | (81) |
a__sel(N,XS) | → | a__U41(tt,N,XS) | (23) |
a__U41(X1,X2,X3) | → | U41(X1,X2,X3) | (70) |
a__snd(pair(X,Y)) | → | a__U51(tt,Y) | (24) |
a__U61(X1,X2,X3,X4) | → | U61(X1,X2,X3,X4) | (76) |
mark(pair(X1,X2)) | → | pair(mark(X1),mark(X2)) | (57) |
a__U61(tt,N,X,XS) | → | a__U62(tt,N,X,XS) | (11) |
a__U51(tt,Y) | → | a__U52(tt,Y) | (9) |
a__U63(tt,N,X,XS) | → | a__U64(a__splitAt(mark(N),mark(XS)),X) | (13) |
mark(fst(X)) | → | a__fst(mark(X)) | (51) |
mark(afterNth(X1,X2)) | → | a__afterNth(mark(X1),mark(X2)) | (40) |
a__U22(X1,X2) | → | U22(X1,X2) | (67) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (55) |
mark(s(X)) | → | s(mark(X)) | (59) |
a__U32(tt,N) | → | mark(N) | (6) |
mark(U42(X1,X2,X3)) | → | a__U42(mark(X1),X2,X3) | (38) |
mark(nil) | → | nil | (61) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (58) |
a__U51(X1,X2) | → | U51(X1,X2) | (74) |
a__U52(X1,X2) | → | U52(X1,X2) | (75) |
mark(U72(X1,X2)) | → | a__U72(mark(X1),X2) | (48) |
a__U42(X1,X2,X3) | → | U42(X1,X2,X3) | (71) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (53) |
mark(U71(X1,X2)) | → | a__U71(mark(X1),X2) | (47) |
a__afterNth(X1,X2) | → | afterNth(X1,X2) | (73) |
mark(U41(X1,X2,X3)) | → | a__U41(mark(X1),X2,X3) | (37) |
mark(U51(X1,X2)) | → | a__U51(mark(X1),X2) | (41) |
mark(U52(X1,X2)) | → | a__U52(mark(X1),X2) | (42) |
mark(U64(X1,X2)) | → | a__U64(mark(X1),X2) | (46) |
a__U21(X1,X2) | → | U21(X1,X2) | (66) |
a__U82(X1,X2,X3) | → | U82(X1,X2,X3) | (83) |
mark(U31(X1,X2)) | → | a__U31(mark(X1),X2) | (35) |
mark(U11(X1,X2,X3)) | → | a__U11(mark(X1),X2,X3) | (29) |
mark(U61(X1,X2,X3,X4)) | → | a__U61(mark(X1),X2,X3,X4) | (43) |
a__sel(X1,X2) | → | sel(X1,X2) | (86) |
a__U12(tt,N,XS) | → | a__snd(a__splitAt(mark(N),mark(XS))) | (2) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U61#(tt,N,X,XS) | (94) |
a__U63#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (118) |
The dependency pairs are split into 0 components.
mark#(s(X)) | → | mark#(X) | (145) |
mark#(cons(X1,X2)) | → | mark#(X1) | (173) |
mark#(U64(X1,X2)) | → | mark#(X1) | (137) |
[a__U63(x1,...,x4)] | = | x1 + x4 + 3762 |
[U21(x1, x2)] | = | x2 + 1 |
[a__U82#(x1, x2, x3)] | = | 0 |
[a__U72#(x1, x2)] | = | 0 |
[a__U71#(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 1210 |
[U64(x1, x2)] | = | x1 + 1512 |
[s(x1)] | = | x1 + 1 |
[a__U31#(x1, x2)] | = | 0 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 0 |
[a__snd#(x1)] | = | 0 |
[a__afterNth(x1, x2)] | = | x1 + x2 + 0 |
[U42(x1, x2, x3)] | = | x3 + 2248 |
[a__U82(x1, x2, x3)] | = | x2 + x3 + 3136 |
[take(x1, x2)] | = | 3 |
[U71(x1, x2)] | = | x2 + 53433 |
[a__U62(x1,...,x4)] | = | x1 + x3 + 3761 |
[pair(x1, x2)] | = | x1 + x2 + 1 |
[fst(x1)] | = | 23202 |
[natsFrom(x1)] | = | x1 + 27018 |
[a__snd(x1)] | = | x1 + 1162 |
[a__U51#(x1, x2)] | = | 0 |
[U63(x1,...,x4)] | = | x3 + x4 + 3761 |
[a__U22(x1, x2)] | = | x1 + 3 |
[splitAt(x1, x2)] | = | x1 + 887 |
[a__U64(x1, x2)] | = | x2 + 3764 |
[U72(x1, x2)] | = | x1 + x2 + 28312 |
[a__U11#(x1, x2, x3)] | = | 0 |
[a__U31(x1, x2)] | = | 2249 |
[a__U51(x1, x2)] | = | x1 + 1163 |
[a__U81(x1, x2, x3)] | = | 3135 |
[a__take#(x1, x2)] | = | 0 |
[U12(x1, x2, x3)] | = | 1214 |
[a__U62#(x1,...,x4)] | = | 4 |
[a__U42#(x1, x2, x3)] | = | 0 |
[a__U41(x1, x2, x3)] | = | x2 + 2246 |
[a__U64#(x1, x2)] | = | 0 |
[a__U12#(x1, x2, x3)] | = | 0 |
[a__U21#(x1, x2)] | = | 0 |
[a__U81#(x1, x2, x3)] | = | 0 |
[a__U61#(x1,...,x4)] | = | 4 |
[a__fst(x1)] | = | x1 + 0 |
[a__natsFrom(x1)] | = | x1 + 27019 |
[tail(x1)] | = | x1 + 51179 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1373 |
[a__U21(x1, x2)] | = | x1 + 2 |
[a__U32(x1, x2)] | = | x1 + 2249 |
[sel(x1, x2)] | = | 2246 |
[afterNth(x1, x2)] | = | 147 |
[nil] | = | 25477 |
[a__splitAt(x1, x2)] | = | x2 + 886 |
[U62(x1,...,x4)] | = | x2 + x4 + 1898 |
[a__U52#(x1, x2)] | = | 0 |
[a__sel#(x1, x2)] | = | 0 |
[mark(x1)] | = | x1 + 2251 |
[a__U72(x1, x2)] | = | 53433 |
[a__U11(x1, x2, x3)] | = | x1 + x3 + 1211 |
[U32(x1, x2)] | = | x2 + 2250 |
[a__sel(x1, x2)] | = | x1 + x2 + 2245 |
[a__U42(x1, x2, x3)] | = | x2 + 2247 |
[a__U52(x1, x2)] | = | x1 + x2 + 2150 |
[a__U12(x1, x2, x3)] | = | x2 + 1213 |
[a__U63#(x1,...,x4)] | = | 4 |
[U52(x1, x2)] | = | x2 + 2149 |
[U61(x1,...,x4)] | = | x1 + x3 + x4 + 1509 |
[a__U22#(x1, x2)] | = | 0 |
[U31(x1, x2)] | = | x1 + 2250 |
[a__U71(x1, x2)] | = | 53432 |
[head(x1)] | = | x1 + 2249 |
[a__afterNth#(x1, x2)] | = | 0 |
[a__splitAt#(x1, x2)] | = | 2 |
[cons(x1, x2)] | = | x1 + x2 + 1047 |
[a__U61(x1,...,x4)] | = | x2 + 3761 |
[snd(x1)] | = | 1161 |
[a__take(x1, x2)] | = | x1 + x2 + 0 |
[U81(x1, x2, x3)] | = | x1 + 883 |
[a__U41#(x1, x2, x3)] | = | 0 |
[U82(x1, x2, x3)] | = | x1 + 3137 |
[tt] | = | 1 |
[a__fst#(x1)] | = | 0 |
[U22(x1, x2)] | = | x2 + 2 |
[U51(x1, x2)] | = | 1162 |
[a__tail(x1)] | = | 53431 |
[U41(x1, x2, x3)] | = | x3 + 2247 |
[a__tail#(x1)] | = | 0 |
[a__U32#(x1, x2)] | = | 0 |
[a__head(x1)] | = | 2248 |
mark#(s(X)) | → | mark#(X) | (145) |
mark#(cons(X1,X2)) | → | mark#(X1) | (173) |
mark#(U64(X1,X2)) | → | mark#(X1) | (137) |
The dependency pairs are split into 0 components.