WORST_CASE(?,O(n^1)) proof of input_guymdr22oQ.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) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 56 ms] (8) CdtProblem (9) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (10) 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(g(x)) -> f(a(g(g(f(x))), g(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(g(z0)) -> f(a(g(g(f(z0))), g(f(z0)))) Tuples: F(g(z0)) -> c(F(a(g(g(f(z0))), g(f(z0)))), F(z0)) F(g(z0)) -> c1(F(a(g(g(f(z0))), g(f(z0)))), F(z0)) S tuples: F(g(z0)) -> c(F(a(g(g(f(z0))), g(f(z0)))), F(z0)) F(g(z0)) -> c1(F(a(g(g(f(z0))), g(f(z0)))), F(z0)) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c_2, c1_2 ---------------------------------------- (3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0)) -> f(a(g(g(f(z0))), g(f(z0)))) Tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) S tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c_1, c1_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f(g(z0)) -> f(a(g(g(f(z0))), g(f(z0)))) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) S tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: F_1 Compound Symbols: c_1, c1_1 ---------------------------------------- (7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) We considered the (Usable) Rules:none And the Tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F(x_1)) = [3]x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(g(x_1)) = [3] + x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) S tuples:none K tuples: F(g(z0)) -> c(F(z0)) F(g(z0)) -> c1(F(z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1 Compound Symbols: c_1, c1_1 ---------------------------------------- (9) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (10) BOUNDS(1, 1)