WORST_CASE(?,O(n^1)) proof of input_TvN0N0k2aK.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 [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtRhsSimplificationProcessorProof [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)), 33 ms] (10) CdtProblem (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (12) 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: f(0) -> 1 f(s(x)) -> g(f(x)) g(x) -> +(x, s(x)) f(s(x)) -> +(f(x), s(f(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: f(0) -> 1 f(s(z0)) -> g(f(z0)) f(s(z0)) -> +(f(z0), s(f(z0))) g(z0) -> +(z0, s(z0)) Tuples: F(0) -> c F(s(z0)) -> c1(G(f(z0)), F(z0)) F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) G(z0) -> c4 S tuples: F(0) -> c F(s(z0)) -> c1(G(f(z0)), F(z0)) F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) G(z0) -> c4 K tuples:none Defined Rule Symbols: f_1, g_1 Defined Pair Symbols: F_1, G_1 Compound Symbols: c, c1_2, c2_1, c3_1, c4 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: G(z0) -> c4 F(0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(0) -> 1 f(s(z0)) -> g(f(z0)) f(s(z0)) -> +(f(z0), s(f(z0))) g(z0) -> +(z0, s(z0)) Tuples: F(s(z0)) -> c1(G(f(z0)), F(z0)) F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) S tuples: F(s(z0)) -> c1(G(f(z0)), F(z0)) F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) K tuples:none Defined Rule Symbols: f_1, g_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2, c2_1, c3_1 ---------------------------------------- (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f(0) -> 1 f(s(z0)) -> g(f(z0)) f(s(z0)) -> +(f(z0), s(f(z0))) g(z0) -> +(z0, s(z0)) Tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) S tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) K tuples:none Defined Rule Symbols: f_1, g_1 Defined Pair Symbols: F_1 Compound Symbols: c2_1, c3_1, c1_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f(0) -> 1 f(s(z0)) -> g(f(z0)) f(s(z0)) -> +(f(z0), s(f(z0))) g(z0) -> +(z0, s(z0)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) S tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: F_1 Compound Symbols: c2_1, c3_1, c1_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. F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) We considered the (Usable) Rules:none And the Tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) S tuples:none K tuples: F(s(z0)) -> c2(F(z0)) F(s(z0)) -> c3(F(z0)) F(s(z0)) -> c1(F(z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1 Compound Symbols: c2_1, c3_1, c1_1 ---------------------------------------- (11) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (12) BOUNDS(1, 1)