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.540 CpxTRS8.18/2.54
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))8.18/2.54
↳2 CdtProblem8.18/2.54
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))8.18/2.54
↳4 CdtProblem8.18/2.54
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))8.18/2.54
↳6 CdtProblem8.18/2.54
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)8.18/2.54
↳8 CdtProblem8.18/2.54
↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))8.18/2.54
↳10 CdtProblem8.18/2.54
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))8.18/2.54
↳12 CdtProblem8.18/2.54
↳13 CdtKnowledgeProof (⇔)8.18/2.54
↳14 BOUNDS(O(1), O(1))8.18/2.54
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
Tuples:
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
S 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))
K tuples:none
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))
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
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
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
Tuples:
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
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
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
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
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
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
Tuples:
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
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
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))
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
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
c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c23, c24, c26, c28, c29, c21
Removed 34 trailing nodes:
TAKE(z0, z1) → c28(U81'(tt, z0, z1)) 8.18/2.59
SEL(z0, z1) → c23(U41'(tt, z0, z1))
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))
Tuples:
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
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
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)))
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
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
c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c24, c26, c29, c21
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))
Tuples:
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
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:
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
Defined Rule Symbols:
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))
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
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
c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c24, c26, c29, c21
We considered the (Usable) Rules:
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))
And the Tuples:
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)
The order we found is given by the following interpretation:
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)))
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]
Tuples:
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
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:
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
Defined Rule Symbols:
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))
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
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
c3, c5, c9, c10, c11, c12, c13, c15, c18, c19, c20, c24, c26, c29, c21
Now S is empty
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