WORST_CASE(?,O(n^1)) proof of input_iUUQYoeoAw.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) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 60 ms] (6) CdtProblem (7) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (8) 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, y) -> 0 f(s(x), y) -> f(f(x, y), y) 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, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) Tuples: F(0, z0) -> c F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) S tuples: F(0, z0) -> c F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c, c1_2 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, z0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) Tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) S tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c1_2 ---------------------------------------- (5) 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), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) We considered the (Usable) Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) And the Tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(F(x_1, x_2)) = [1] + [3]x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(f(x_1, x_2)) = 0 POL(s(x_1)) = [3] + x_1 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) Tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) S tuples:none K tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c1_2 ---------------------------------------- (7) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (8) BOUNDS(1, 1)