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), 403 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 45 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), 8 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: DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) The (relative) TRS S consists of the following rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(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: DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) The (relative) TRS S consists of the following rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1)))) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1)))) DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) Tuples: DX'(z0) -> c14 DX'(a) -> c15 DX'(plus(z0, z1)) -> c16(DX'(z0), DX'(z1)) DX'(times(z0, z1)) -> c17(DX'(z0), DX'(z1)) DX'(minus(z0, z1)) -> c18(DX'(z0), DX'(z1)) DX'(neg(z0)) -> c19(DX'(z0)) DX'(div(z0, z1)) -> c20(DX'(z0), DX'(z1)) DX'(ln(z0)) -> c21(DX'(z0)) DX'(exp(z0, z1)) -> c22(DX'(z0), DX'(z1)) DX''(z0) -> c23 DX''(a) -> c24 DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) S tuples: DX''(z0) -> c23 DX''(a) -> c24 DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) K tuples:none Defined Rule Symbols: DX_1, dx_1 Defined Pair Symbols: DX'_1, DX''_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: DX'(a) -> c15 DX'(z0) -> c14 DX''(z0) -> c23 DX''(a) -> c24 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1)))) DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) Tuples: DX'(plus(z0, z1)) -> c16(DX'(z0), DX'(z1)) DX'(times(z0, z1)) -> c17(DX'(z0), DX'(z1)) DX'(minus(z0, z1)) -> c18(DX'(z0), DX'(z1)) DX'(neg(z0)) -> c19(DX'(z0)) DX'(div(z0, z1)) -> c20(DX'(z0), DX'(z1)) DX'(ln(z0)) -> c21(DX'(z0)) DX'(exp(z0, z1)) -> c22(DX'(z0), DX'(z1)) DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) S tuples: DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) K tuples:none Defined Rule Symbols: DX_1, dx_1 Defined Pair Symbols: DX'_1, DX''_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: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1)))) DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: DX'(plus(z0, z1)) -> c16(DX'(z0), DX'(z1)) DX'(times(z0, z1)) -> c17(DX'(z0), DX'(z1)) DX'(minus(z0, z1)) -> c18(DX'(z0), DX'(z1)) DX'(neg(z0)) -> c19(DX'(z0)) DX'(div(z0, z1)) -> c20(DX'(z0), DX'(z1)) DX'(ln(z0)) -> c21(DX'(z0)) DX'(exp(z0, z1)) -> c22(DX'(z0), DX'(z1)) DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) S tuples: DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: DX'_1, DX''_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. DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) We considered the (Usable) Rules:none And the Tuples: DX'(plus(z0, z1)) -> c16(DX'(z0), DX'(z1)) DX'(times(z0, z1)) -> c17(DX'(z0), DX'(z1)) DX'(minus(z0, z1)) -> c18(DX'(z0), DX'(z1)) DX'(neg(z0)) -> c19(DX'(z0)) DX'(div(z0, z1)) -> c20(DX'(z0), DX'(z1)) DX'(ln(z0)) -> c21(DX'(z0)) DX'(exp(z0, z1)) -> c22(DX'(z0), DX'(z1)) DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(DX'(x_1)) = x_1 POL(DX''(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(exp(x_1, x_2)) = [1] + x_1 + x_2 POL(ln(x_1)) = [1] + x_1 POL(minus(x_1, x_2)) = [1] + x_1 + x_2 POL(neg(x_1)) = [1] + x_1 POL(plus(x_1, x_2)) = [1] + x_1 + x_2 POL(times(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: DX'(plus(z0, z1)) -> c16(DX'(z0), DX'(z1)) DX'(times(z0, z1)) -> c17(DX'(z0), DX'(z1)) DX'(minus(z0, z1)) -> c18(DX'(z0), DX'(z1)) DX'(neg(z0)) -> c19(DX'(z0)) DX'(div(z0, z1)) -> c20(DX'(z0), DX'(z1)) DX'(ln(z0)) -> c21(DX'(z0)) DX'(exp(z0, z1)) -> c22(DX'(z0), DX'(z1)) DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) S tuples:none K tuples: DX''(plus(z0, z1)) -> c25(DX''(z0)) DX''(plus(z0, z1)) -> c26(DX''(z1)) DX''(times(z0, z1)) -> c27(DX''(z0)) DX''(times(z0, z1)) -> c28(DX''(z1)) DX''(minus(z0, z1)) -> c29(DX''(z0)) DX''(minus(z0, z1)) -> c30(DX''(z1)) DX''(neg(z0)) -> c31(DX''(z0)) DX''(div(z0, z1)) -> c32(DX''(z0)) DX''(div(z0, z1)) -> c33(DX''(z1)) DX''(ln(z0)) -> c34(DX''(z0)) DX''(exp(z0, z1)) -> c35(DX''(z0)) DX''(exp(z0, z1)) -> c36(DX''(z1)) Defined Rule Symbols:none Defined Pair Symbols: DX'_1, DX''_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: DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) The (relative) TRS S consists of the following rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(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 DX(times(z0, z1)) ->^+ c4(DX(z0)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / times(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: DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) The (relative) TRS S consists of the following rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(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: DX(z0) -> c DX(a) -> c1 DX(plus(z0, z1)) -> c2(DX(z0)) DX(plus(z0, z1)) -> c3(DX(z1)) DX(times(z0, z1)) -> c4(DX(z0)) DX(times(z0, z1)) -> c5(DX(z1)) DX(minus(z0, z1)) -> c6(DX(z0)) DX(minus(z0, z1)) -> c7(DX(z1)) DX(neg(z0)) -> c8(DX(z0)) DX(div(z0, z1)) -> c9(DX(z0)) DX(div(z0, z1)) -> c10(DX(z1)) DX(ln(z0)) -> c11(DX(z0)) DX(exp(z0, z1)) -> c12(DX(z0)) DX(exp(z0, z1)) -> c13(DX(z1)) The (relative) TRS S consists of the following rules: dx(z0) -> one dx(a) -> zero dx(plus(z0, z1)) -> plus(dx(z0), dx(z1)) dx(times(z0, z1)) -> plus(times(z1, dx(z0)), times(z0, dx(z1))) dx(minus(z0, z1)) -> minus(dx(z0), dx(z1)) dx(neg(z0)) -> neg(dx(z0)) dx(div(z0, z1)) -> minus(div(dx(z0), z1), times(z0, div(dx(z1), exp(z1, two)))) dx(ln(z0)) -> div(dx(z0), z0) dx(exp(z0, z1)) -> plus(times(z1, times(exp(z0, minus(z1, one)), dx(z0))), times(exp(z0, z1), times(ln(z0), dx(z1)))) Rewrite Strategy: INNERMOST