WORST_CASE(?,O(n^1)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 2091 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 25 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 196 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 95 ms] (18) CdtProblem (19) CdtKnowledgeProof [FINISHED, 0 ms] (20) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 Tuples: U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U12''(tt, z0, z1) -> c44(SND'(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U21''(tt, z0) -> c45(U22''(tt, activate(z0)), ACTIVATE'(z0)) U22''(tt, z0) -> c46(ACTIVATE'(z0)) U31''(tt, z0) -> c47(U32''(tt, activate(z0)), ACTIVATE'(z0)) U32''(tt, z0) -> c48(ACTIVATE'(z0)) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U42''(tt, z0, z1) -> c50(HEAD'(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U51''(tt, z0) -> c51(U52''(tt, activate(z0)), ACTIVATE'(z0)) U52''(tt, z0) -> c52(ACTIVATE'(z0)) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2)) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2)) U63''(tt, z0, z1, z2) -> c55(U64''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1)) U64''(pair(z0, z1), z2) -> c56(ACTIVATE'(z2)) U71''(tt, z0) -> c57(U72''(tt, activate(z0)), ACTIVATE'(z0)) U72''(tt, z0) -> c58(ACTIVATE'(z0)) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U82''(tt, z0, z1) -> c60(FST'(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) FST'(pair(z0, z1)) -> c62(U21''(tt, z0)) HEAD'(cons(z0, z1)) -> c63(U31''(tt, z0)) NATSFROM'(z0) -> c64 NATSFROM'(z0) -> c65 SEL'(z0, z1) -> c66(U41''(tt, z0, z1)) SND'(pair(z0, z1)) -> c67(U51''(tt, z1)) SPLITAT'(0, z0) -> c68 SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2)), ACTIVATE'(z2)) TAIL'(cons(z0, z1)) -> c70(U71''(tt, activate(z1)), ACTIVATE'(z1)) TAKE'(z0, z1) -> c71(U81''(tt, z0, z1)) ACTIVATE'(n__natsFrom(z0)) -> c72(NATSFROM'(z0)) ACTIVATE'(z0) -> c73 U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c76(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U12'''(tt, z0, z1) -> c77(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U21'''(tt, z0) -> c78(U22'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U22'''(tt, z0) -> c79(ACTIVATE''(z0)) U31'''(tt, z0) -> c80(U32'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U32'''(tt, z0) -> c81(ACTIVATE''(z0)) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U42'''(tt, z0, z1) -> c84(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U42'''(tt, z0, z1) -> c85(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U51'''(tt, z0) -> c86(U52'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U52'''(tt, z0) -> c87(ACTIVATE''(z0)) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c94(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z0)) U63'''(tt, z0, z1, z2) -> c95(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c96(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) U64'''(pair(z0, z1), z2) -> c97(ACTIVATE''(z2)) U71'''(tt, z0) -> c98(U72'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U72'''(tt, z0) -> c99(ACTIVATE''(z0)) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U82'''(tt, z0, z1) -> c102(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U82'''(tt, z0, z1) -> c103(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) FST''(pair(z0, z1)) -> c105(U21'''(tt, z0)) HEAD''(cons(z0, z1)) -> c106(U31'''(tt, z0)) NATSFROM''(z0) -> c107 NATSFROM''(z0) -> c108 SEL''(z0, z1) -> c109(U41'''(tt, z0, z1)) SND''(pair(z0, z1)) -> c110(U51'''(tt, z1)) SPLITAT''(0, z0) -> c111 SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) TAIL''(cons(z0, z1)) -> c113(U71'''(tt, activate(z1)), ACTIVATE'(z1), ACTIVATE''(z1)) TAKE''(z0, z1) -> c114(U81'''(tt, z0, z1)) ACTIVATE''(n__natsFrom(z0)) -> c115(NATSFROM''(z0)) ACTIVATE''(z0) -> c116 S tuples: U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c76(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U12'''(tt, z0, z1) -> c77(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U21'''(tt, z0) -> c78(U22'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U22'''(tt, z0) -> c79(ACTIVATE''(z0)) U31'''(tt, z0) -> c80(U32'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U32'''(tt, z0) -> c81(ACTIVATE''(z0)) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U42'''(tt, z0, z1) -> c84(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U42'''(tt, z0, z1) -> c85(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U51'''(tt, z0) -> c86(U52'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U52'''(tt, z0) -> c87(ACTIVATE''(z0)) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c94(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z0)) U63'''(tt, z0, z1, z2) -> c95(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c96(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) U64'''(pair(z0, z1), z2) -> c97(ACTIVATE''(z2)) U71'''(tt, z0) -> c98(U72'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U72'''(tt, z0) -> c99(ACTIVATE''(z0)) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U82'''(tt, z0, z1) -> c102(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U82'''(tt, z0, z1) -> c103(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) FST''(pair(z0, z1)) -> c105(U21'''(tt, z0)) HEAD''(cons(z0, z1)) -> c106(U31'''(tt, z0)) NATSFROM''(z0) -> c107 NATSFROM''(z0) -> c108 SEL''(z0, z1) -> c109(U41'''(tt, z0, z1)) SND''(pair(z0, z1)) -> c110(U51'''(tt, z1)) SPLITAT''(0, z0) -> c111 SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) TAIL''(cons(z0, z1)) -> c113(U71'''(tt, activate(z1)), ACTIVATE'(z1), ACTIVATE''(z1)) TAKE''(z0, z1) -> c114(U81'''(tt, z0, z1)) ACTIVATE''(n__natsFrom(z0)) -> c115(NATSFROM''(z0)) ACTIVATE''(z0) -> c116 K tuples:none Defined Rule Symbols: U11'_3, U12'_3, U21'_2, U22'_2, U31'_2, U32'_2, U41'_3, U42'_3, U51'_2, U52'_2, U61'_4, U62'_4, U63'_4, U64'_2, U71'_2, U72'_2, U81'_3, U82'_3, AFTERNTH_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_3, U12_3, U21_2, U22_2, U31_2, U32_2, U41_3, U42_3, U51_2, U52_2, U61_4, U62_4, U63_4, U64_2, U71_2, U72_2, U81_3, U82_3, afterNth_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_3, U12''_3, U21''_2, U22''_2, U31''_2, U32''_2, U41''_3, U42''_3, U51''_2, U52''_2, U61''_4, U62''_4, U63''_4, U64''_2, U71''_2, U72''_2, U81''_3, U82''_3, AFTERNTH'_2, FST'_1, HEAD'_1, NATSFROM'_1, SEL'_2, SND'_1, SPLITAT'_2, TAIL'_1, TAKE'_2, ACTIVATE'_1, U11'''_3, U12'''_3, U21'''_2, U22'''_2, U31'''_2, U32'''_2, U41'''_3, U42'''_3, U51'''_2, U52'''_2, U61'''_4, U62'''_4, U63'''_4, U64'''_2, U71'''_2, U72'''_2, U81'''_3, U82'''_3, AFTERNTH''_2, FST''_1, HEAD''_1, NATSFROM''_1, SEL''_2, SND''_1, SPLITAT''_2, TAIL''_1, TAKE''_2, ACTIVATE''_1 Compound Symbols: c43_3, c44_4, c45_2, c46_1, c47_2, c48_1, c49_3, c50_4, c51_2, c52_1, c53_4, c54_4, c55_5, c56_1, c57_2, c58_1, c59_3, c60_4, c61_1, c62_1, c63_1, c64, c65, c66_1, c67_1, c68, c69_2, c70_2, c71_1, c72_1, c73, c74_4, c75_4, c76_8, c77_8, c78_3, c79_1, c80_3, c81_1, c82_4, c83_4, c84_8, c85_8, c86_3, c87_1, c88_5, c89_5, c90_5, c91_5, c92_5, c93_5, c94_9, c95_9, c96_6, c97_1, c98_3, c99_1, c100_4, c101_4, c102_8, c103_8, c104_1, c105_1, c106_1, c107, c108, c109_1, c110_1, c111, c112_3, c113_3, c114_1, c115_1, c116 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 4 leading nodes: SEL'(z0, z1) -> c66(U41''(tt, z0, z1)) SEL''(z0, z1) -> c109(U41'''(tt, z0, z1)) TAKE'(z0, z1) -> c71(U81''(tt, z0, z1)) TAKE''(z0, z1) -> c114(U81'''(tt, z0, z1)) Removed 36 trailing nodes: U71''(tt, z0) -> c57(U72''(tt, activate(z0)), ACTIVATE'(z0)) U22'''(tt, z0) -> c79(ACTIVATE''(z0)) TAIL'(cons(z0, z1)) -> c70(U71''(tt, activate(z1)), ACTIVATE'(z1)) ACTIVATE''(z0) -> c116 NATSFROM''(z0) -> c107 HEAD''(cons(z0, z1)) -> c106(U31'''(tt, z0)) SPLITAT''(0, z0) -> c111 U31''(tt, z0) -> c47(U32''(tt, activate(z0)), ACTIVATE'(z0)) U51''(tt, z0) -> c51(U52''(tt, activate(z0)), ACTIVATE'(z0)) U31'''(tt, z0) -> c80(U32'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U32'''(tt, z0) -> c81(ACTIVATE''(z0)) SPLITAT'(0, z0) -> c68 U72'''(tt, z0) -> c99(ACTIVATE''(z0)) ACTIVATE'(z0) -> c73 ACTIVATE''(n__natsFrom(z0)) -> c115(NATSFROM''(z0)) U72''(tt, z0) -> c58(ACTIVATE'(z0)) U52'''(tt, z0) -> c87(ACTIVATE''(z0)) TAIL''(cons(z0, z1)) -> c113(U71'''(tt, activate(z1)), ACTIVATE'(z1), ACTIVATE''(z1)) U21''(tt, z0) -> c45(U22''(tt, activate(z0)), ACTIVATE'(z0)) U71'''(tt, z0) -> c98(U72'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U64''(pair(z0, z1), z2) -> c56(ACTIVATE'(z2)) FST'(pair(z0, z1)) -> c62(U21''(tt, z0)) ACTIVATE'(n__natsFrom(z0)) -> c72(NATSFROM'(z0)) U32''(tt, z0) -> c48(ACTIVATE'(z0)) SND''(pair(z0, z1)) -> c110(U51'''(tt, z1)) SND'(pair(z0, z1)) -> c67(U51''(tt, z1)) U22''(tt, z0) -> c46(ACTIVATE'(z0)) NATSFROM'(z0) -> c65 U51'''(tt, z0) -> c86(U52'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) U21'''(tt, z0) -> c78(U22'''(tt, activate(z0)), ACTIVATE'(z0), ACTIVATE''(z0)) FST''(pair(z0, z1)) -> c105(U21'''(tt, z0)) U52''(tt, z0) -> c52(ACTIVATE'(z0)) NATSFROM'(z0) -> c64 NATSFROM''(z0) -> c108 U64'''(pair(z0, z1), z2) -> c97(ACTIVATE''(z2)) HEAD'(cons(z0, z1)) -> c63(U31''(tt, z0)) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 Tuples: U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U12''(tt, z0, z1) -> c44(SND'(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U42''(tt, z0, z1) -> c50(HEAD'(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2)) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2)) U63''(tt, z0, z1, z2) -> c55(U64''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1)) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U82''(tt, z0, z1) -> c60(FST'(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2)), ACTIVATE'(z2)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c76(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U12'''(tt, z0, z1) -> c77(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U42'''(tt, z0, z1) -> c84(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U42'''(tt, z0, z1) -> c85(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c94(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z0)) U63'''(tt, z0, z1, z2) -> c95(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c96(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U82'''(tt, z0, z1) -> c102(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U82'''(tt, z0, z1) -> c103(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) S tuples: U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c76(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U12'''(tt, z0, z1) -> c77(SND''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U42'''(tt, z0, z1) -> c84(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U42'''(tt, z0, z1) -> c85(HEAD''(afterNth(activate(z0), activate(z1))), AFTERNTH'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), AFTERNTH''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z0)) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z1)) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c94(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z0)) U63'''(tt, z0, z1, z2) -> c95(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE''(z2)) U63'''(tt, z0, z1, z2) -> c96(U64'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U82'''(tt, z0, z1) -> c102(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U82'''(tt, z0, z1) -> c103(FST''(splitAt(activate(z0), activate(z1))), SPLITAT'(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), SPLITAT''(activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) K tuples:none Defined Rule Symbols: U11'_3, U12'_3, U21'_2, U22'_2, U31'_2, U32'_2, U41'_3, U42'_3, U51'_2, U52'_2, U61'_4, U62'_4, U63'_4, U64'_2, U71'_2, U72'_2, U81'_3, U82'_3, AFTERNTH_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_3, U12_3, U21_2, U22_2, U31_2, U32_2, U41_3, U42_3, U51_2, U52_2, U61_4, U62_4, U63_4, U64_2, U71_2, U72_2, U81_3, U82_3, afterNth_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, AFTERNTH'_2, SPLITAT'_2, U11'''_3, U12'''_3, U41'''_3, U42'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, U82'''_3, AFTERNTH''_2, SPLITAT''_2 Compound Symbols: c43_3, c44_4, c49_3, c50_4, c53_4, c54_4, c55_5, c59_3, c60_4, c61_1, c69_2, c74_4, c75_4, c76_8, c77_8, c82_4, c83_4, c84_8, c85_8, c88_5, c89_5, c90_5, c91_5, c92_5, c93_5, c94_9, c95_9, c96_6, c100_4, c101_4, c102_8, c103_8, c104_1, c112_3 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 125 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c76(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c77(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c84(AFTERNTH'(activate(z0), activate(z1)), AFTERNTH''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c85(AFTERNTH'(activate(z0), activate(z1)), AFTERNTH''(activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c102(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c103(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) S tuples: AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c76(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c77(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c84(AFTERNTH'(activate(z0), activate(z1)), AFTERNTH''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c85(AFTERNTH'(activate(z0), activate(z1)), AFTERNTH''(activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c102(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c103(SPLITAT'(activate(z0), activate(z1)), SPLITAT''(activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) K tuples:none Defined Rule Symbols: U11'_3, U12'_3, U21'_2, U22'_2, U31'_2, U32'_2, U41'_3, U42'_3, U51'_2, U52'_2, U61'_4, U62'_4, U63'_4, U64'_2, U71'_2, U72'_2, U81'_3, U82'_3, AFTERNTH_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_3, U12_3, U21_2, U22_2, U31_2, U32_2, U41_3, U42_3, U51_2, U52_2, U61_4, U62_4, U63_4, U64_2, U71_2, U72_2, U81_3, U82_3, afterNth_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: AFTERNTH'_2, AFTERNTH''_2, U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, SPLITAT'_2, U11'''_3, U12'''_3, U41'''_3, U42'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, U82'''_3, SPLITAT''_2 Compound Symbols: c61_1, c104_1, c43_1, c44_1, c49_1, c50_1, c53_1, c54_1, c55_1, c59_1, c60_1, c69_1, c74_1, c75_1, c76_2, c77_2, c82_1, c83_1, c84_2, c85_2, c88_1, c89_1, c90_1, c91_1, c92_1, c93_1, c94_2, c95_2, c96_1, c100_1, c101_1, c102_2, c103_2, c112_1 ---------------------------------------- (9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) S tuples: AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) K tuples:none Defined Rule Symbols: U11'_3, U12'_3, U21'_2, U22'_2, U31'_2, U32'_2, U41'_3, U42'_3, U51'_2, U52'_2, U61'_4, U62'_4, U63'_4, U64'_2, U71'_2, U72'_2, U81'_3, U82'_3, AFTERNTH_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_3, U12_3, U21_2, U22_2, U31_2, U32_2, U41_3, U42_3, U51_2, U52_2, U61_4, U62_4, U63_4, U64_2, U71_2, U72_2, U81_3, U82_3, afterNth_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: AFTERNTH'_2, AFTERNTH''_2, U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, SPLITAT'_2, U11'''_3, U41'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, SPLITAT''_2, U12'''_3, U42'''_3, U82'''_3 Compound Symbols: c61_1, c104_1, c43_1, c44_1, c49_1, c50_1, c53_1, c54_1, c55_1, c59_1, c60_1, c69_1, c74_1, c75_1, c82_1, c83_1, c88_1, c89_1, c90_1, c91_1, c92_1, c93_1, c94_2, c95_2, c96_1, c100_1, c101_1, c112_1, c45_1 ---------------------------------------- (11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) S tuples: U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) K tuples: U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) Defined Rule Symbols: U11'_3, U12'_3, U21'_2, U22'_2, U31'_2, U32'_2, U41'_3, U42'_3, U51'_2, U52'_2, U61'_4, U62'_4, U63'_4, U64'_2, U71'_2, U72'_2, U81'_3, U82'_3, AFTERNTH_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_3, U12_3, U21_2, U22_2, U31_2, U32_2, U41_3, U42_3, U51_2, U52_2, U61_4, U62_4, U63_4, U64_2, U71_2, U72_2, U81_3, U82_3, afterNth_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: AFTERNTH'_2, AFTERNTH''_2, U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, SPLITAT'_2, U11'''_3, U41'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, SPLITAT''_2, U12'''_3, U42'''_3, U82'''_3 Compound Symbols: c61_1, c104_1, c43_1, c44_1, c49_1, c50_1, c53_1, c54_1, c55_1, c59_1, c60_1, c69_1, c74_1, c75_1, c82_1, c83_1, c88_1, c89_1, c90_1, c91_1, c92_1, c93_1, c94_2, c95_2, c96_1, c100_1, c101_1, c112_1, c45_1 ---------------------------------------- (13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> snd(splitAt(activate(z0), activate(z1))) U21(tt, z0) -> U22(tt, activate(z0)) U22(tt, z0) -> activate(z0) U31(tt, z0) -> U32(tt, activate(z0)) U32(tt, z0) -> activate(z0) U41(tt, z0, z1) -> U42(tt, activate(z0), activate(z1)) U42(tt, z0, z1) -> head(afterNth(activate(z0), activate(z1))) U51(tt, z0) -> U52(tt, activate(z0)) U52(tt, z0) -> activate(z0) U61(tt, z0, z1, z2) -> U62(tt, activate(z0), activate(z1), activate(z2)) U62(tt, z0, z1, z2) -> U63(tt, activate(z0), activate(z1), activate(z2)) U63(tt, z0, z1, z2) -> U64(splitAt(activate(z0), activate(z2)), activate(z1)) U64(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) U71(tt, z0) -> U72(tt, activate(z0)) U72(tt, z0) -> activate(z0) U81(tt, z0, z1) -> U82(tt, activate(z0), activate(z1)) U82(tt, z0, z1) -> fst(splitAt(activate(z0), activate(z1))) afterNth(z0, z1) -> U11(tt, z0, z1) fst(pair(z0, z1)) -> U21(tt, z0) head(cons(z0, z1)) -> U31(tt, z0) sel(z0, z1) -> U41(tt, z0, z1) snd(pair(z0, z1)) -> U51(tt, z1) splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U61(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> U71(tt, activate(z1)) take(z0, z1) -> U81(tt, z0, z1) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U12'(tt, z0, z1) -> c3(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) U22'(tt, z0) -> c5(ACTIVATE(z0)) U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U42'(tt, z0, z1) -> c10(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0)) U42'(tt, z0, z1) -> c11(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z1)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0)) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z1)) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c20(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U63'(tt, z0, z1, z2) -> c21(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U82'(tt, z0, z1) -> c28(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0)) U82'(tt, z0, z1) -> c29(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 SEL(z0, z1) -> c35(U41'(tt, z0, z1)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) SPLITAT(0, z0) -> c37 SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) ACTIVATE(z0) -> c42 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) S tuples: U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) K tuples: U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: AFTERNTH'_2, AFTERNTH''_2, U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, SPLITAT'_2, U11'''_3, U41'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, SPLITAT''_2, U12'''_3, U42'''_3, U82'''_3 Compound Symbols: c61_1, c104_1, c43_1, c44_1, c49_1, c50_1, c53_1, c54_1, c55_1, c59_1, c60_1, c69_1, c74_1, c75_1, c82_1, c83_1, c88_1, c89_1, c90_1, c91_1, c92_1, c93_1, c94_2, c95_2, c96_1, c100_1, c101_1, c112_1, c45_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) We considered the (Usable) Rules:none And the Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(AFTERNTH'(x_1, x_2)) = [1] POL(AFTERNTH''(x_1, x_2)) = [1] POL(SPLITAT'(x_1, x_2)) = 0 POL(SPLITAT''(x_1, x_2)) = [1] POL(U11''(x_1, x_2, x_3)) = [1] POL(U11'''(x_1, x_2, x_3)) = x_1 POL(U12''(x_1, x_2, x_3)) = [1] POL(U12'''(x_1, x_2, x_3)) = [1] POL(U41''(x_1, x_2, x_3)) = [1] + x_1 POL(U41'''(x_1, x_2, x_3)) = [1] + x_1 POL(U42''(x_1, x_2, x_3)) = x_1 POL(U42'''(x_1, x_2, x_3)) = [1] + x_1 POL(U61''(x_1, x_2, x_3, x_4)) = 0 POL(U61'''(x_1, x_2, x_3, x_4)) = x_1 POL(U62''(x_1, x_2, x_3, x_4)) = 0 POL(U62'''(x_1, x_2, x_3, x_4)) = x_1 POL(U63''(x_1, x_2, x_3, x_4)) = 0 POL(U63'''(x_1, x_2, x_3, x_4)) = [1] POL(U81''(x_1, x_2, x_3)) = [1] POL(U81'''(x_1, x_2, x_3)) = [1] + x_1 POL(U82''(x_1, x_2, x_3)) = [1] POL(U82'''(x_1, x_2, x_3)) = [1] + x_1 POL(activate(x_1)) = x_1 POL(c100(x_1)) = x_1 POL(c101(x_1)) = x_1 POL(c104(x_1)) = x_1 POL(c112(x_1)) = x_1 POL(c43(x_1)) = x_1 POL(c44(x_1)) = x_1 POL(c45(x_1)) = x_1 POL(c49(x_1)) = x_1 POL(c50(x_1)) = x_1 POL(c53(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1)) = x_1 POL(c88(x_1)) = x_1 POL(c89(x_1)) = x_1 POL(c90(x_1)) = x_1 POL(c91(x_1)) = x_1 POL(c92(x_1)) = x_1 POL(c93(x_1)) = x_1 POL(c94(x_1, x_2)) = x_1 + x_2 POL(c95(x_1, x_2)) = x_1 + x_2 POL(c96(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] POL(n__natsFrom(x_1)) = [1] + x_1 POL(natsFrom(x_1)) = [1] + x_1 POL(s(x_1)) = [1] + x_1 POL(tt) = [1] ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) S tuples: U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) K tuples: U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: AFTERNTH'_2, AFTERNTH''_2, U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, SPLITAT'_2, U11'''_3, U41'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, SPLITAT''_2, U12'''_3, U42'''_3, U82'''_3 Compound Symbols: c61_1, c104_1, c43_1, c44_1, c49_1, c50_1, c53_1, c54_1, c55_1, c59_1, c60_1, c69_1, c74_1, c75_1, c82_1, c83_1, c88_1, c89_1, c90_1, c91_1, c92_1, c93_1, c94_2, c95_2, c96_1, c100_1, c101_1, c112_1, c45_1 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) We considered the (Usable) Rules: natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 natsFrom(z0) -> n__natsFrom(z0) And the Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(AFTERNTH'(x_1, x_2)) = [1] + x_1 + x_2 POL(AFTERNTH''(x_1, x_2)) = [1] + x_1 + x_2 POL(SPLITAT'(x_1, x_2)) = 0 POL(SPLITAT''(x_1, x_2)) = x_1 POL(U11''(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(U11'''(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(U12''(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(U12'''(x_1, x_2, x_3)) = x_2 POL(U41''(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(U41'''(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(U42''(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(U42'''(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(U61''(x_1, x_2, x_3, x_4)) = 0 POL(U61'''(x_1, x_2, x_3, x_4)) = x_1 + x_2 POL(U62''(x_1, x_2, x_3, x_4)) = 0 POL(U62'''(x_1, x_2, x_3, x_4)) = x_2 POL(U63''(x_1, x_2, x_3, x_4)) = 0 POL(U63'''(x_1, x_2, x_3, x_4)) = x_2 POL(U81''(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(U81'''(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(U82''(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(U82'''(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(activate(x_1)) = x_1 POL(c100(x_1)) = x_1 POL(c101(x_1)) = x_1 POL(c104(x_1)) = x_1 POL(c112(x_1)) = x_1 POL(c43(x_1)) = x_1 POL(c44(x_1)) = x_1 POL(c45(x_1)) = x_1 POL(c49(x_1)) = x_1 POL(c50(x_1)) = x_1 POL(c53(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1)) = x_1 POL(c88(x_1)) = x_1 POL(c89(x_1)) = x_1 POL(c90(x_1)) = x_1 POL(c91(x_1)) = x_1 POL(c92(x_1)) = x_1 POL(c93(x_1)) = x_1 POL(c94(x_1, x_2)) = x_1 + x_2 POL(c95(x_1, x_2)) = x_1 + x_2 POL(c96(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 POL(n__natsFrom(x_1)) = [1] + x_1 POL(natsFrom(x_1)) = [1] + x_1 POL(s(x_1)) = [1] + x_1 POL(tt) = [1] ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) Tuples: AFTERNTH'(z0, z1) -> c61(U11''(tt, z0, z1)) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11''(tt, z0, z1) -> c43(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c44(SPLITAT'(activate(z0), activate(z1))) U41''(tt, z0, z1) -> c49(U42''(tt, activate(z0), activate(z1))) U42''(tt, z0, z1) -> c50(AFTERNTH'(activate(z0), activate(z1))) U61''(tt, z0, z1, z2) -> c53(U62''(tt, activate(z0), activate(z1), activate(z2))) U62''(tt, z0, z1, z2) -> c54(U63''(tt, activate(z0), activate(z1), activate(z2))) U63''(tt, z0, z1, z2) -> c55(SPLITAT'(activate(z0), activate(z2))) U81''(tt, z0, z1) -> c59(U82''(tt, activate(z0), activate(z1))) U82''(tt, z0, z1) -> c60(SPLITAT'(activate(z0), activate(z1))) SPLITAT'(s(z0), cons(z1, z2)) -> c69(U61''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) S tuples: U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) K tuples: U41'''(tt, z0, z1) -> c82(U42'''(tt, activate(z0), activate(z1))) U41'''(tt, z0, z1) -> c83(U42'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c100(U82'''(tt, activate(z0), activate(z1))) U81'''(tt, z0, z1) -> c101(U82'''(tt, activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH'(activate(z0), activate(z1))) U42'''(tt, z0, z1) -> c45(AFTERNTH''(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U82'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) AFTERNTH''(z0, z1) -> c104(U11'''(tt, z0, z1)) U11'''(tt, z0, z1) -> c74(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c75(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT'(activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c45(SPLITAT''(activate(z0), activate(z1))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: AFTERNTH'_2, AFTERNTH''_2, U11''_3, U12''_3, U41''_3, U42''_3, U61''_4, U62''_4, U63''_4, U81''_3, U82''_3, SPLITAT'_2, U11'''_3, U41'''_3, U61'''_4, U62'''_4, U63'''_4, U81'''_3, SPLITAT''_2, U12'''_3, U42'''_3, U82'''_3 Compound Symbols: c61_1, c104_1, c43_1, c44_1, c49_1, c50_1, c53_1, c54_1, c55_1, c59_1, c60_1, c69_1, c74_1, c75_1, c82_1, c83_1, c88_1, c89_1, c90_1, c91_1, c92_1, c93_1, c94_2, c95_2, c96_1, c100_1, c101_1, c112_1, c45_1 ---------------------------------------- (19) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: U62'''(tt, z0, z1, z2) -> c91(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c92(U63'''(tt, activate(z0), activate(z1), activate(z2))) U62'''(tt, z0, z1, z2) -> c93(U63'''(tt, activate(z0), activate(z1), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c94(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c95(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U63'''(tt, z0, z1, z2) -> c96(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c112(U61'''(tt, z0, z1, activate(z2))) U61'''(tt, z0, z1, z2) -> c88(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c89(U62'''(tt, activate(z0), activate(z1), activate(z2))) U61'''(tt, z0, z1, z2) -> c90(U62'''(tt, activate(z0), activate(z1), activate(z2))) Now S is empty ---------------------------------------- (20) BOUNDS(1, 1)