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), 421 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 1 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 37 ms] (10) CdtProblem (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (12) BOUNDS(1, 1) (13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (14) TRS for Loop Detection (15) DecreasingLoopProof [LOWER BOUND(ID), 3 ms] (16) BEST (17) proven lower bound (18) LowerBoundPropagationProof [FINISHED, 0 ms] (19) BOUNDS(n^1, INF) (20) 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: D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) The (relative) TRS S consists of the following rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) 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: D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) The (relative) TRS S consists of the following rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) Tuples: D''(t) -> c14 D''(constant) -> c15 D''(+(z0, z1)) -> c16(D''(z0), D''(z1)) D''(*(z0, z1)) -> c17(D''(z0), D''(z1)) D''(-(z0, z1)) -> c18(D''(z0), D''(z1)) D''(minus(z0)) -> c19(D''(z0)) D''(div(z0, z1)) -> c20(D''(z0), D''(z1)) D''(ln(z0)) -> c21(D''(z0)) D''(pow(z0, z1)) -> c22(D''(z0), D''(z1)) D'''(t) -> c23 D'''(constant) -> c24 D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) S tuples: D'''(t) -> c23 D'''(constant) -> c24 D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) K tuples:none Defined Rule Symbols: D'_1, D_1 Defined Pair Symbols: D''_1, D'''_1 Compound Symbols: c14, c15, c16_2, c17_2, c18_2, c19_1, c20_2, c21_1, c22_2, c23, c24, c25_1, c26_1, c27_1, c28_1, c29_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: D'''(t) -> c23 D''(constant) -> c15 D''(t) -> c14 D'''(constant) -> c24 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) Tuples: D''(+(z0, z1)) -> c16(D''(z0), D''(z1)) D''(*(z0, z1)) -> c17(D''(z0), D''(z1)) D''(-(z0, z1)) -> c18(D''(z0), D''(z1)) D''(minus(z0)) -> c19(D''(z0)) D''(div(z0, z1)) -> c20(D''(z0), D''(z1)) D''(ln(z0)) -> c21(D''(z0)) D''(pow(z0, z1)) -> c22(D''(z0), D''(z1)) D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) S tuples: D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) K tuples:none Defined Rule Symbols: D'_1, D_1 Defined Pair Symbols: D''_1, D'''_1 Compound Symbols: c16_2, c17_2, c18_2, c19_1, c20_2, c21_1, c22_2, c25_1, c26_1, c27_1, c28_1, c29_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: D''(+(z0, z1)) -> c16(D''(z0), D''(z1)) D''(*(z0, z1)) -> c17(D''(z0), D''(z1)) D''(-(z0, z1)) -> c18(D''(z0), D''(z1)) D''(minus(z0)) -> c19(D''(z0)) D''(div(z0, z1)) -> c20(D''(z0), D''(z1)) D''(ln(z0)) -> c21(D''(z0)) D''(pow(z0, z1)) -> c22(D''(z0), D''(z1)) D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) S tuples: D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: D''_1, D'''_1 Compound Symbols: c16_2, c17_2, c18_2, c19_1, c20_2, c21_1, c22_2, c25_1, c26_1, c27_1, c28_1, c29_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_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. D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) We considered the (Usable) Rules:none And the Tuples: D''(+(z0, z1)) -> c16(D''(z0), D''(z1)) D''(*(z0, z1)) -> c17(D''(z0), D''(z1)) D''(-(z0, z1)) -> c18(D''(z0), D''(z1)) D''(minus(z0)) -> c19(D''(z0)) D''(div(z0, z1)) -> c20(D''(z0), D''(z1)) D''(ln(z0)) -> c21(D''(z0)) D''(pow(z0, z1)) -> c22(D''(z0), D''(z1)) D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = [1] + x_1 + x_2 POL(+(x_1, x_2)) = [1] + x_1 + x_2 POL(-(x_1, x_2)) = [1] + x_1 + x_2 POL(D''(x_1)) = x_1 POL(D'''(x_1)) = x_1 POL(c16(x_1, x_2)) = x_1 + x_2 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1)) = x_1 POL(c20(x_1, x_2)) = x_1 + x_2 POL(c21(x_1)) = x_1 POL(c22(x_1, x_2)) = x_1 + x_2 POL(c25(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(c30(x_1)) = x_1 POL(c31(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1)) = x_1 POL(c36(x_1)) = x_1 POL(div(x_1, x_2)) = [1] + x_1 + x_2 POL(ln(x_1)) = [1] + x_1 POL(minus(x_1)) = [1] + x_1 POL(pow(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: D''(+(z0, z1)) -> c16(D''(z0), D''(z1)) D''(*(z0, z1)) -> c17(D''(z0), D''(z1)) D''(-(z0, z1)) -> c18(D''(z0), D''(z1)) D''(minus(z0)) -> c19(D''(z0)) D''(div(z0, z1)) -> c20(D''(z0), D''(z1)) D''(ln(z0)) -> c21(D''(z0)) D''(pow(z0, z1)) -> c22(D''(z0), D''(z1)) D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) S tuples:none K tuples: D'''(+(z0, z1)) -> c25(D'''(z0)) D'''(+(z0, z1)) -> c26(D'''(z1)) D'''(*(z0, z1)) -> c27(D'''(z0)) D'''(*(z0, z1)) -> c28(D'''(z1)) D'''(-(z0, z1)) -> c29(D'''(z0)) D'''(-(z0, z1)) -> c30(D'''(z1)) D'''(minus(z0)) -> c31(D'''(z0)) D'''(div(z0, z1)) -> c32(D'''(z0)) D'''(div(z0, z1)) -> c33(D'''(z1)) D'''(ln(z0)) -> c34(D'''(z0)) D'''(pow(z0, z1)) -> c35(D'''(z0)) D'''(pow(z0, z1)) -> c36(D'''(z1)) Defined Rule Symbols:none Defined Pair Symbols: D''_1, D'''_1 Compound Symbols: c16_2, c17_2, c18_2, c19_1, c20_2, c21_1, c22_2, c25_1, c26_1, c27_1, c28_1, c29_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1 ---------------------------------------- (11) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (12) BOUNDS(1, 1) ---------------------------------------- (13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (14) 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: D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) The (relative) TRS S consists of the following rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) Rewrite Strategy: INNERMOST ---------------------------------------- (15) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence D'(+(z0, z1)) ->^+ c3(D'(z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / +(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (16) Complex Obligation (BEST) ---------------------------------------- (17) 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: D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) The (relative) TRS S consists of the following rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) Rewrite Strategy: INNERMOST ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (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: D'(t) -> c D'(constant) -> c1 D'(+(z0, z1)) -> c2(D'(z0)) D'(+(z0, z1)) -> c3(D'(z1)) D'(*(z0, z1)) -> c4(D'(z0)) D'(*(z0, z1)) -> c5(D'(z1)) D'(-(z0, z1)) -> c6(D'(z0)) D'(-(z0, z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) D'(div(z0, z1)) -> c9(D'(z0)) D'(div(z0, z1)) -> c10(D'(z1)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0, z1)) -> c12(D'(z0)) D'(pow(z0, z1)) -> c13(D'(z1)) The (relative) TRS S consists of the following rules: D(t) -> 1 D(constant) -> 0 D(+(z0, z1)) -> +(D(z0), D(z1)) D(*(z0, z1)) -> +(*(z1, D(z0)), *(z0, D(z1))) D(-(z0, z1)) -> -(D(z0), D(z1)) D(minus(z0)) -> minus(D(z0)) D(div(z0, z1)) -> -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) D(ln(z0)) -> div(D(z0), z0) D(pow(z0, z1)) -> +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1))) Rewrite Strategy: INNERMOST