WORST_CASE(?,O(n^1)) proof of input_AvyFMmQTOo.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (4) CdtProblem (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 199 ms] (12) CdtProblem (13) CdtKnowledgeProof [FINISHED, 0 ms] (14) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: U11(tt, N, XS) -> U12(tt, activate(N), activate(XS)) U12(tt, N, XS) -> snd(splitAt(activate(N), activate(XS))) U21(tt, X) -> U22(tt, activate(X)) U22(tt, X) -> activate(X) U31(tt, N) -> U32(tt, activate(N)) U32(tt, N) -> activate(N) U41(tt, N, XS) -> U42(tt, activate(N), activate(XS)) U42(tt, N, XS) -> head(afterNth(activate(N), activate(XS))) U51(tt, Y) -> U52(tt, activate(Y)) U52(tt, Y) -> activate(Y) U61(tt, N, X, XS) -> U62(tt, activate(N), activate(X), activate(XS)) U62(tt, N, X, XS) -> U63(tt, activate(N), activate(X), activate(XS)) U63(tt, N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) U71(tt, XS) -> U72(tt, activate(XS)) U72(tt, XS) -> activate(XS) U81(tt, N, XS) -> U82(tt, activate(N), activate(XS)) U82(tt, N, XS) -> fst(splitAt(activate(N), activate(XS))) afterNth(N, XS) -> U11(tt, N, XS) fst(pair(X, Y)) -> U21(tt, X) head(cons(N, XS)) -> U31(tt, N) natsFrom(N) -> cons(N, n__natsFrom(s(N))) sel(N, XS) -> U41(tt, N, XS) snd(pair(X, Y)) -> U51(tt, Y) splitAt(0, XS) -> pair(nil, XS) splitAt(s(N), cons(X, XS)) -> U61(tt, N, X, activate(XS)) tail(cons(N, XS)) -> U71(tt, activate(XS)) take(N, XS) -> U81(tt, N, XS) natsFrom(X) -> n__natsFrom(X) activate(n__natsFrom(X)) -> natsFrom(X) activate(X) -> X S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) 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 Tuples: 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 S tuples: 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 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 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 Compound Symbols: c_2, c1_2, c2_3, c3_3, c4_2, c5_1, c6_2, c7_1, c8_2, c9_2, c10_3, c11_3, c12_2, c13_1, c14_2, c15_2, c16_2, c17_2, c18_2, c19_2, c20_3, c21_3, c22_2, c23_1, c24_2, c25_1, c26_2, c27_2, c28_3, c29_3, c30_1, c31_1, c32_1, c33, c34, c35_1, c36_1, c37, c38_2, c39_2, c40_1, c41_1, c42 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 2 leading nodes: SEL(z0, z1) -> c35(U41'(tt, z0, z1)) TAKE(z0, z1) -> c40(U81'(tt, z0, z1)) Removed 19 trailing nodes: TAIL(cons(z0, z1)) -> c39(U71'(tt, activate(z1)), ACTIVATE(z1)) U22'(tt, z0) -> c5(ACTIVATE(z0)) SPLITAT(0, z0) -> c37 U63'(tt, z0, z1, z2) -> c22(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), ACTIVATE(z1)) HEAD(cons(z0, z1)) -> c32(U31'(tt, z0)) U51'(tt, z0) -> c12(U52'(tt, activate(z0)), ACTIVATE(z0)) U72'(tt, z0) -> c25(ACTIVATE(z0)) U21'(tt, z0) -> c4(U22'(tt, activate(z0)), ACTIVATE(z0)) FST(pair(z0, z1)) -> c31(U21'(tt, z0)) U64'(pair(z0, z1), z2) -> c23(ACTIVATE(z2)) NATSFROM(z0) -> c33 NATSFROM(z0) -> c34 ACTIVATE(z0) -> c42 U31'(tt, z0) -> c6(U32'(tt, activate(z0)), ACTIVATE(z0)) U71'(tt, z0) -> c24(U72'(tt, activate(z0)), ACTIVATE(z0)) ACTIVATE(n__natsFrom(z0)) -> c41(NATSFROM(z0)) U52'(tt, z0) -> c13(ACTIVATE(z0)) U32'(tt, z0) -> c7(ACTIVATE(z0)) SND(pair(z0, z1)) -> c36(U51'(tt, z1)) ---------------------------------------- (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 Tuples: 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)) 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)) 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)) 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)) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2)) S tuples: 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)) 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)) 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)) 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)) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, 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 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 Compound Symbols: c_2, c1_2, c2_3, c3_3, c8_2, c9_2, c10_3, c11_3, c14_2, c15_2, c16_2, c17_2, c18_2, c19_2, c20_3, c21_3, c26_2, c27_2, c28_3, c29_3, c30_1, c38_2 ---------------------------------------- (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 29 trailing tuple parts ---------------------------------------- (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 Tuples: AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) S tuples: AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) SPLITAT(s(z0), cons(z1, z2)) -> c38(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 Defined Pair Symbols: AFTERNTH_2, U11'_3, U12'_3, U41'_3, U42'_3, U61'_4, U62'_4, U63'_4, U81'_3, U82'_3, SPLITAT_2 Compound Symbols: c30_1, c_1, c1_1, c2_1, c3_1, c8_1, c9_1, c10_1, c11_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c26_1, c27_1, c28_1, c29_1, c38_1 ---------------------------------------- (7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) ---------------------------------------- (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 Tuples: AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) S tuples: U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) K tuples: U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(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 Defined Pair Symbols: AFTERNTH_2, U11'_3, U12'_3, U41'_3, U42'_3, U61'_4, U62'_4, U63'_4, U81'_3, U82'_3, SPLITAT_2 Compound Symbols: c30_1, c_1, c1_1, c2_1, c3_1, c8_1, c9_1, c10_1, c11_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c26_1, c27_1, c28_1, c29_1, c38_1 ---------------------------------------- (9) 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) ---------------------------------------- (10) 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) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) S tuples: U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) K tuples: U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: AFTERNTH_2, U11'_3, U12'_3, U41'_3, U42'_3, U61'_4, U62'_4, U63'_4, U81'_3, U82'_3, SPLITAT_2 Compound Symbols: c30_1, c_1, c1_1, c2_1, c3_1, c8_1, c9_1, c10_1, c11_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c26_1, c27_1, c28_1, c29_1, c38_1 ---------------------------------------- (11) 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) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(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) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(AFTERNTH(x_1, x_2)) = [2]x_1 POL(SPLITAT(x_1, x_2)) = [2]x_1 POL(U11'(x_1, x_2, x_3)) = [3]x_1 + [2]x_2 POL(U12'(x_1, x_2, x_3)) = [3]x_1 + [2]x_2 POL(U41'(x_1, x_2, x_3)) = [3] + [3]x_1 + [3]x_2 + x_3 POL(U42'(x_1, x_2, x_3)) = [3]x_1 + [2]x_2 POL(U61'(x_1, x_2, x_3, x_4)) = [2] + [3]x_1 + [2]x_2 POL(U62'(x_1, x_2, x_3, x_4)) = [3]x_1 + [2]x_2 POL(U63'(x_1, x_2, x_3, x_4)) = [3]x_1 + [2]x_2 POL(U81'(x_1, x_2, x_3)) = [3]x_1 + [2]x_2 + x_3 POL(U82'(x_1, x_2, x_3)) = [3]x_1 + [2]x_2 POL(activate(x_1)) = x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c28(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(x_1)) = x_1 POL(c38(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = x_1 POL(n__natsFrom(x_1)) = x_1 POL(natsFrom(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 POL(tt) = 0 ---------------------------------------- (12) 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) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) S tuples: U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) K tuples: U41'(tt, z0, z1) -> c8(U42'(tt, activate(z0), activate(z1))) U41'(tt, z0, z1) -> c9(U42'(tt, activate(z0), activate(z1))) U42'(tt, z0, z1) -> c10(AFTERNTH(activate(z0), activate(z1))) U42'(tt, z0, z1) -> c11(AFTERNTH(activate(z0), activate(z1))) U81'(tt, z0, z1) -> c26(U82'(tt, activate(z0), activate(z1))) U81'(tt, z0, z1) -> c27(U82'(tt, activate(z0), activate(z1))) U82'(tt, z0, z1) -> c28(SPLITAT(activate(z0), activate(z1))) U82'(tt, z0, z1) -> c29(SPLITAT(activate(z0), activate(z1))) AFTERNTH(z0, z1) -> c30(U11'(tt, z0, z1)) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1))) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1))) U12'(tt, z0, z1) -> c2(SPLITAT(activate(z0), activate(z1))) U12'(tt, z0, z1) -> c3(SPLITAT(activate(z0), activate(z1))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) Defined Rule Symbols: activate_1, natsFrom_1 Defined Pair Symbols: AFTERNTH_2, U11'_3, U12'_3, U41'_3, U42'_3, U61'_4, U62'_4, U63'_4, U81'_3, U82'_3, SPLITAT_2 Compound Symbols: c30_1, c_1, c1_1, c2_1, c3_1, c8_1, c9_1, c10_1, c11_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c26_1, c27_1, c28_1, c29_1, c38_1 ---------------------------------------- (13) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: U62'(tt, z0, z1, z2) -> c17(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c18(U63'(tt, activate(z0), activate(z1), activate(z2))) U62'(tt, z0, z1, z2) -> c19(U63'(tt, activate(z0), activate(z1), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c20(SPLITAT(activate(z0), activate(z2))) U63'(tt, z0, z1, z2) -> c21(SPLITAT(activate(z0), activate(z2))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) SPLITAT(s(z0), cons(z1, z2)) -> c38(U61'(tt, z0, z1, activate(z2))) U61'(tt, z0, z1, z2) -> c14(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c15(U62'(tt, activate(z0), activate(z1), activate(z2))) U61'(tt, z0, z1, z2) -> c16(U62'(tt, activate(z0), activate(z1), activate(z2))) Now S is empty ---------------------------------------- (14) BOUNDS(1, 1)