WORST_CASE(?,O(n^1)) proof of input_mxICHJNz0i.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) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 66 ms] (8) CdtProblem (9) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (16) CdtProblem (17) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms] (20) CdtProblem (21) SIsEmptyProof [BOTH BOUNDS(ID, ID), 1 ms] (22) 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(x, 0) -> s(0) f(s(x), s(y)) -> s(f(x, y)) g(0, x) -> g(f(x, x), 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(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) g(0, z0) -> g(f(z0, z0), z0) Tuples: F(z0, 0) -> c F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) S tuples: F(z0, 0) -> c F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) K tuples:none Defined Rule Symbols: f_2, g_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c, c1_1, c2_2 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(z0, 0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) g(0, z0) -> g(f(z0, z0), z0) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) K tuples:none Defined Rule Symbols: f_2, g_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c1_1, c2_2 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: g(0, z0) -> g(f(z0, z0), z0) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c1_1, c2_2 ---------------------------------------- (7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) We considered the (Usable) Rules: f(s(z0), s(z1)) -> s(f(z0, z1)) f(z0, 0) -> s(0) And the Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [2] POL(F(x_1, x_2)) = [1] POL(G(x_1, x_2)) = [2]x_1 POL(c1(x_1)) = x_1 POL(c2(x_1, x_2)) = x_1 + x_2 POL(f(x_1, x_2)) = 0 POL(s(x_1)) = 0 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) K tuples: G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) Defined Rule Symbols: f_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c1_1, c2_2 ---------------------------------------- (9) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) by G(0, 0) -> c2(G(s(0), 0), F(0, 0)) G(0, s(z0)) -> c2(G(s(f(z0, z0)), s(z0)), F(s(z0), s(z0))) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, 0) -> c2(G(s(0), 0), F(0, 0)) G(0, s(z0)) -> c2(G(s(f(z0, z0)), s(z0)), F(s(z0), s(z0))) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) K tuples: G(0, z0) -> c2(G(f(z0, z0), z0), F(z0, z0)) Defined Rule Symbols: f_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c1_1, c2_2 ---------------------------------------- (11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: G(0, 0) -> c2(G(s(0), 0), F(0, 0)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, s(z0)) -> c2(G(s(f(z0, z0)), s(z0)), F(s(z0), s(z0))) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c1_1, c2_2 ---------------------------------------- (13) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) G(0, s(z0)) -> c2(F(s(z0), s(z0))) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2, G_2 Compound Symbols: c1_1, c2_1 ---------------------------------------- (15) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: G(0, s(z0)) -> c2(F(s(z0), s(z0))) ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c1_1 ---------------------------------------- (17) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f(z0, 0) -> s(0) f(s(z0), s(z1)) -> s(f(z0, z1)) ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) S tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: F_2 Compound Symbols: c1_1 ---------------------------------------- (19) 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), s(z1)) -> c1(F(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F(x_1, x_2)) = x_2 POL(c1(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) S tuples:none K tuples: F(s(z0), s(z1)) -> c1(F(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_2 Compound Symbols: c1_1 ---------------------------------------- (21) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (22) BOUNDS(1, 1)