YES(O(1), O(n^1)) 7.02/2.25 YES(O(1), O(n^1)) 8.18/2.54 8.18/2.54 8.18/2.54 8.18/2.54 8.18/2.54 8.18/2.54 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 8.18/2.54 8.18/2.54 8.18/2.54
8.18/2.54 8.18/2.54 8.18/2.54
8.18/2.54
8.18/2.55

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, activate(N), activate(XS)) 8.18/2.55
U12(tt, N, XS) → snd(splitAt(activate(N), activate(XS))) 8.18/2.55
U21(tt, X) → U22(tt, activate(X)) 8.18/2.55
U22(tt, X) → activate(X) 8.18/2.55
U31(tt, N) → U32(tt, activate(N)) 8.18/2.55
U32(tt, N) → activate(N) 8.18/2.55
U41(tt, N, XS) → U42(tt, activate(N), activate(XS)) 8.18/2.55
U42(tt, N, XS) → head(afterNth(activate(N), activate(XS))) 8.18/2.55
U51(tt, Y) → U52(tt, activate(Y)) 8.18/2.55
U52(tt, Y) → activate(Y) 8.18/2.55
U61(tt, N, X, XS) → U62(tt, activate(N), activate(X), activate(XS)) 8.18/2.55
U62(tt, N, X, XS) → U63(tt, activate(N), activate(X), activate(XS)) 8.18/2.55
U63(tt, N, X, XS) → U64(splitAt(activate(N), activate(XS)), activate(X)) 8.18/2.55
U64(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS) 8.18/2.55
U71(tt, XS) → U72(tt, activate(XS)) 8.18/2.55
U72(tt, XS) → activate(XS) 8.18/2.55
U81(tt, N, XS) → U82(tt, activate(N), activate(XS)) 8.18/2.55
U82(tt, N, XS) → fst(splitAt(activate(N), activate(XS))) 8.18/2.55
afterNth(N, XS) → U11(tt, N, XS) 8.18/2.55
fst(pair(X, Y)) → U21(tt, X) 8.18/2.55
head(cons(N, XS)) → U31(tt, N) 8.18/2.55
natsFrom(N) → cons(N, n__natsFrom(s(N))) 8.18/2.55
sel(N, XS) → U41(tt, N, XS) 8.18/2.55
snd(pair(X, Y)) → U51(tt, Y) 8.18/2.55
splitAt(0, XS) → pair(nil, XS) 8.18/2.55
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, activate(XS)) 8.18/2.55
tail(cons(N, XS)) → U71(tt, activate(XS)) 8.18/2.55
take(N, XS) → U81(tt, N, XS) 8.18/2.55
natsFrom(X) → n__natsFrom(X) 8.18/2.55
activate(n__natsFrom(X)) → natsFrom(X) 8.18/2.55
activate(X) → X

Rewrite Strategy: INNERMOST
8.18/2.55
8.18/2.55

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
8.18/2.55
8.18/2.55

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.55
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.55
U21(tt, z0) → U22(tt, activate(z0)) 8.18/2.55
U22(tt, z0) → activate(z0) 8.18/2.55
U31(tt, z0) → U32(tt, activate(z0)) 8.18/2.55
U32(tt, z0) → activate(z0) 8.18/2.55
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1)) 8.18/2.55
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1))) 8.18/2.55
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.55
U52(tt, z0) → activate(z0) 8.18/2.55
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.55
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.55
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.55
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.55
U71(tt, z0) → U72(tt, activate(z0)) 8.18/2.55
U72(tt, z0) → activate(z0) 8.18/2.55
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1)) 8.18/2.55
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1))) 8.18/2.55
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.55
fst(pair(z0, z1)) → U21(tt, z0) 8.18/2.55
head(cons(z0, z1)) → U31(tt, z0) 8.18/2.55
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.55
natsFrom(z0) → n__natsFrom(z0) 8.18/2.55
sel(z0, z1) → U41(tt, z0, z1) 8.18/2.55
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.55
splitAt(0, z0) → pair(nil, z0) 8.18/2.55
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.55
tail(cons(z0, z1)) → U71(tt, activate(z1)) 8.18/2.55
take(z0, z1) → U81(tt, z0, z1) 8.18/2.55
activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.55
activate(z0) → z0
Tuples:

U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.55
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.55
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.55
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.55
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.55
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.55
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.55
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.55
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.55
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.55
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.55
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.55
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.55
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.55
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.55
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.55
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.55
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.55
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.55
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.55
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.55
SEL(z0, z1) → c23(U41'(tt, z0, z1)) 8.18/2.55
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.55
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.55
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1)) 8.18/2.55
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.55
ACTIVATE(n__natsFrom(z0)) → c29(NATSFROM(z0))
S tuples:

U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1)) 8.18/2.59
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29(NATSFROM(z0))
K tuples:none
Defined Rule Symbols:

U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate

Defined Pair Symbols:

U11', U12', U21', U22', U31', U32', U41', U42', U51', U52', U61', U62', U63', U64', U71', U72', U81', U82', AFTERNTH, FST, HEAD, SEL, SND, SPLITAT, TAIL, TAKE, ACTIVATE

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c23, c24, c26, c27, c28, c29

8.18/2.59
8.18/2.59

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
8.18/2.59
8.18/2.59

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.59
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.59
U21(tt, z0) → U22(tt, activate(z0)) 8.18/2.59
U22(tt, z0) → activate(z0) 8.18/2.59
U31(tt, z0) → U32(tt, activate(z0)) 8.18/2.59
U32(tt, z0) → activate(z0) 8.18/2.59
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1)) 8.18/2.59
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1))) 8.18/2.59
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.59
U52(tt, z0) → activate(z0) 8.18/2.59
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.59
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.59
U71(tt, z0) → U72(tt, activate(z0)) 8.18/2.59
U72(tt, z0) → activate(z0) 8.18/2.59
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1)) 8.18/2.59
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1))) 8.18/2.59
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.59
fst(pair(z0, z1)) → U21(tt, z0) 8.18/2.59
head(cons(z0, z1)) → U31(tt, z0) 8.18/2.59
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.59
natsFrom(z0) → n__natsFrom(z0) 8.18/2.59
sel(z0, z1) → U41(tt, z0, z1) 8.18/2.59
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.59
splitAt(0, z0) → pair(nil, z0) 8.18/2.59
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.59
tail(cons(z0, z1)) → U71(tt, activate(z1)) 8.18/2.59
take(z0, z1) → U81(tt, z0, z1) 8.18/2.59
activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.59
activate(z0) → z0
Tuples:

U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1)) 8.18/2.59
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29
S tuples:

U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1)) 8.18/2.59
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29
K tuples:none
Defined Rule Symbols:

U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate

Defined Pair Symbols:

U11', U12', U21', U22', U31', U32', U41', U42', U51', U52', U61', U62', U63', U64', U71', U72', U81', U82', AFTERNTH, FST, HEAD, SEL, SND, SPLITAT, TAIL, TAKE, ACTIVATE

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c23, c24, c26, c27, c28, c29

8.18/2.59
8.18/2.59

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC
8.18/2.59
8.18/2.59

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.59
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.59
U21(tt, z0) → U22(tt, activate(z0)) 8.18/2.59
U22(tt, z0) → activate(z0) 8.18/2.59
U31(tt, z0) → U32(tt, activate(z0)) 8.18/2.59
U32(tt, z0) → activate(z0) 8.18/2.59
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1)) 8.18/2.59
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1))) 8.18/2.59
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.59
U52(tt, z0) → activate(z0) 8.18/2.59
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.59
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.59
U71(tt, z0) → U72(tt, activate(z0)) 8.18/2.59
U72(tt, z0) → activate(z0) 8.18/2.59
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1)) 8.18/2.59
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1))) 8.18/2.59
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.59
fst(pair(z0, z1)) → U21(tt, z0) 8.18/2.59
head(cons(z0, z1)) → U31(tt, z0) 8.18/2.59
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.59
natsFrom(z0) → n__natsFrom(z0) 8.18/2.59
sel(z0, z1) → U41(tt, z0, z1) 8.18/2.59
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.59
splitAt(0, z0) → pair(nil, z0) 8.18/2.59
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.59
tail(cons(z0, z1)) → U71(tt, activate(z1)) 8.18/2.59
take(z0, z1) → U81(tt, z0, z1) 8.18/2.59
activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.59
activate(z0) → z0
Tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U41'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U81'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1))) 8.18/2.59
TAIL(cons(z0, z1)) → c21(ACTIVATE(z1))
S tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U41'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U81'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1))) 8.18/2.59
TAIL(cons(z0, z1)) → c21(ACTIVATE(z1))
K tuples:none
Defined Rule Symbols:

U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate

Defined Pair Symbols:

U22', U32', U52', U61', U62', U63', U64', U72', AFTERNTH, FST, HEAD, SEL, SND, SPLITAT, TAKE, ACTIVATE, U11', U12', U21', U31', U41', U42', U51', U71', U81', U82', TAIL

Compound Symbols:

c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c23, c24, c26, c28, c29, c21

8.18/2.59
8.18/2.59

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1))
Removed 34 trailing nodes:

U41'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U81'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U81'(tt, z0, z1) → c21(ACTIVATE(z1))
8.18/2.59
8.18/2.59

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.59
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.59
U21(tt, z0) → U22(tt, activate(z0)) 8.18/2.59
U22(tt, z0) → activate(z0) 8.18/2.59
U31(tt, z0) → U32(tt, activate(z0)) 8.18/2.59
U32(tt, z0) → activate(z0) 8.18/2.59
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1)) 8.18/2.59
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1))) 8.18/2.59
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.59
U52(tt, z0) → activate(z0) 8.18/2.59
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.59
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.59
U71(tt, z0) → U72(tt, activate(z0)) 8.18/2.59
U72(tt, z0) → activate(z0) 8.18/2.59
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1)) 8.18/2.59
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1))) 8.18/2.59
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.59
fst(pair(z0, z1)) → U21(tt, z0) 8.18/2.59
head(cons(z0, z1)) → U31(tt, z0) 8.18/2.59
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.59
natsFrom(z0) → n__natsFrom(z0) 8.18/2.59
sel(z0, z1) → U41(tt, z0, z1) 8.18/2.59
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.59
splitAt(0, z0) → pair(nil, z0) 8.18/2.59
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.59
tail(cons(z0, z1)) → U71(tt, activate(z1)) 8.18/2.59
take(z0, z1) → U81(tt, z0, z1) 8.18/2.59
activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.59
activate(z0) → z0
Tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1)))
S tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1)))
K tuples:none
Defined Rule Symbols:

U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate

Defined Pair Symbols:

U22', U32', U52', U61', U62', U63', U64', U72', AFTERNTH, FST, HEAD, SND, SPLITAT, ACTIVATE, U11', U12', U21', U31', U41', U42', U51', U71', U81', U82', TAIL

Compound Symbols:

c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c24, c26, c29, c21

8.18/2.59
8.18/2.59

(9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0))
8.18/2.59
8.18/2.59

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.59
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.59
U21(tt, z0) → U22(tt, activate(z0)) 8.18/2.59
U22(tt, z0) → activate(z0) 8.18/2.59
U31(tt, z0) → U32(tt, activate(z0)) 8.18/2.59
U32(tt, z0) → activate(z0) 8.18/2.59
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1)) 8.18/2.59
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1))) 8.18/2.59
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.59
U52(tt, z0) → activate(z0) 8.18/2.59
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.59
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.59
U71(tt, z0) → U72(tt, activate(z0)) 8.18/2.59
U72(tt, z0) → activate(z0) 8.18/2.59
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1)) 8.18/2.59
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1))) 8.18/2.59
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.59
fst(pair(z0, z1)) → U21(tt, z0) 8.18/2.59
head(cons(z0, z1)) → U31(tt, z0) 8.18/2.59
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.59
natsFrom(z0) → n__natsFrom(z0) 8.18/2.59
sel(z0, z1) → U41(tt, z0, z1) 8.18/2.59
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.59
splitAt(0, z0) → pair(nil, z0) 8.18/2.59
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.59
tail(cons(z0, z1)) → U71(tt, activate(z1)) 8.18/2.59
take(z0, z1) → U81(tt, z0, z1) 8.18/2.59
activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.59
activate(z0) → z0
Tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1)))
S tuples:

U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29
K tuples:

U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1))) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0))
Defined Rule Symbols:

U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate

Defined Pair Symbols:

U22', U32', U52', U61', U62', U63', U64', U72', AFTERNTH, FST, HEAD, SND, SPLITAT, ACTIVATE, U11', U12', U21', U31', U41', U42', U51', U71', U81', U82', TAIL

Compound Symbols:

c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c24, c26, c29, c21

8.18/2.59
8.18/2.59

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
We considered the (Usable) Rules:

activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.59
activate(z0) → z0 8.18/2.59
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.59
natsFrom(z0) → n__natsFrom(z0) 8.18/2.59
splitAt(0, z0) → pair(nil, z0) 8.18/2.59
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.59
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.59
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.59
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.59
U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.59
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.59
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.59
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.59
U52(tt, z0) → activate(z0)
And the Tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1)))
The order we found is given by the following interpretation:
Polynomial interpretation : 8.18/2.59

POL(0) = [4]    8.18/2.59
POL(ACTIVATE(x1)) = 0    8.18/2.59
POL(AFTERNTH(x1, x2)) = [2] + [5]x1    8.18/2.59
POL(FST(x1)) = [4] + [3]x1    8.18/2.59
POL(HEAD(x1)) = 0    8.18/2.59
POL(SND(x1)) = x1    8.18/2.59
POL(SPLITAT(x1, x2)) = [4]x1    8.18/2.59
POL(TAIL(x1)) = [1]    8.18/2.59
POL(U11(x1, x2, x3)) = [3] + x1 + [3]x2 + [3]x3    8.18/2.59
POL(U11'(x1, x2, x3)) = [2] + [5]x2    8.18/2.59
POL(U12(x1, x2, x3)) = [3] + x1    8.18/2.59
POL(U12'(x1, x2, x3)) = [2] + [5]x2    8.18/2.59
POL(U21'(x1, x2)) = [2] + x1    8.18/2.59
POL(U22'(x1, x2)) = [4]    8.18/2.59
POL(U31'(x1, x2)) = 0    8.18/2.59
POL(U32'(x1, x2)) = 0    8.18/2.59
POL(U41'(x1, x2, x3)) = [4] + x1 + [5]x2 + [5]x3    8.18/2.59
POL(U42'(x1, x2, x3)) = [2]x1 + [5]x2    8.18/2.59
POL(U51(x1, x2)) = [3] + [3]x1 + [3]x2    8.18/2.59
POL(U51'(x1, x2)) = x1    8.18/2.59
POL(U52(x1, x2)) = [3] + [3]x1 + [3]x2    8.18/2.59
POL(U52'(x1, x2)) = x1    8.18/2.59
POL(U61(x1, x2, x3, x4)) = x1 + x2    8.18/2.59
POL(U61'(x1, x2, x3, x4)) = [4]x1 + [4]x2    8.18/2.59
POL(U62(x1, x2, x3, x4)) = [2] + x2    8.18/2.59
POL(U62'(x1, x2, x3, x4)) = [3] + [3]x1 + [4]x2    8.18/2.59
POL(U63(x1, x2, x3, x4)) = x2    8.18/2.59
POL(U63'(x1, x2, x3, x4)) = [4]x2    8.18/2.59
POL(U64(x1, x2)) = x1    8.18/2.59
POL(U64'(x1, x2)) = 0    8.18/2.59
POL(U71'(x1, x2)) = [1]    8.18/2.59
POL(U72'(x1, x2)) = [1]    8.18/2.59
POL(U81'(x1, x2, x3)) = [4]x1 + [5]x2 + [4]x3    8.18/2.59
POL(U82'(x1, x2, x3)) = [4] + [4]x2    8.18/2.59
POL(activate(x1)) = x1    8.18/2.59
POL(afterNth(x1, x2)) = 0    8.18/2.59
POL(c10(x1, x2, x3, x4)) = x1 + x2 + x3 + x4    8.18/2.59
POL(c11(x1, x2, x3, x4)) = x1 + x2 + x3 + x4    8.18/2.59
POL(c12(x1, x2, x3, x4, x5)) = x1 + x2 + x3 + x4 + x5    8.18/2.59
POL(c13(x1)) = x1    8.18/2.59
POL(c15(x1)) = x1    8.18/2.59
POL(c18(x1)) = x1    8.18/2.59
POL(c19(x1)) = x1    8.18/2.59
POL(c20(x1)) = x1    8.18/2.59
POL(c21(x1)) = x1    8.18/2.59
POL(c24(x1)) = x1    8.18/2.59
POL(c26(x1, x2)) = x1 + x2    8.18/2.59
POL(c29) = 0    8.18/2.59
POL(c3(x1)) = x1    8.18/2.59
POL(c5(x1)) = x1    8.18/2.59
POL(c9(x1)) = x1    8.18/2.59
POL(cons(x1, x2)) = 0    8.18/2.59
POL(n__natsFrom(x1)) = 0    8.18/2.59
POL(natsFrom(x1)) = 0    8.18/2.59
POL(nil) = [3]    8.18/2.59
POL(pair(x1, x2)) = [4]    8.18/2.59
POL(s(x1)) = [4] + x1    8.18/2.59
POL(snd(x1)) = [3]    8.18/2.59
POL(splitAt(x1, x2)) = x1    8.18/2.59
POL(tt) = [4]   
8.18/2.59
8.18/2.59

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1)) 8.18/2.59
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1))) 8.18/2.59
U21(tt, z0) → U22(tt, activate(z0)) 8.18/2.59
U22(tt, z0) → activate(z0) 8.18/2.59
U31(tt, z0) → U32(tt, activate(z0)) 8.18/2.59
U32(tt, z0) → activate(z0) 8.18/2.59
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1)) 8.18/2.59
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1))) 8.18/2.59
U51(tt, z0) → U52(tt, activate(z0)) 8.18/2.59
U52(tt, z0) → activate(z0) 8.18/2.59
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2)) 8.18/2.59
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1)) 8.18/2.59
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1) 8.18/2.59
U71(tt, z0) → U72(tt, activate(z0)) 8.18/2.59
U72(tt, z0) → activate(z0) 8.18/2.59
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1)) 8.18/2.59
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1))) 8.18/2.59
afterNth(z0, z1) → U11(tt, z0, z1) 8.18/2.59
fst(pair(z0, z1)) → U21(tt, z0) 8.18/2.59
head(cons(z0, z1)) → U31(tt, z0) 8.18/2.59
natsFrom(z0) → cons(z0, n__natsFrom(s(z0))) 8.18/2.59
natsFrom(z0) → n__natsFrom(z0) 8.18/2.59
sel(z0, z1) → U41(tt, z0, z1) 8.18/2.59
snd(pair(z0, z1)) → U51(tt, z1) 8.18/2.59
splitAt(0, z0) → pair(nil, z0) 8.18/2.59
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2)) 8.18/2.59
tail(cons(z0, z1)) → U71(tt, activate(z1)) 8.18/2.59
take(z0, z1) → U81(tt, z0, z1) 8.18/2.59
activate(n__natsFrom(z0)) → natsFrom(z0) 8.18/2.59
activate(z0) → z0
Tuples:

U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1)))
S tuples:

U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29
K tuples:

U41'(tt, z0, z1) → c21(U42'(tt, activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(HEAD(afterNth(activate(z0), activate(z1)))) 8.18/2.59
U42'(tt, z0, z1) → c21(AFTERNTH(activate(z0), activate(z1))) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U42'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U81'(tt, z0, z1) → c21(U82'(tt, activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(FST(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U82'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U82'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
TAIL(cons(z0, z1)) → c21(U71'(tt, activate(z1))) 8.18/2.59
HEAD(cons(z0, z1)) → c20(U31'(tt, z0)) 8.18/2.59
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1)) 8.18/2.59
FST(pair(z0, z1)) → c19(U21'(tt, z0)) 8.18/2.59
U71'(tt, z0) → c21(U72'(tt, activate(z0))) 8.18/2.59
U71'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U31'(tt, z0) → c21(U32'(tt, activate(z0))) 8.18/2.59
U31'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(U12'(tt, activate(z0), activate(z1))) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U11'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U21'(tt, z0) → c21(U22'(tt, activate(z0))) 8.18/2.59
U21'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U72'(tt, z0) → c15(ACTIVATE(z0)) 8.18/2.59
U32'(tt, z0) → c5(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(SND(splitAt(activate(z0), activate(z1)))) 8.18/2.59
U12'(tt, z0, z1) → c21(SPLITAT(activate(z0), activate(z1))) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z0)) 8.18/2.59
U12'(tt, z0, z1) → c21(ACTIVATE(z1)) 8.18/2.59
U22'(tt, z0) → c3(ACTIVATE(z0)) 8.18/2.59
SND(pair(z0, z1)) → c24(U51'(tt, z1)) 8.18/2.59
U51'(tt, z0) → c21(U52'(tt, activate(z0))) 8.18/2.59
U51'(tt, z0) → c21(ACTIVATE(z0)) 8.18/2.59
U52'(tt, z0) → c9(ACTIVATE(z0)) 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
Defined Rule Symbols:

U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate

Defined Pair Symbols:

U22', U32', U52', U61', U62', U63', U64', U72', AFTERNTH, FST, HEAD, SND, SPLITAT, ACTIVATE, U11', U12', U21', U31', U41', U42', U51', U71', U81', U82', TAIL

Compound Symbols:

c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c24, c26, c29, c21

8.18/2.59
8.18/2.59

(13) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1)) 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2)) 8.18/2.59
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29 8.18/2.59
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2)) 8.18/2.59
ACTIVATE(n__natsFrom(z0)) → c29
Now S is empty
8.18/2.59
8.18/2.59

(14) BOUNDS(O(1), O(1))

8.18/2.59
8.18/2.59
8.61/2.65 EOF