WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/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), 235 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 55 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 2 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 13 ms] (14) CdtProblem (15) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (16) BOUNDS(1, 1) (17) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (18) TRS for Loop Detection (19) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (20) BEST (21) proven lower bound (22) LowerBoundPropagationProof [FINISHED, 0 ms] (23) BOUNDS(n^1, INF) (24) 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: SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 The (relative) TRS S consists of the following rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, 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: SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 The (relative) TRS S consists of the following rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) SELECT'(Cons(z0, z1)) -> c9(SELECTS'(z0, Nil, z1)) SELECT'(Nil) -> c10 REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) REVAPP'(Nil, z0) -> c12 SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) SELECT''(Cons(z0, z1)) -> c16(SELECTS''(z0, Nil, z1)) SELECT''(Nil) -> c17 REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) REVAPP''(Nil, z0) -> c19 S tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) SELECT''(Cons(z0, z1)) -> c16(SELECTS''(z0, Nil, z1)) SELECT''(Nil) -> c17 REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) REVAPP''(Nil, z0) -> c19 K tuples:none Defined Rule Symbols: SELECTS_3, SELECT_1, REVAPP_2, selects_3, select_1, revapp_2 Defined Pair Symbols: SELECTS'_3, SELECT'_1, REVAPP'_2, SELECTS''_3, SELECT''_1, REVAPP''_2 Compound Symbols: c7_2, c8_1, c9_1, c10, c11_1, c12, c13_1, c14_1, c15_1, c16_1, c17, c18_1, c19 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 2 leading nodes: SELECT'(Cons(z0, z1)) -> c9(SELECTS'(z0, Nil, z1)) SELECT''(Cons(z0, z1)) -> c16(SELECTS''(z0, Nil, z1)) Removed 4 trailing nodes: SELECT''(Nil) -> c17 REVAPP''(Nil, z0) -> c19 REVAPP'(Nil, z0) -> c12 SELECT'(Nil) -> c10 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) S tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) K tuples:none Defined Rule Symbols: SELECTS_3, SELECT_1, REVAPP_2, selects_3, select_1, revapp_2 Defined Pair Symbols: SELECTS'_3, REVAPP'_2, SELECTS''_3, REVAPP''_2 Compound Symbols: c7_2, c8_1, c11_1, c13_1, c14_1, c15_1, c18_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) S tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: SELECTS'_3, REVAPP'_2, SELECTS''_3, REVAPP''_2 Compound Symbols: c7_2, c8_1, c11_1, c13_1, c14_1, c15_1, c18_1 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) We considered the (Usable) Rules:none And the Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(Nil) = [1] POL(REVAPP'(x_1, x_2)) = [1] POL(REVAPP''(x_1, x_2)) = x_1 + x_2 POL(SELECTS'(x_1, x_2, x_3)) = x_1 + x_3 POL(SELECTS''(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(c11(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c7(x_1, x_2)) = x_1 + x_2 POL(c8(x_1)) = x_1 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) S tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) K tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) Defined Rule Symbols:none Defined Pair Symbols: SELECTS'_3, REVAPP'_2, SELECTS''_3, REVAPP''_2 Compound Symbols: c7_2, c8_1, c11_1, c13_1, c14_1, c15_1, c18_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. REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) We considered the (Usable) Rules:none And the Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(Nil) = [1] POL(REVAPP'(x_1, x_2)) = [1] POL(REVAPP''(x_1, x_2)) = [1] + x_1 POL(SELECTS'(x_1, x_2, x_3)) = [1] + x_1 + x_3 POL(SELECTS''(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(c11(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c7(x_1, x_2)) = x_1 + x_2 POL(c8(x_1)) = x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) S tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) K tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) Defined Rule Symbols:none Defined Pair Symbols: SELECTS'_3, REVAPP'_2, SELECTS''_3, REVAPP''_2 Compound Symbols: c7_2, c8_1, c11_1, c13_1, c14_1, c15_1, c18_1 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) We considered the (Usable) Rules:none And the Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(Nil) = [1] POL(REVAPP'(x_1, x_2)) = [1] POL(REVAPP''(x_1, x_2)) = [1] POL(SELECTS'(x_1, x_2, x_3)) = [1] + x_1 + x_3 POL(SELECTS''(x_1, x_2, x_3)) = x_1 + x_3 POL(c11(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c7(x_1, x_2)) = x_1 + x_2 POL(c8(x_1)) = x_1 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: SELECTS'(z0, z1, Cons(z2, z3)) -> c7(REVAPP'(z1, Cons(z2, z3)), SELECTS'(z2, Cons(z0, z1), z3)) SELECTS'(z0, z1, Nil) -> c8(REVAPP'(z1, Nil)) REVAPP'(Cons(z0, z1), z2) -> c11(REVAPP'(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) S tuples:none K tuples: SELECTS''(z0, z1, Cons(z2, z3)) -> c13(REVAPP''(z1, Cons(z2, z3))) SELECTS''(z0, z1, Nil) -> c15(REVAPP''(z1, Nil)) REVAPP''(Cons(z0, z1), z2) -> c18(REVAPP''(z1, Cons(z0, z2))) SELECTS''(z0, z1, Cons(z2, z3)) -> c14(SELECTS''(z2, Cons(z0, z1), z3)) Defined Rule Symbols:none Defined Pair Symbols: SELECTS'_3, REVAPP'_2, SELECTS''_3, REVAPP''_2 Compound Symbols: c7_2, c8_1, c11_1, c13_1, c14_1, c15_1, c18_1 ---------------------------------------- (15) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (16) BOUNDS(1, 1) ---------------------------------------- (17) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (18) 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: SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 The (relative) TRS S consists of the following rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (19) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence REVAPP(Cons(z0, z1), z2) ->^+ c5(REVAPP(z1, Cons(z0, z2))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / Cons(z0, z1)]. The result substitution is [z2 / Cons(z0, z2)]. ---------------------------------------- (20) Complex Obligation (BEST) ---------------------------------------- (21) 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: SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 The (relative) TRS S consists of the following rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (22) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (23) BOUNDS(n^1, INF) ---------------------------------------- (24) 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: SELECTS(z0, z1, Cons(z2, z3)) -> c(REVAPP(z1, Cons(z2, z3))) SELECTS(z0, z1, Cons(z2, z3)) -> c1(SELECTS(z2, Cons(z0, z1), z3)) SELECTS(z0, z1, Nil) -> c2(REVAPP(z1, Nil)) SELECT(Cons(z0, z1)) -> c3(SELECTS(z0, Nil, z1)) SELECT(Nil) -> c4 REVAPP(Cons(z0, z1), z2) -> c5(REVAPP(z1, Cons(z0, z2))) REVAPP(Nil, z0) -> c6 The (relative) TRS S consists of the following rules: selects(z0, z1, Cons(z2, z3)) -> Cons(Cons(z0, revapp(z1, Cons(z2, z3))), selects(z2, Cons(z0, z1), z3)) selects(z0, z1, Nil) -> Cons(Cons(z0, revapp(z1, Nil)), Nil) select(Cons(z0, z1)) -> selects(z0, Nil, z1) select(Nil) -> Nil revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2)) revapp(Nil, z0) -> z0 Rewrite Strategy: INNERMOST