WORST_CASE(Omega(n^1),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(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 458 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 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) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (12) CdtProblem (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 74 ms] (16) CdtProblem (17) CdtKnowledgeProof [FINISHED, 0 ms] (18) BOUNDS(1, 1) (19) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (20) TRS for Loop Detection (21) DecreasingLoopProof [LOWER BOUND(ID), 3544 ms] (22) BEST (23) proven lower bound (24) LowerBoundPropagationProof [FINISHED, 0 ms] (25) BOUNDS(n^1, INF) (26) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 The (relative) TRS S consists of the following rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(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(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 The (relative) TRS S consists of the following rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(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, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 Tuples: U11''(tt, z0, z1, z2) -> c18(U12''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1)) U12''(pair(z0, z1), z2) -> c19(ACTIVATE'(z2)) AFTERNTH'(z0, z1) -> c20(SND'(splitAt(z0, z1)), SPLITAT'(z0, z1)) AND'(tt, z0) -> c21(ACTIVATE'(z0)) FST'(pair(z0, z1)) -> c22 HEAD'(cons(z0, z1)) -> c23 NATSFROM'(z0) -> c24 NATSFROM'(z0) -> c25 SEL'(z0, z1) -> c26(HEAD'(afterNth(z0, z1)), AFTERNTH'(z0, z1)) SND'(pair(z0, z1)) -> c27 SPLITAT'(0, z0) -> c28 SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2)), ACTIVATE'(z2)) TAIL'(cons(z0, z1)) -> c30(ACTIVATE'(z1)) TAKE'(z0, z1) -> c31(FST'(splitAt(z0, z1)), SPLITAT'(z0, z1)) ACTIVATE'(n__natsFrom(z0)) -> c32(NATSFROM'(z0)) ACTIVATE'(z0) -> c33 U11'''(tt, z0, z1, z2) -> c34(U12'''(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)) U11'''(tt, z0, z1, z2) -> c35(U12'''(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)) U11'''(tt, z0, z1, z2) -> c36(U12'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(pair(z0, z1), z2) -> c37(ACTIVATE''(z2)) AFTERNTH''(z0, z1) -> c38(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) AND''(tt, z0) -> c39(ACTIVATE''(z0)) FST''(pair(z0, z1)) -> c40 HEAD''(cons(z0, z1)) -> c41 NATSFROM''(z0) -> c42 NATSFROM''(z0) -> c43 SEL''(z0, z1) -> c44(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1)) SND''(pair(z0, z1)) -> c45 SPLITAT''(0, z0) -> c46 SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) TAIL''(cons(z0, z1)) -> c48(ACTIVATE''(z1)) TAKE''(z0, z1) -> c49(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) ACTIVATE''(n__natsFrom(z0)) -> c50(NATSFROM''(z0)) ACTIVATE''(z0) -> c51 S tuples: U11'''(tt, z0, z1, z2) -> c34(U12'''(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)) U11'''(tt, z0, z1, z2) -> c35(U12'''(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)) U11'''(tt, z0, z1, z2) -> c36(U12'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(pair(z0, z1), z2) -> c37(ACTIVATE''(z2)) AFTERNTH''(z0, z1) -> c38(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) AND''(tt, z0) -> c39(ACTIVATE''(z0)) FST''(pair(z0, z1)) -> c40 HEAD''(cons(z0, z1)) -> c41 NATSFROM''(z0) -> c42 NATSFROM''(z0) -> c43 SEL''(z0, z1) -> c44(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1)) SND''(pair(z0, z1)) -> c45 SPLITAT''(0, z0) -> c46 SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) TAIL''(cons(z0, z1)) -> c48(ACTIVATE''(z1)) TAKE''(z0, z1) -> c49(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) ACTIVATE''(n__natsFrom(z0)) -> c50(NATSFROM''(z0)) ACTIVATE''(z0) -> c51 K tuples:none Defined Rule Symbols: U11'_4, U12'_2, AFTERNTH_2, AND_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_4, U12''_2, AFTERNTH'_2, AND'_2, FST'_1, HEAD'_1, NATSFROM'_1, SEL'_2, SND'_1, SPLITAT'_2, TAIL'_1, TAKE'_2, ACTIVATE'_1, U11'''_4, U12'''_2, AFTERNTH''_2, AND''_2, FST''_1, HEAD''_1, NATSFROM''_1, SEL''_2, SND''_1, SPLITAT''_2, TAIL''_1, TAKE''_2, ACTIVATE''_1 Compound Symbols: c18_5, c19_1, c20_2, c21_1, c22, c23, c24, c25, c26_2, c27, c28, c29_2, c30_1, c31_2, c32_1, c33, c34_9, c35_9, c36_6, c37_1, c38_3, c39_1, c40, c41, c42, c43, c44_3, c45, c46, c47_3, c48_1, c49_3, c50_1, c51 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 22 trailing nodes: U12'''(pair(z0, z1), z2) -> c37(ACTIVATE''(z2)) ACTIVATE'(n__natsFrom(z0)) -> c32(NATSFROM'(z0)) SPLITAT''(0, z0) -> c46 FST''(pair(z0, z1)) -> c40 TAIL''(cons(z0, z1)) -> c48(ACTIVATE''(z1)) HEAD''(cons(z0, z1)) -> c41 TAIL'(cons(z0, z1)) -> c30(ACTIVATE'(z1)) ACTIVATE''(z0) -> c51 ACTIVATE''(n__natsFrom(z0)) -> c50(NATSFROM''(z0)) U12''(pair(z0, z1), z2) -> c19(ACTIVATE'(z2)) NATSFROM'(z0) -> c24 AND''(tt, z0) -> c39(ACTIVATE''(z0)) SND''(pair(z0, z1)) -> c45 ACTIVATE'(z0) -> c33 NATSFROM''(z0) -> c43 SPLITAT'(0, z0) -> c28 HEAD'(cons(z0, z1)) -> c23 AND'(tt, z0) -> c21(ACTIVATE'(z0)) FST'(pair(z0, z1)) -> c22 NATSFROM''(z0) -> c42 SND'(pair(z0, z1)) -> c27 NATSFROM'(z0) -> c25 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 Tuples: U11''(tt, z0, z1, z2) -> c18(U12''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1)) AFTERNTH'(z0, z1) -> c20(SND'(splitAt(z0, z1)), SPLITAT'(z0, z1)) SEL'(z0, z1) -> c26(HEAD'(afterNth(z0, z1)), AFTERNTH'(z0, z1)) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2)), ACTIVATE'(z2)) TAKE'(z0, z1) -> c31(FST'(splitAt(z0, z1)), SPLITAT'(z0, z1)) U11'''(tt, z0, z1, z2) -> c34(U12'''(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)) U11'''(tt, z0, z1, z2) -> c35(U12'''(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)) U11'''(tt, z0, z1, z2) -> c36(U12'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) AFTERNTH''(z0, z1) -> c38(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) SEL''(z0, z1) -> c44(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1)) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) TAKE''(z0, z1) -> c49(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) S tuples: U11'''(tt, z0, z1, z2) -> c34(U12'''(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)) U11'''(tt, z0, z1, z2) -> c35(U12'''(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)) U11'''(tt, z0, z1, z2) -> c36(U12'''(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT'(activate(z0), activate(z2)), ACTIVATE'(z0), ACTIVATE'(z2), ACTIVATE'(z1), ACTIVATE''(z1)) AFTERNTH''(z0, z1) -> c38(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) SEL''(z0, z1) -> c44(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1)) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2)) TAKE''(z0, z1) -> c49(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1)) K tuples:none Defined Rule Symbols: U11'_4, U12'_2, AFTERNTH_2, AND_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_4, AFTERNTH'_2, SEL'_2, SPLITAT'_2, TAKE'_2, U11'''_4, AFTERNTH''_2, SEL''_2, SPLITAT''_2, TAKE''_2 Compound Symbols: c18_5, c20_2, c26_2, c29_2, c31_2, c34_9, c35_9, c36_6, c38_3, c44_3, c47_3, c49_3 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 32 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 Tuples: U11''(tt, z0, z1, z2) -> c18(SPLITAT'(activate(z0), activate(z2))) AFTERNTH'(z0, z1) -> c20(SPLITAT'(z0, z1)) SEL'(z0, z1) -> c26(AFTERNTH'(z0, z1)) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2))) TAKE'(z0, z1) -> c31(SPLITAT'(z0, z1)) U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) AFTERNTH''(z0, z1) -> c38(SPLITAT'(z0, z1), SPLITAT''(z0, z1)) SEL''(z0, z1) -> c44(AFTERNTH'(z0, z1), AFTERNTH''(z0, z1)) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) TAKE''(z0, z1) -> c49(SPLITAT'(z0, z1), SPLITAT''(z0, z1)) S tuples: U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) AFTERNTH''(z0, z1) -> c38(SPLITAT'(z0, z1), SPLITAT''(z0, z1)) SEL''(z0, z1) -> c44(AFTERNTH'(z0, z1), AFTERNTH''(z0, z1)) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) TAKE''(z0, z1) -> c49(SPLITAT'(z0, z1), SPLITAT''(z0, z1)) K tuples:none Defined Rule Symbols: U11'_4, U12'_2, AFTERNTH_2, AND_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_4, AFTERNTH'_2, SEL'_2, SPLITAT'_2, TAKE'_2, U11'''_4, AFTERNTH''_2, SEL''_2, SPLITAT''_2, TAKE''_2 Compound Symbols: c18_1, c20_1, c26_1, c29_1, c31_1, c34_2, c35_2, c36_1, c38_2, c44_2, c47_1, c49_2 ---------------------------------------- (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, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 Tuples: U11''(tt, z0, z1, z2) -> c18(SPLITAT'(activate(z0), activate(z2))) AFTERNTH'(z0, z1) -> c20(SPLITAT'(z0, z1)) SEL'(z0, z1) -> c26(AFTERNTH'(z0, z1)) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2))) TAKE'(z0, z1) -> c31(SPLITAT'(z0, z1)) U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) AFTERNTH''(z0, z1) -> c19(SPLITAT'(z0, z1)) AFTERNTH''(z0, z1) -> c19(SPLITAT''(z0, z1)) SEL''(z0, z1) -> c19(AFTERNTH'(z0, z1)) SEL''(z0, z1) -> c19(AFTERNTH''(z0, z1)) TAKE''(z0, z1) -> c19(SPLITAT'(z0, z1)) TAKE''(z0, z1) -> c19(SPLITAT''(z0, z1)) S tuples: U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) AFTERNTH''(z0, z1) -> c19(SPLITAT'(z0, z1)) AFTERNTH''(z0, z1) -> c19(SPLITAT''(z0, z1)) SEL''(z0, z1) -> c19(AFTERNTH'(z0, z1)) SEL''(z0, z1) -> c19(AFTERNTH''(z0, z1)) TAKE''(z0, z1) -> c19(SPLITAT'(z0, z1)) TAKE''(z0, z1) -> c19(SPLITAT''(z0, z1)) K tuples:none Defined Rule Symbols: U11'_4, U12'_2, AFTERNTH_2, AND_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_4, AFTERNTH'_2, SEL'_2, SPLITAT'_2, TAKE'_2, U11'''_4, SPLITAT''_2, AFTERNTH''_2, SEL''_2, TAKE''_2 Compound Symbols: c18_1, c20_1, c26_1, c29_1, c31_1, c34_2, c35_2, c36_1, c47_1, c19_1 ---------------------------------------- (11) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 9 leading nodes: SEL'(z0, z1) -> c26(AFTERNTH'(z0, z1)) SEL''(z0, z1) -> c19(AFTERNTH'(z0, z1)) AFTERNTH'(z0, z1) -> c20(SPLITAT'(z0, z1)) TAKE'(z0, z1) -> c31(SPLITAT'(z0, z1)) SEL''(z0, z1) -> c19(AFTERNTH''(z0, z1)) AFTERNTH''(z0, z1) -> c19(SPLITAT''(z0, z1)) TAKE''(z0, z1) -> c19(SPLITAT''(z0, z1)) AFTERNTH''(z0, z1) -> c19(SPLITAT'(z0, z1)) TAKE''(z0, z1) -> c19(SPLITAT'(z0, z1)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 Tuples: U11''(tt, z0, z1, z2) -> c18(SPLITAT'(activate(z0), activate(z2))) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) S tuples: U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) K tuples:none Defined Rule Symbols: U11'_4, U12'_2, AFTERNTH_2, AND_2, FST_1, HEAD_1, NATSFROM_1, SEL_2, SND_1, SPLITAT_2, TAIL_1, TAKE_2, ACTIVATE_1, U11_4, U12_2, afterNth_2, and_2, fst_1, head_1, natsFrom_1, sel_2, snd_1, splitAt_2, tail_1, take_2, activate_1 Defined Pair Symbols: U11''_4, SPLITAT'_2, U11'''_4, SPLITAT''_2 Compound Symbols: c18_1, c29_1, c34_2, c35_2, c36_1, c47_1 ---------------------------------------- (13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 ---------------------------------------- (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: U11''(tt, z0, z1, z2) -> c18(SPLITAT'(activate(z0), activate(z2))) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) S tuples: U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) K tuples:none Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: U11''_4, SPLITAT'_2, U11'''_4, SPLITAT''_2 Compound Symbols: c18_1, c29_1, c34_2, c35_2, c36_1, c47_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. U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, 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: U11''(tt, z0, z1, z2) -> c18(SPLITAT'(activate(z0), activate(z2))) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(SPLITAT'(x_1, x_2)) = 0 POL(SPLITAT''(x_1, x_2)) = [1] + x_1 POL(U11''(x_1, x_2, x_3, x_4)) = 0 POL(U11'''(x_1, x_2, x_3, x_4)) = [1] + x_2 POL(activate(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c34(x_1, x_2)) = x_1 + x_2 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c47(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] ---------------------------------------- (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: U11''(tt, z0, z1, z2) -> c18(SPLITAT'(activate(z0), activate(z2))) SPLITAT'(s(z0), cons(z1, z2)) -> c29(U11''(tt, z0, z1, activate(z2))) U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) S tuples: U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) K tuples: U11'''(tt, z0, z1, z2) -> c36(SPLITAT'(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: U11''_4, SPLITAT'_2, U11'''_4, SPLITAT''_2 Compound Symbols: c18_1, c29_1, c34_2, c35_2, c36_1, c47_1 ---------------------------------------- (17) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: U11'''(tt, z0, z1, z2) -> c34(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) U11'''(tt, z0, z1, z2) -> c35(SPLITAT'(activate(z0), activate(z2)), SPLITAT''(activate(z0), activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) SPLITAT''(s(z0), cons(z1, z2)) -> c47(U11'''(tt, z0, z1, activate(z2))) Now S is empty ---------------------------------------- (18) BOUNDS(1, 1) ---------------------------------------- (19) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (20) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 The (relative) TRS S consists of the following rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (21) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence U11'(tt, s(z01_3), z1, cons(z12_3, z23_3)) ->^+ c1(U12'(splitAt(activate(s(z01_3)), activate(cons(z12_3, z23_3))), activate(z1)), c13(U11'(tt, z01_3, z12_3, z23_3), ACTIVATE(z23_3)), ACTIVATE(cons(z12_3, z23_3))) gives rise to a decreasing loop by considering the right hand sides subterm at position [1,0]. The pumping substitution is [z01_3 / s(z01_3), z23_3 / cons(z12_3, z23_3)]. The result substitution is [z1 / z12_3]. ---------------------------------------- (22) Complex Obligation (BEST) ---------------------------------------- (23) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 The (relative) TRS S consists of the following rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1, z2) -> c(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0)) U11'(tt, z0, z1, z2) -> c1(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z2)) U11'(tt, z0, z1, z2) -> c2(U12'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) U12'(pair(z0, z1), z2) -> c3(ACTIVATE(z2)) AFTERNTH(z0, z1) -> c4(SND(splitAt(z0, z1)), SPLITAT(z0, z1)) AND(tt, z0) -> c5(ACTIVATE(z0)) FST(pair(z0, z1)) -> c6 HEAD(cons(z0, z1)) -> c7 NATSFROM(z0) -> c8 NATSFROM(z0) -> c9 SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1)) SND(pair(z0, z1)) -> c11 SPLITAT(0, z0) -> c12 SPLITAT(s(z0), cons(z1, z2)) -> c13(U11'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) TAIL(cons(z0, z1)) -> c14(ACTIVATE(z1)) TAKE(z0, z1) -> c15(FST(splitAt(z0, z1)), SPLITAT(z0, z1)) ACTIVATE(n__natsFrom(z0)) -> c16(NATSFROM(z0)) ACTIVATE(z0) -> c17 The (relative) TRS S consists of the following rules: U11(tt, z0, z1, z2) -> U12(splitAt(activate(z0), activate(z2)), activate(z1)) U12(pair(z0, z1), z2) -> pair(cons(activate(z2), z0), z1) afterNth(z0, z1) -> snd(splitAt(z0, z1)) and(tt, z0) -> activate(z0) fst(pair(z0, z1)) -> z0 head(cons(z0, z1)) -> z0 natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0, z1) -> head(afterNth(z0, z1)) snd(pair(z0, z1)) -> z1 splitAt(0, z0) -> pair(nil, z0) splitAt(s(z0), cons(z1, z2)) -> U11(tt, z0, z1, activate(z2)) tail(cons(z0, z1)) -> activate(z1) take(z0, z1) -> fst(splitAt(z0, z1)) activate(n__natsFrom(z0)) -> natsFrom(z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST